%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM672+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 : n019.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:23 PM UTC 2026
% Result : Theorem 23.34s 4.83s
% Output : Refutation 27.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 36
% Syntax : Number of formulae : 201 ( 34 unt; 21 def)
% Number of atoms : 487 ( 2 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 490 ( 204 ~; 216 |; 28 &)
% ( 37 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 22 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 12 con; 0-2 aty)
% Number of variables : 125 ( 0 sgn 123 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X1),X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f29,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f35,axiom,
! [X0] : scratc1121938171d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__n__pl) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc926143280_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f150,axiom,
pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_bw)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz19a) ).
fof(f171,axiom,
pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_dq)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz12) ).
fof(f298,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0))
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__35) ).
fof(f317,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bw,X0))
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__54) ).
fof(f319,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__56) ).
fof(f342,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__79) ).
fof(f373,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__110) ).
fof(f375,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__112) ).
fof(f392,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__129) ).
fof(f399,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__136) ).
fof(f458,conjecture,
pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f459,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f458]) ).
fof(f460,plain,
~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f459]) ).
fof(f477,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc926143280_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f478,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc926143280_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f477]) ).
fof(f544,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f342]) ).
fof(f558,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1)) ) ),
inference(ennf_transformation,[],[f392]) ).
fof(f569,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f399]) ).
fof(f596,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f597,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f660,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc926143280_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc926143280_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f478]) ).
fof(f661,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc926143280_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc926143280_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1)) ) ),
inference(rectify,[],[f660]) ).
fof(f662,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc926143280_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc926143280_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f661]) ).
fof(f716,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0))) )
& ( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0)) ) ),
inference(nnf_transformation,[],[f298]) ).
fof(f735,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bw,X0))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,X0))) )
& ( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bw,X0)) ) ),
inference(nnf_transformation,[],[f317]) ).
fof(f737,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f319]) ).
fof(f768,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1)) ) ),
inference(nnf_transformation,[],[f544]) ).
fof(f769,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1)) ) ),
inference(flattening,[],[f768]) ).
fof(f806,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,X0),X1)) ) ),
inference(nnf_transformation,[],[f373]) ).
fof(f808,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1)) ) ),
inference(nnf_transformation,[],[f375]) ).
fof(f826,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f558]) ).
fof(f827,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2)) ) ),
inference(flattening,[],[f826]) ).
fof(f840,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f569]) ).
fof(f841,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f840]) ).
fof(f924,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f596]) ).
fof(f925,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f597]) ).
fof(f937,plain,
! [X0] : scratc1121938171d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f1111,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc926143280_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1)) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1112,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1113,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| scratc926143280_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1114,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1118,plain,
pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_bw)),
inference(cnf_transformation,[],[f150]) ).
fof(f1139,plain,
pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_dq)),
inference(cnf_transformation,[],[f171]) ).
fof(f1330,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dq,X0)) ),
inference(cnf_transformation,[],[f716]) ).
fof(f1368,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bw,X0)) ),
inference(cnf_transformation,[],[f735]) ).
fof(f1373,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f737]) ).
fof(f1424,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,X0),X1)) ),
inference(cnf_transformation,[],[f769]) ).
fof(f1493,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,X0),X1)) ),
inference(cnf_transformation,[],[f806]) ).
fof(f1498,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f808]) ).
fof(f1532,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2)) ),
inference(cnf_transformation,[],[f827]) ).
fof(f1558,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f841]) ).
fof(f1559,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1121938171d_n_pl(X1),X2))) ),
inference(cnf_transformation,[],[f841]) ).
fof(f1677,plain,
~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f460]) ).
fof(f1781,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X1)),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(X0),X1),X2)) ),
inference(definition_unfolding,[],[f1532,f937,f937]) ).
fof(f1786,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,X1)),X2))) ),
inference(definition_unfolding,[],[f1559,f937,f937]) ).
fof(f1843,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f1845,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f1843]) ).
fof(f1846,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f1677,f1843]) ).
fof(f1847,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f1845,f1112]) ).
fof(f1848,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f1845,f1113]) ).
fof(f1849,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f1845,f1114]) ).
fof(f1862,definition,
( spl29_2
<=> scratc926143280_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f1864,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1865,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f1848,f1843,f1862]) ).
fof(f1867,definition,
( spl29_3
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f1869,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_3 ),
inference(avatar_component_clause,[],[f1867]) ).
fof(f1870,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f1849,f1843,f1867]) ).
fof(f1871,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_3 ),
inference(resolution,[],[f1869,f1373]) ).
fof(f1909,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f1864,f1111]) ).
fof(f1910,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f1909,f1847]) ).
fof(f1912,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f1913,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f1912]) ).
fof(f1914,plain,
( spl29_4
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f1910,f1862,f1843,f1912]) ).
fof(f2223,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_dq))
| pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(resolution,[],[f1913,f1330]) ).
fof(f2299,plain,
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f2223,f1139]) ).
fof(f2390,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f2392,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f2390]) ).
fof(f2393,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f1871,f1867,f2390]) ).
fof(f2395,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(resolution,[],[f2392,f1112]) ).
fof(f2396,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
| spl29_6 ),
inference(resolution,[],[f2392,f1113]) ).
fof(f2397,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_6 ),
inference(resolution,[],[f2392,f1114]) ).
fof(f2410,definition,
( spl29_7
<=> scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f2412,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f2410]) ).
fof(f2413,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f2396,f2390,f2410]) ).
fof(f2415,definition,
( spl29_8
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f2417,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_8 ),
inference(avatar_component_clause,[],[f2415]) ).
fof(f2418,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f2397,f2390,f2415]) ).
fof(f2419,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_8 ),
inference(resolution,[],[f2417,f1498]) ).
fof(f2465,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f2467,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_9 ),
inference(avatar_component_clause,[],[f2465]) ).
fof(f2468,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f2419,f2415,f2465]) ).
fof(f2470,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_9 ),
inference(resolution,[],[f2467,f1112]) ).
fof(f2471,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
| spl29_9 ),
inference(resolution,[],[f2467,f1113]) ).
fof(f2472,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_9 ),
inference(resolution,[],[f2467,f1114]) ).
fof(f2485,definition,
( spl29_10
<=> scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f2487,plain,
( scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f2485]) ).
fof(f2488,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f2471,f2465,f2485]) ).
fof(f2493,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f2412,f1111]) ).
fof(f2494,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f2493,f2395]) ).
fof(f2496,definition,
( spl29_11
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f2497,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f2496]) ).
fof(f2498,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f2494,f2410,f2390,f2496]) ).
fof(f2787,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aTP_Lamm_bw))
| pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(resolution,[],[f2497,f1368]) ).
fof(f2904,plain,
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f2787,f1118]) ).
fof(f3160,definition,
( spl29_15
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f3162,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_15 ),
inference(avatar_component_clause,[],[f3160]) ).
fof(f3163,plain,
( ~ spl29_15
| spl29_9 ),
inference(avatar_split_clause,[],[f2472,f2465,f3160]) ).
fof(f3164,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_15 ),
inference(resolution,[],[f3162,f1558]) ).
fof(f3165,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_15 ),
inference(resolution,[],[f3162,f1786]) ).
fof(f3211,definition,
( spl29_16
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
fof(f3213,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_16 ),
inference(avatar_component_clause,[],[f3211]) ).
fof(f3214,plain,
( ~ spl29_16
| spl29_15 ),
inference(avatar_split_clause,[],[f3165,f3160,f3211]) ).
fof(f3216,plain,
( ~ pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))))
| spl29_16 ),
inference(resolution,[],[f3213,f924]) ).
fof(f3274,definition,
( spl29_17
<=> pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).
fof(f3276,plain,
( ~ pp(aa_fun171081125l_bool(scratc2128566643n_some,aa_TPT43085870d_bool(scratc1789090231ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))))
| spl29_17 ),
inference(avatar_component_clause,[],[f3274]) ).
fof(f3277,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f3216,f3211,f3274]) ).
fof(f3278,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_17 ),
inference(resolution,[],[f3276,f925]) ).
fof(f3292,definition,
( spl29_18
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_18])],[avatar_definition]) ).
fof(f3294,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc972347070bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1994158633d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_18 ),
inference(avatar_component_clause,[],[f3292]) ).
fof(f3295,plain,
( ~ spl29_18
| spl29_17 ),
inference(avatar_split_clause,[],[f3278,f3274,f3292]) ).
fof(f3296,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_18 ),
inference(resolution,[],[f3294,f1781]) ).
fof(f3353,definition,
( spl29_19
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f3355,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_19 ),
inference(avatar_component_clause,[],[f3353]) ).
fof(f3357,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f3359,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1230437244_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_20 ),
inference(avatar_component_clause,[],[f3357]) ).
fof(f3360,plain,
( ~ spl29_19
| ~ spl29_20
| spl29_18 ),
inference(avatar_split_clause,[],[f3296,f3292,f3357,f3353]) ).
fof(f3372,plain,
( ! [X0] :
( ~ scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
| spl29_19 ),
inference(resolution,[],[f3355,f1111]) ).
fof(f3406,plain,
( ! [X0] :
( ~ scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
| spl29_9
| spl29_19 ),
inference(forward_subsumption_resolution,[],[f3372,f2470]) ).
fof(f3408,definition,
( spl29_21
<=> ! [X0] :
( ~ scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ) ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
fof(f3409,plain,
( ! [X0] :
( ~ scratc926143280_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc126597545all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) )
| ~ spl29_21 ),
inference(avatar_component_clause,[],[f3408]) ).
fof(f3410,plain,
( spl29_21
| spl29_9
| spl29_19 ),
inference(avatar_split_clause,[],[f3406,f3353,f2465,f3408]) ).
fof(f3413,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc501764986nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_20 ),
inference(resolution,[],[f3359,f1424]) ).
fof(f3466,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_15
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f3413,f3164]) ).
fof(f3468,definition,
( spl29_22
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_22])],[avatar_definition]) ).
fof(f3470,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_22 ),
inference(avatar_component_clause,[],[f3468]) ).
fof(f3471,plain,
( ~ spl29_22
| spl29_15
| spl29_20 ),
inference(avatar_split_clause,[],[f3466,f3357,f3160,f3468]) ).
fof(f3480,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dp,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_11
| spl29_22 ),
inference(resolution,[],[f3470,f2497]) ).
fof(f3519,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_22 ),
inference(forward_subsumption_resolution,[],[f3480,f2299]) ).
fof(f3520,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_22 ),
inference(avatar_contradiction_clause,[],[f3519]) ).
fof(f3604,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_10
| ~ spl29_21 ),
inference(resolution,[],[f3409,f2487]) ).
fof(f3681,definition,
( spl29_27
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_27])],[avatar_definition]) ).
fof(f3683,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bu(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_27 ),
inference(avatar_component_clause,[],[f3681]) ).
fof(f3684,plain,
( ~ spl29_27
| ~ spl29_10
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f3604,f3408,f2485,f3681]) ).
fof(f4477,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_27 ),
inference(resolution,[],[f3683,f1493]) ).
fof(f6511,definition,
( spl29_131
<=> pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_131])],[avatar_definition]) ).
fof(f6513,plain,
( pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_131 ),
inference(avatar_component_clause,[],[f6511]) ).
fof(f6514,plain,
( spl29_131
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f2904,f2496,f6511]) ).
fof(f6950,definition,
( spl29_148
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_148])],[avatar_definition]) ).
fof(f6952,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_148 ),
inference(avatar_component_clause,[],[f6950]) ).
fof(f6953,plain,
( ~ spl29_148
| spl29_27 ),
inference(avatar_split_clause,[],[f4477,f3681,f6950]) ).
fof(f6961,plain,
( ~ pp(aa_fun171081125l_bool(scratc126597545all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_4
| spl29_148 ),
inference(resolution,[],[f6952,f1913]) ).
fof(f7000,plain,
( $false
| ~ spl29_4
| ~ spl29_131
| spl29_148 ),
inference(forward_subsumption_resolution,[],[f6961,f6513]) ).
fof(f7001,plain,
( ~ spl29_4
| ~ spl29_131
| spl29_148 ),
inference(avatar_contradiction_clause,[],[f7000]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f1846]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f1865]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s4,plain,
( spl29_1
| ~ spl29_2
| spl29_4 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f2393]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f2413]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f2418]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f2468]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f2488]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f2498]) ).
cnf(s15,plain,
( spl29_9
| ~ spl29_15 ),
inference(sat_conversion,[],[f3163]) ).
cnf(s16,plain,
( spl29_15
| ~ spl29_16 ),
inference(sat_conversion,[],[f3214]) ).
cnf(s17,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f3277]) ).
cnf(s18,plain,
( spl29_17
| ~ spl29_18 ),
inference(sat_conversion,[],[f3295]) ).
cnf(s19,plain,
( spl29_18
| ~ spl29_19
| ~ spl29_20 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s20,plain,
( spl29_9
| spl29_19
| spl29_21 ),
inference(sat_conversion,[],[f3410]) ).
cnf(s21,plain,
( spl29_15
| spl29_20
| ~ spl29_22 ),
inference(sat_conversion,[],[f3471]) ).
cnf(s22,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_22 ),
inference(sat_conversion,[],[f3520]) ).
cnf(s27,plain,
( ~ spl29_10
| ~ spl29_21
| ~ spl29_27 ),
inference(sat_conversion,[],[f3684]) ).
cnf(s133,plain,
( ~ spl29_11
| spl29_131 ),
inference(sat_conversion,[],[f6514]) ).
cnf(s150,plain,
( spl29_27
| ~ spl29_148 ),
inference(sat_conversion,[],[f6953]) ).
cnf(s151,plain,
( ~ spl29_4
| ~ spl29_131
| spl29_148 ),
inference(sat_conversion,[],[f7001]) ).
cnf(s153,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s154,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s160,plain,
~ spl29_6,
inference(rat,[],[s6,s153]) ).
cnf(s161,plain,
spl29_4,
inference(rat,[],[s4,s1,s154]) ).
cnf(s163,plain,
~ spl29_8,
inference(rat,[],[s8,s160]) ).
cnf(s164,plain,
spl29_7,
inference(rat,[],[s7,s160]) ).
cnf(s212,plain,
~ spl29_9,
inference(rat,[],[s9,s163]) ).
cnf(s213,plain,
spl29_11,
inference(rat,[],[s11,s160,s164]) ).
cnf(s216,plain,
~ spl29_15,
inference(rat,[],[s15,s212]) ).
cnf(s217,plain,
spl29_10,
inference(rat,[],[s10,s212]) ).
cnf(s229,plain,
spl29_131,
inference(rat,[],[s133,s213]) ).
cnf(s263,plain,
spl29_22,
inference(rat,[],[s22,s161,s213]) ).
cnf(s268,plain,
spl29_20,
inference(rat,[],[s21,s263,s216]) ).
cnf(s269,plain,
~ spl29_16,
inference(rat,[],[s16,s216]) ).
cnf(s271,plain,
spl29_148,
inference(rat,[],[s151,s161,s229]) ).
cnf(s280,plain,
~ spl29_17,
inference(rat,[],[s17,s269]) ).
cnf(s282,plain,
spl29_27,
inference(rat,[],[s150,s271]) ).
cnf(s285,plain,
~ spl29_18,
inference(rat,[],[s18,s280]) ).
cnf(s286,plain,
~ spl29_21,
inference(rat,[],[s27,s217,s282]) ).
cnf(s291,plain,
~ spl29_19,
inference(rat,[],[s19,s268,s285]) ).
cnf(s292,plain,
$false,
inference(rat,[],[s20,s212,s286,s291]) ).
fof(f7002,plain,
$false,
inference(avatar_sat_refutation,[],[s292]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM672+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.43 % Computer : n019.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 27 21:02:48 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.49 Running first-order theorem proving
% 0.21/0.49 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
% 18.74/3.78 % (3401184)Detected formulas, will run a generic FOF schedule.
% 18.74/3.78 % (3401190)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=2771173803:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 18.74/3.78 % (3401189)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=4192739367:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 18.74/3.78 % (3401194)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1288913377:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 18.74/3.78 % (3401191)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=2113912135:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 18.74/3.78 % (3401193)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2896007474:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 18.74/3.78 % (3401192)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1606604307:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 18.74/3.78 % (3401195)dis-21_1_sil=8000:lcm=predicate:random_seed=2023298628: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)
% 18.74/3.78 % (3401192)Refutation not found, incomplete strategy
% 18.74/3.78 % (3401192)------------------------------
% 18.74/3.78 % (3401192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.78 % (3401192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.78 % (3401192)CaDiCaL version: 2.1.3
% 18.74/3.78 % (3401192)Termination reason: Refutation not found, incomplete strategy
% 18.74/3.78 % (3401192)Time elapsed: 0.003 s
% 18.74/3.78 % (3401192)Peak memory usage: 87 MB
% 18.74/3.78 % (3401192)Instructions burned: 2 (million)
% 18.74/3.78 % (3401193)Refutation not found, incomplete strategy
% 18.74/3.78 % (3401193)------------------------------
% 18.74/3.78 % (3401193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.78 % (3401193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.78 % (3401193)CaDiCaL version: 2.1.3
% 18.74/3.78 % (3401193)Termination reason: Refutation not found, incomplete strategy
% 18.74/3.78 % (3401193)Time elapsed: 0.004 s
% 18.74/3.78 % (3401193)Peak memory usage: 87 MB
% 18.74/3.78 % (3401193)Instructions burned: 2 (million)
% 18.74/3.78 % (3401195)Instruction limit reached!
% 18.74/3.78 % (3401195)------------------------------
% 18.74/3.78 % (3401195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.78 % (3401195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.78 % (3401195)CaDiCaL version: 2.1.3
% 18.74/3.78 % (3401195)Termination reason: Instruction limit
% 18.74/3.78 % (3401195)Termination phase: Saturation
% 18.74/3.78 % (3401195)Time elapsed: 0.134 s
% 18.74/3.78 % (3401195)Peak memory usage: 90 MB
% 18.74/3.78 % (3401195)Instructions burned: 129 (million)
% 18.74/3.78 % (3401194)Instruction limit reached!
% 18.74/3.78 % (3401194)------------------------------
% 18.74/3.78 % (3401194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.78 % (3401194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.78 % (3401194)CaDiCaL version: 2.1.3
% 18.74/3.78 % (3401194)Termination reason: Instruction limit
% 18.74/3.78 % (3401194)Termination phase: Saturation
% 18.74/3.78 % (3401194)Time elapsed: 0.147 s
% 18.74/3.78 % (3401194)Peak memory usage: 90 MB
% 18.74/3.78 % (3401194)Instructions burned: 139 (million)
% 18.74/3.78 % (3401203)lrs+10_1_sil=8000:sp=occurrence:random_seed=2481191245:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 18.74/3.78 % (3401203)Refutation not found, incomplete strategy
% 18.74/3.78 % (3401203)------------------------------
% 18.74/3.78 % (3401203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/3.78 % (3401203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/3.78 % (3401203)CaDiCaL version: 2.1.3
% 18.74/3.78 % (3401203)Termination reason: Refutation not found, incomplete strategy
% 18.74/3.78 % (3401203)Time elapsed: 0.003 s
% 18.74/3.78 % (3401203)Peak memory usage: 88 MB
% 18.74/3.78 % (3401203)Instructions burned: 2 (million)
% 18.74/3.78 % (3401193)------------------------------
% 23.34/4.82 % (3401193)------------------------------
% 23.34/4.82 % (3401192)------------------------------
% 23.34/4.82 % (3401192)------------------------------
% 23.34/4.82 % (3401204)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1881662818:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 23.34/4.82 % (3401204)Refutation not found, incomplete strategy
% 23.34/4.82 % (3401204)------------------------------
% 23.34/4.82 % (3401204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.82 % (3401204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.82 % (3401204)CaDiCaL version: 2.1.3
% 23.34/4.82 % (3401204)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.82 % (3401204)Time elapsed: 0.008 s
% 23.34/4.82 % (3401204)Peak memory usage: 88 MB
% 23.34/4.82 % (3401204)Instructions burned: 7 (million)
% 23.34/4.82 % (3401203)------------------------------
% 23.34/4.82 % (3401203)------------------------------
% 23.34/4.82 % (3401206)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1104180759:i=325:sd=1:ss=axioms:sgt=32_2992 on theBenchmark for (2992ds/325Mi)
% 23.34/4.83 % (3401207)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=3468119192:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 23.34/4.83 % (3401206)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401206)------------------------------
% 23.34/4.83 % (3401206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401206)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401206)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401206)Time elapsed: 0.007 s
% 23.34/4.83 % (3401206)Peak memory usage: 89 MB
% 23.34/4.83 % (3401206)Instructions burned: 5 (million)
% 23.34/4.83 % (3401204)------------------------------
% 23.34/4.83 % (3401204)------------------------------
% 23.34/4.83 % (3401209)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=933277243:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 23.34/4.83 % (3401209)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401209)------------------------------
% 23.34/4.83 % (3401209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401209)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401209)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401209)Time elapsed: 0.007 s
% 23.34/4.83 % (3401209)Peak memory usage: 88 MB
% 23.34/4.83 % (3401209)Instructions burned: 6 (million)
% 23.34/4.83 % (3401207)Instruction limit reached!
% 23.34/4.83 % (3401207)------------------------------
% 23.34/4.83 % (3401207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401207)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401207)Termination reason: Instruction limit
% 23.34/4.83 % (3401207)Termination phase: Saturation
% 23.34/4.83 % (3401207)Time elapsed: 0.214 s
% 23.34/4.83 % (3401207)Peak memory usage: 94 MB
% 23.34/4.83 % (3401207)Instructions burned: 248 (million)
% 23.34/4.83 % (3401206)------------------------------
% 23.34/4.83 % (3401206)------------------------------
% 23.34/4.83 % (3401212)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1054581848:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 23.34/4.83 % (3401214)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2173066737:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 23.34/4.83 % (3401209)------------------------------
% 23.34/4.83 % (3401209)------------------------------
% 23.34/4.83 % (3401214)Instruction limit reached!
% 23.34/4.83 % (3401214)------------------------------
% 23.34/4.83 % (3401214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401214)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401214)Termination reason: Instruction limit
% 23.34/4.83 % (3401214)Termination phase: Saturation
% 23.34/4.83 % (3401214)Time elapsed: 0.108 s
% 23.34/4.83 % (3401214)Peak memory usage: 90 MB
% 23.34/4.83 % (3401214)Instructions burned: 113 (million)
% 23.34/4.83 % (3401215)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3300632216:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 23.34/4.83 % (3401215)Instruction limit reached!
% 23.34/4.83 % (3401215)------------------------------
% 23.34/4.83 % (3401215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401215)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401215)Termination reason: Instruction limit
% 23.34/4.83 % (3401215)Termination phase: Saturation
% 23.34/4.83 % (3401215)Time elapsed: 0.106 s
% 23.34/4.83 % (3401215)Peak memory usage: 89 MB
% 23.34/4.83 % (3401215)Instructions burned: 127 (million)
% 23.34/4.83 % (3401218)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2748141465:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2984 on theBenchmark for (2984ds/114Mi)
% 23.34/4.83 % (3401219)lrs+10_1_sil=8000:sp=occurrence:random_seed=2136585236:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 23.34/4.83 % (3401219)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401219)------------------------------
% 23.34/4.83 % (3401219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401219)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401219)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401219)Time elapsed: 0.004 s
% 23.34/4.83 % (3401219)Peak memory usage: 88 MB
% 23.34/4.83 % (3401219)Instructions burned: 2 (million)
% 23.34/4.83 % (3401218)Instruction limit reached!
% 23.34/4.83 % (3401218)------------------------------
% 23.34/4.83 % (3401218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401218)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401218)Termination reason: Instruction limit
% 23.34/4.83 % (3401218)Termination phase: Saturation
% 23.34/4.83 % (3401218)Time elapsed: 0.107 s
% 23.34/4.83 % (3401218)Peak memory usage: 89 MB
% 23.34/4.83 % (3401218)Instructions burned: 115 (million)
% 23.34/4.83 % (3401221)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3350975286:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 23.34/4.83 % (3401221)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401221)------------------------------
% 23.34/4.83 % (3401221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401221)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401221)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401221)Time elapsed: 0.056 s
% 23.34/4.83 % (3401221)Peak memory usage: 90 MB
% 23.34/4.83 % (3401221)Instructions burned: 62 (million)
% 23.34/4.83 % (3401224)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=187256029:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 23.34/4.83 % (3401219)------------------------------
% 23.34/4.83 % (3401219)------------------------------
% 23.34/4.83 % (3401221)------------------------------
% 23.34/4.83 % (3401221)------------------------------
% 23.34/4.83 % (3401227)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=723483743:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2977 on theBenchmark for (2977ds/134Mi)
% 23.34/4.83 % (3401227)Instruction limit reached!
% 23.34/4.83 % (3401227)------------------------------
% 23.34/4.83 % (3401227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401227)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401227)Termination reason: Instruction limit
% 23.34/4.83 % (3401227)Termination phase: Saturation
% 23.34/4.83 % (3401227)Time elapsed: 0.116 s
% 23.34/4.83 % (3401227)Peak memory usage: 93 MB
% 23.34/4.83 % (3401227)Instructions burned: 134 (million)
% 23.34/4.83 % (3401228)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=649159178:st=8:i=592:sd=3:ep=RST:ss=axioms_2975 on theBenchmark for (2975ds/592Mi)
% 23.34/4.83 % (3401228)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401228)------------------------------
% 23.34/4.83 % (3401228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401228)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401228)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401228)Time elapsed: 0.029 s
% 23.34/4.83 % (3401228)Peak memory usage: 89 MB
% 23.34/4.83 % (3401228)Instructions burned: 31 (million)
% 23.34/4.83 % (3401230)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1785827220:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 23.34/4.83 % (3401228)------------------------------
% 23.34/4.83 % (3401228)------------------------------
% 23.34/4.83 % (3401191)First to succeed.
% 23.34/4.83 % (3401233)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=1904489934:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2968 on theBenchmark for (2968ds/125Mi)
% 23.34/4.83 % (3401191)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3401184"
% 23.34/4.83 % (3401233)Refutation not found, incomplete strategy
% 23.34/4.83 % (3401233)------------------------------
% 23.34/4.83 % (3401233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.34/4.83 % (3401233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.34/4.83 % (3401233)CaDiCaL version: 2.1.3
% 23.34/4.83 % (3401233)Termination reason: Refutation not found, incomplete strategy
% 23.34/4.83 % (3401233)Time elapsed: 0.008 s
% 23.34/4.83 % (3401233)Peak memory usage: 89 MB
% 23.34/4.83 % (3401233)Instructions burned: 9 (million)
% 23.34/4.83 % (3401233)------------------------------
% 23.34/4.83 % (3401233)------------------------------
% 23.34/4.83 % (3401191)Refutation found. Thanks to Tanya!
% 23.34/4.83 % SZS status Theorem for theBenchmark
% 23.34/4.83 % SZS output start Proof for theBenchmark
% See solution above
% 27.55/5.10 % (3401191)------------------------------
% 27.55/5.10 % (3401191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.55/5.10 % (3401191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/5.10 % (3401191)CaDiCaL version: 2.1.3
% 27.55/5.10 % (3401191)Termination reason: Refutation
% 27.55/5.10 % (3401191)Time elapsed: 3.072 s
% 27.55/5.10 % (3401191)Peak memory usage: 152 MB
% 27.55/5.10 % (3401191)Instructions burned: 3037 (million)
% 27.55/5.10 % (3401191)------------------------------
% 27.55/5.10 % (3401191)------------------------------
% 27.55/5.10 % (3401184)Success in time 3.817 s
% 27.55/5.10 % Vampire exiting
%------------------------------------------------------------------------------