%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM793+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:04 PM UTC 2026
% Result : Theorem 12.02s 3.02s
% Output : Refutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 47
% Syntax : Number of formulae : 271 ( 44 unt; 29 def)
% Number of atoms : 729 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 796 ( 338 ~; 358 |; 40 &)
% ( 51 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 33 ( 32 usr; 30 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 15 con; 0-2 aty)
% Number of variables : 168 ( 0 sgn 166 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f222,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc557563170_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f226,axiom,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ck)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz87a) ).
fof(f229,axiom,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_cr)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz84) ).
fof(f238,axiom,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dj)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz83) ).
fof(f239,axiom,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dl)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz82) ).
fof(f774,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__236) ).
fof(f775,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dj,X0))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__237) ).
fof(f784,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cr,X0))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__246) ).
fof(f787,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ck,X0))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__249) ).
fof(f790,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__252) ).
fof(f838,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__300) ).
fof(f840,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__302) ).
fof(f841,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__303) ).
fof(f1035,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cj,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__497) ).
fof(f1038,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__500) ).
fof(f1089,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__551) ).
fof(f1090,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(scratc260604120t_more,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__552) ).
fof(f1319,conjecture,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1320,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f1319]) ).
fof(f1321,plain,
~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f1320]) ).
fof(f1338,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc557563170_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f222]) ).
fof(f1339,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc557563170_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1338]) ).
fof(f1414,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f838]) ).
fof(f1416,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) ),
inference(ennf_transformation,[],[f840]) ).
fof(f1417,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1)) ) ),
inference(ennf_transformation,[],[f841]) ).
fof(f1484,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1)) ) ),
inference(ennf_transformation,[],[f1089]) ).
fof(f1485,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1)) ) ),
inference(flattening,[],[f1484]) ).
fof(f1486,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(scratc260604120t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) ),
inference(ennf_transformation,[],[f1090]) ).
fof(f1487,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(scratc260604120t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) ),
inference(flattening,[],[f1486]) ).
fof(f1773,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc557563170_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc557563170_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1339]) ).
fof(f1774,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc557563170_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc557563170_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1)) ) ),
inference(rectify,[],[f1773]) ).
fof(f1775,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc557563170_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc557563170_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1774]) ).
fof(f2030,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0)) ) ),
inference(nnf_transformation,[],[f774]) ).
fof(f2031,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dj,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,X0))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dj,X0)) ) ),
inference(nnf_transformation,[],[f775]) ).
fof(f2040,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cr,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,X0))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cr,X0)) ) ),
inference(nnf_transformation,[],[f784]) ).
fof(f2043,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ck,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ck,X0)) ) ),
inference(nnf_transformation,[],[f787]) ).
fof(f2046,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f790]) ).
fof(f2109,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1)) ) ),
inference(nnf_transformation,[],[f1414]) ).
fof(f2110,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1)) ) ),
inference(flattening,[],[f2109]) ).
fof(f2113,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1)) ) ),
inference(nnf_transformation,[],[f1416]) ).
fof(f2114,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1)) ) ),
inference(flattening,[],[f2113]) ).
fof(f2115,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1)) ) ),
inference(nnf_transformation,[],[f1417]) ).
fof(f2116,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1)) ) ),
inference(flattening,[],[f2115]) ).
fof(f2343,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cj,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cj,X0),X1)) ) ),
inference(nnf_transformation,[],[f1035]) ).
fof(f2346,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc158354487all_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,[],[f1038]) ).
fof(f2421,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1485]) ).
fof(f2422,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2)) ) ),
inference(flattening,[],[f2421]) ).
fof(f2423,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(scratc260604120t_more,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1487]) ).
fof(f2424,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(scratc260604120t_more,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f2423]) ).
fof(f3059,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc557563170_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1775]) ).
fof(f3060,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1775]) ).
fof(f3061,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| scratc557563170_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1775]) ).
fof(f3062,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1775]) ).
fof(f3067,plain,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ck)),
inference(cnf_transformation,[],[f226]) ).
fof(f3070,plain,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_cr)),
inference(cnf_transformation,[],[f229]) ).
fof(f3079,plain,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dj)),
inference(cnf_transformation,[],[f238]) ).
fof(f3080,plain,
pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dl)),
inference(cnf_transformation,[],[f239]) ).
fof(f3880,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dl,X0)) ),
inference(cnf_transformation,[],[f2030]) ).
fof(f3882,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dj,X0)) ),
inference(cnf_transformation,[],[f2031]) ).
fof(f3900,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cr,X0)) ),
inference(cnf_transformation,[],[f2040]) ).
fof(f3906,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ck,X0)) ),
inference(cnf_transformation,[],[f2043]) ).
fof(f3907,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ck,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) ),
inference(cnf_transformation,[],[f2043]) ).
fof(f3913,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f2046]) ).
fof(f4021,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,X0),X1)) ),
inference(cnf_transformation,[],[f2110]) ).
fof(f4027,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,X0),X1)) ),
inference(cnf_transformation,[],[f2114]) ).
fof(f4030,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,X0),X1)) ),
inference(cnf_transformation,[],[f2116]) ).
fof(f4452,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cj,X0),X1)) ),
inference(cnf_transformation,[],[f2343]) ).
fof(f4459,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f2346]) ).
fof(f4586,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2422]) ).
fof(f4591,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(scratc260604120t_more,X0),X1)) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f4592,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(scratc1041149730moreis,X1),X2)) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f4593,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(scratc260604120t_more,X0),X2)) ),
inference(cnf_transformation,[],[f2424]) ).
fof(f5224,plain,
~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f1321]) ).
fof(f5584,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f5586,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f5584]) ).
fof(f5587,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f5224,f5584]) ).
fof(f5588,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f5586,f3060]) ).
fof(f5589,plain,
( scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f5586,f3061]) ).
fof(f5590,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f5586,f3062]) ).
fof(f5603,definition,
( spl29_2
<=> scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f5605,plain,
( scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f5603]) ).
fof(f5606,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f5589,f5584,f5603]) ).
fof(f5608,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f5605,f3059]) ).
fof(f5609,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f5608,f5588]) ).
fof(f5611,definition,
( spl29_3
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f5612,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f5611]) ).
fof(f5613,plain,
( spl29_3
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f5609,f5603,f5584,f5611]) ).
fof(f6595,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dl))
| pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_3 ),
inference(resolution,[],[f5612,f3880]) ).
fof(f6853,plain,
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f6595,f3080]) ).
fof(f6989,definition,
( spl29_4
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f6991,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f6989]) ).
fof(f6992,plain,
( spl29_4
| spl29_1 ),
inference(avatar_split_clause,[],[f5588,f5584,f6989]) ).
fof(f6994,definition,
( spl29_5
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f6996,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_5 ),
inference(avatar_component_clause,[],[f6994]) ).
fof(f6997,plain,
( ~ spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f5590,f5584,f6994]) ).
fof(f6998,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_5 ),
inference(resolution,[],[f6996,f3913]) ).
fof(f7037,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc158354487all_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(f7039,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f7037]) ).
fof(f7040,plain,
( ~ spl29_6
| spl29_5 ),
inference(avatar_split_clause,[],[f6998,f6994,f7037]) ).
fof(f7042,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,[],[f7039,f3060]) ).
fof(f7043,plain,
( scratc557563170_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,[],[f7039,f3061]) ).
fof(f7044,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,[],[f7039,f3062]) ).
fof(f7057,definition,
( spl29_7
<=> scratc557563170_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(f7059,plain,
( scratc557563170_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,[],[f7057]) ).
fof(f7060,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f7043,f7037,f7057]) ).
fof(f7062,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f7059,f3059]) ).
fof(f7063,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f7062,f7042]) ).
fof(f7065,definition,
( spl29_8
<=> ! [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(scratc158354487all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f7066,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_8 ),
inference(avatar_component_clause,[],[f7065]) ).
fof(f7067,plain,
( spl29_8
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f7063,f7057,f7037,f7065]) ).
fof(f8039,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_cr))
| pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_8 ),
inference(resolution,[],[f7066,f3900]) ).
fof(f8317,plain,
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_8 ),
inference(forward_subsumption_resolution,[],[f8039,f3070]) ).
fof(f8443,definition,
( spl29_9
<=> 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_9])],[avatar_definition]) ).
fof(f8445,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_9 ),
inference(avatar_component_clause,[],[f8443]) ).
fof(f8446,plain,
( ~ spl29_9
| spl29_6 ),
inference(avatar_split_clause,[],[f7044,f7037,f8443]) ).
fof(f8447,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_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(resolution,[],[f8445,f4459]) ).
fof(f8494,definition,
( spl29_10
<=> pp(aa_fun171081125l_bool(scratc158354487all_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_10])],[avatar_definition]) ).
fof(f8496,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_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_10 ),
inference(avatar_component_clause,[],[f8494]) ).
fof(f8497,plain,
( ~ spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f8447,f8443,f8494]) ).
fof(f8499,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_10 ),
inference(resolution,[],[f8496,f3060]) ).
fof(f8500,plain,
( scratc557563170_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(resolution,[],[f8496,f3061]) ).
fof(f8501,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_10 ),
inference(resolution,[],[f8496,f3062]) ).
fof(f8514,definition,
( spl29_11
<=> scratc557563170_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_11])],[avatar_definition]) ).
fof(f8516,plain,
( scratc557563170_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_11 ),
inference(avatar_component_clause,[],[f8514]) ).
fof(f8517,plain,
( spl29_11
| spl29_10 ),
inference(avatar_split_clause,[],[f8500,f8494,f8514]) ).
fof(f8519,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,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)))))))
| ~ 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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(resolution,[],[f8516,f3059]) ).
fof(f8520,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| spl29_10
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f8519,f8499]) ).
fof(f8522,definition,
( spl29_12
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,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(scratc158354487all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f8523,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,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(scratc158354487all_of(aTP_Lamm_a),X0)) )
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f8522]) ).
fof(f8524,plain,
( spl29_12
| spl29_10
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f8520,f8514,f8494,f8522]) ).
fof(f8526,definition,
( spl29_13
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f8528,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f8526]) ).
fof(f8529,plain,
( spl29_13
| spl29_6 ),
inference(avatar_split_clause,[],[f7042,f7037,f8526]) ).
fof(f9687,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_ck))
| pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,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_12 ),
inference(resolution,[],[f8523,f3906]) ).
fof(f9699,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aTP_Lamm_dj))
| pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,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_12 ),
inference(resolution,[],[f8523,f3882]) ).
fof(f9959,plain,
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,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_12 ),
inference(forward_subsumption_resolution,[],[f9699,f3079]) ).
fof(f9971,plain,
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,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_12 ),
inference(forward_subsumption_resolution,[],[f9687,f3067]) ).
fof(f10098,definition,
( spl29_17
<=> 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_17])],[avatar_definition]) ).
fof(f10100,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_17 ),
inference(avatar_component_clause,[],[f10098]) ).
fof(f10101,plain,
( ~ spl29_17
| spl29_10 ),
inference(avatar_split_clause,[],[f8501,f8494,f10098]) ).
fof(f10102,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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,[],[f10100,f4591]) ).
fof(f10103,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,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_17 ),
inference(resolution,[],[f10100,f4592]) ).
fof(f10104,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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,[],[f10100,f4593]) ).
fof(f10158,definition,
( spl29_19
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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(f10160,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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,[],[f10158]) ).
fof(f10161,plain,
( ~ spl29_19
| spl29_17 ),
inference(avatar_split_clause,[],[f10104,f10098,f10158]) ).
fof(f10164,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_19 ),
inference(resolution,[],[f10160,f4030]) ).
fof(f10304,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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_20])],[avatar_definition]) ).
fof(f10306,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc260604120t_more,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(avatar_component_clause,[],[f10304]) ).
fof(f10307,plain,
( spl29_20
| spl29_17 ),
inference(avatar_split_clause,[],[f10102,f10098,f10304]) ).
fof(f10309,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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_dk,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,[],[f10306,f4027]) ).
fof(f10458,definition,
( spl29_24
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,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_24])],[avatar_definition]) ).
fof(f10460,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1041149730moreis,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_24 ),
inference(avatar_component_clause,[],[f10458]) ).
fof(f10461,plain,
( spl29_24
| spl29_17 ),
inference(avatar_split_clause,[],[f10103,f10098,f10458]) ).
fof(f10462,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,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)))))),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_cq,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_24 ),
inference(resolution,[],[f10460,f4021]) ).
fof(f10821,definition,
( spl29_34
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,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_34])],[avatar_definition]) ).
fof(f10823,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cq,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_34 ),
inference(avatar_component_clause,[],[f10821]) ).
fof(f10825,definition,
( spl29_35
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,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)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
fof(f10827,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,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)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ spl29_35 ),
inference(avatar_component_clause,[],[f10825]) ).
fof(f10828,plain,
( ~ spl29_34
| spl29_35
| ~ spl29_24 ),
inference(avatar_split_clause,[],[f10462,f10458,f10825,f10821]) ).
fof(f10837,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_12
| spl29_34 ),
inference(resolution,[],[f10823,f8523]) ).
fof(f10876,plain,
( $false
| ~ spl29_8
| ~ spl29_12
| spl29_34 ),
inference(forward_subsumption_resolution,[],[f10837,f8317]) ).
fof(f10877,plain,
( ~ spl29_8
| ~ spl29_12
| spl29_34 ),
inference(avatar_contradiction_clause,[],[f10876]) ).
fof(f10935,definition,
( spl29_37
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_37])],[avatar_definition]) ).
fof(f10937,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_di,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_37 ),
inference(avatar_component_clause,[],[f10935]) ).
fof(f10939,definition,
( spl29_38
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).
fof(f10941,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_38 ),
inference(avatar_component_clause,[],[f10939]) ).
fof(f10942,plain,
( ~ spl29_37
| ~ spl29_38
| spl29_19 ),
inference(avatar_split_clause,[],[f10164,f10158,f10939,f10935]) ).
fof(f10951,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_di,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_3
| spl29_37 ),
inference(resolution,[],[f10937,f5612]) ).
fof(f10990,plain,
( $false
| ~ spl29_3
| ~ spl29_12
| spl29_37 ),
inference(forward_subsumption_resolution,[],[f10951,f9959]) ).
fof(f10991,plain,
( ~ spl29_3
| ~ spl29_12
| spl29_37 ),
inference(avatar_contradiction_clause,[],[f10990]) ).
fof(f11107,definition,
( spl29_41
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,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_41])],[avatar_definition]) ).
fof(f11109,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dk,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_41 ),
inference(avatar_component_clause,[],[f11107]) ).
fof(f11111,definition,
( spl29_42
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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_42])],[avatar_definition]) ).
fof(f11113,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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_42 ),
inference(avatar_component_clause,[],[f11111]) ).
fof(f11114,plain,
( ~ spl29_41
| spl29_42
| ~ spl29_20 ),
inference(avatar_split_clause,[],[f10309,f10304,f11111,f11107]) ).
fof(f11123,plain,
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dk,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_8
| spl29_41 ),
inference(resolution,[],[f11109,f7066]) ).
fof(f11162,plain,
( $false
| ~ spl29_3
| ~ spl29_8
| spl29_41 ),
inference(forward_subsumption_resolution,[],[f11123,f6853]) ).
fof(f11163,plain,
( ~ spl29_3
| ~ spl29_8
| spl29_41 ),
inference(avatar_contradiction_clause,[],[f11162]) ).
fof(f11169,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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_ci(X0),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_42 ),
inference(resolution,[],[f11113,f4586]) ).
fof(f13945,definition,
( spl29_134
<=> pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,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_134])],[avatar_definition]) ).
fof(f13947,plain,
( pp(aa_fun171081125l_bool(scratc158354487all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cj,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_134 ),
inference(avatar_component_clause,[],[f13945]) ).
fof(f13948,plain,
( spl29_134
| ~ spl29_12 ),
inference(avatar_split_clause,[],[f9971,f8522,f13945]) ).
fof(f13949,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ck,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_134 ),
inference(resolution,[],[f13947,f3907]) ).
fof(f16268,definition,
( spl29_202
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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_ci(X0),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_202])],[avatar_definition]) ).
fof(f16269,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ci(X0),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(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_202 ),
inference(avatar_component_clause,[],[f16268]) ).
fof(f16270,plain,
( spl29_202
| ~ spl29_42 ),
inference(avatar_split_clause,[],[f11169,f11111,f16268]) ).
fof(f16752,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_202 ),
inference(resolution,[],[f16269,f3059]) ).
fof(f16788,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_4
| ~ spl29_202 ),
inference(forward_subsumption_resolution,[],[f16752,f6991]) ).
fof(f16791,definition,
( spl29_222
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_222])],[avatar_definition]) ).
fof(f16792,plain,
( ! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ci(X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_222 ),
inference(avatar_component_clause,[],[f16791]) ).
fof(f16793,plain,
( spl29_222
| ~ spl29_4
| ~ spl29_202 ),
inference(avatar_split_clause,[],[f16788,f16268,f6989,f16791]) ).
fof(f16794,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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_cj,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_222 ),
inference(resolution,[],[f16792,f4452]) ).
fof(f16812,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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_cj,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_2
| ~ spl29_222 ),
inference(forward_subsumption_resolution,[],[f16794,f5605]) ).
fof(f16814,definition,
( spl29_223
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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_cj,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_223])],[avatar_definition]) ).
fof(f16815,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cj,X0),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(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_223 ),
inference(avatar_component_clause,[],[f16814]) ).
fof(f16816,plain,
( spl29_223
| ~ spl29_2
| ~ spl29_222 ),
inference(avatar_split_clause,[],[f16812,f16791,f5603,f16814]) ).
fof(f16828,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) )
| ~ spl29_223 ),
inference(resolution,[],[f16815,f3059]) ).
fof(f16863,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) )
| ~ spl29_13
| ~ spl29_223 ),
inference(forward_subsumption_resolution,[],[f16828,f8528]) ).
fof(f17959,definition,
( spl29_249
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_249])],[avatar_definition]) ).
fof(f17960,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc907166118lessis,X0),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(scratc1544951132t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cj,X0))) )
| ~ spl29_249 ),
inference(avatar_component_clause,[],[f17959]) ).
fof(f17961,plain,
( spl29_249
| ~ spl29_13
| ~ spl29_223 ),
inference(avatar_split_clause,[],[f16863,f16814,f8526,f17959]) ).
fof(f17962,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1544951132t_less,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)))))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cj,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_35
| ~ spl29_249 ),
inference(resolution,[],[f17960,f10827]) ).
fof(f18017,plain,
( ! [X0] :
( ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cj,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_35
| spl29_38
| ~ spl29_249 ),
inference(forward_subsumption_resolution,[],[f17962,f10941]) ).
fof(f18020,definition,
( spl29_250
<=> ! [X0] :
( ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cj,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_250])],[avatar_definition]) ).
fof(f18021,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc158354487all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cj,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))))))))
| ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0) )
| ~ spl29_250 ),
inference(avatar_component_clause,[],[f18020]) ).
fof(f18022,plain,
( spl29_250
| ~ spl29_35
| spl29_38
| ~ spl29_249 ),
inference(avatar_split_clause,[],[f18017,f17959,f10939,f10825,f18020]) ).
fof(f18024,plain,
( ~ scratc557563170_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ck,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_250 ),
inference(resolution,[],[f18021,f3906]) ).
fof(f18043,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ck,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_7
| ~ spl29_250 ),
inference(forward_subsumption_resolution,[],[f18024,f7059]) ).
fof(f18046,plain,
( $false
| ~ spl29_7
| ~ spl29_134
| ~ spl29_250 ),
inference(forward_subsumption_resolution,[],[f18043,f13949]) ).
fof(f18047,plain,
( ~ spl29_7
| ~ spl29_134
| ~ spl29_250 ),
inference(avatar_contradiction_clause,[],[f18046]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f5587]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f5606]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_2
| spl29_3 ),
inference(sat_conversion,[],[f5613]) ).
cnf(s4,plain,
( spl29_1
| spl29_4 ),
inference(sat_conversion,[],[f6992]) ).
cnf(s5,plain,
( spl29_1
| ~ spl29_5 ),
inference(sat_conversion,[],[f6997]) ).
cnf(s6,plain,
( spl29_5
| ~ spl29_6 ),
inference(sat_conversion,[],[f7040]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f7060]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_7
| spl29_8 ),
inference(sat_conversion,[],[f7067]) ).
cnf(s9,plain,
( spl29_6
| ~ spl29_9 ),
inference(sat_conversion,[],[f8446]) ).
cnf(s10,plain,
( spl29_9
| ~ spl29_10 ),
inference(sat_conversion,[],[f8497]) ).
cnf(s11,plain,
( spl29_10
| spl29_11 ),
inference(sat_conversion,[],[f8517]) ).
cnf(s12,plain,
( spl29_10
| ~ spl29_11
| spl29_12 ),
inference(sat_conversion,[],[f8524]) ).
cnf(s13,plain,
( spl29_6
| spl29_13 ),
inference(sat_conversion,[],[f8529]) ).
cnf(s17,plain,
( spl29_10
| ~ spl29_17 ),
inference(sat_conversion,[],[f10101]) ).
cnf(s19,plain,
( spl29_17
| ~ spl29_19 ),
inference(sat_conversion,[],[f10161]) ).
cnf(s20,plain,
( spl29_17
| spl29_20 ),
inference(sat_conversion,[],[f10307]) ).
cnf(s24,plain,
( spl29_17
| spl29_24 ),
inference(sat_conversion,[],[f10461]) ).
cnf(s34,plain,
( ~ spl29_24
| ~ spl29_34
| spl29_35 ),
inference(sat_conversion,[],[f10828]) ).
cnf(s35,plain,
( ~ spl29_8
| ~ spl29_12
| spl29_34 ),
inference(sat_conversion,[],[f10877]) ).
cnf(s37,plain,
( spl29_19
| ~ spl29_37
| ~ spl29_38 ),
inference(sat_conversion,[],[f10942]) ).
cnf(s38,plain,
( ~ spl29_3
| ~ spl29_12
| spl29_37 ),
inference(sat_conversion,[],[f10991]) ).
cnf(s41,plain,
( ~ spl29_20
| ~ spl29_41
| spl29_42 ),
inference(sat_conversion,[],[f11114]) ).
cnf(s42,plain,
( ~ spl29_3
| ~ spl29_8
| spl29_41 ),
inference(sat_conversion,[],[f11163]) ).
cnf(s139,plain,
( ~ spl29_12
| spl29_134 ),
inference(sat_conversion,[],[f13948]) ).
cnf(s204,plain,
( ~ spl29_42
| spl29_202 ),
inference(sat_conversion,[],[f16270]) ).
cnf(s224,plain,
( ~ spl29_4
| ~ spl29_202
| spl29_222 ),
inference(sat_conversion,[],[f16793]) ).
cnf(s225,plain,
( ~ spl29_2
| ~ spl29_222
| spl29_223 ),
inference(sat_conversion,[],[f16816]) ).
cnf(s253,plain,
( ~ spl29_13
| ~ spl29_223
| spl29_249 ),
inference(sat_conversion,[],[f17961]) ).
cnf(s254,plain,
( ~ spl29_35
| spl29_38
| ~ spl29_249
| spl29_250 ),
inference(sat_conversion,[],[f18022]) ).
cnf(s256,plain,
( ~ spl29_7
| ~ spl29_134
| ~ spl29_250 ),
inference(sat_conversion,[],[f18047]) ).
cnf(s257,plain,
~ spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s258,plain,
spl29_4,
inference(rat,[],[s4,s1]) ).
cnf(s259,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s264,plain,
~ spl29_6,
inference(rat,[],[s6,s257]) ).
cnf(s269,plain,
spl29_3,
inference(rat,[],[s3,s1,s259]) ).
cnf(s272,plain,
spl29_13,
inference(rat,[],[s13,s264]) ).
cnf(s273,plain,
~ spl29_9,
inference(rat,[],[s9,s264]) ).
cnf(s274,plain,
spl29_7,
inference(rat,[],[s7,s264]) ).
cnf(s305,plain,
~ spl29_10,
inference(rat,[],[s10,s273]) ).
cnf(s306,plain,
spl29_8,
inference(rat,[],[s8,s264,s274]) ).
cnf(s308,plain,
~ spl29_17,
inference(rat,[],[s17,s305]) ).
cnf(s310,plain,
spl29_11,
inference(rat,[],[s11,s305]) ).
cnf(s334,plain,
spl29_41,
inference(rat,[],[s42,s269,s306]) ).
cnf(s338,plain,
spl29_24,
inference(rat,[],[s24,s308]) ).
cnf(s339,plain,
spl29_20,
inference(rat,[],[s20,s308]) ).
cnf(s340,plain,
~ spl29_19,
inference(rat,[],[s19,s308]) ).
cnf(s343,plain,
spl29_12,
inference(rat,[],[s12,s305,s310]) ).
cnf(s374,plain,
spl29_42,
inference(rat,[],[s41,s334,s339]) ).
cnf(s399,plain,
spl29_134,
inference(rat,[],[s139,s343]) ).
cnf(s409,plain,
spl29_37,
inference(rat,[],[s38,s269,s343]) ).
cnf(s410,plain,
spl29_34,
inference(rat,[],[s35,s306,s343]) ).
cnf(s418,plain,
spl29_202,
inference(rat,[],[s204,s374]) ).
cnf(s423,plain,
~ spl29_250,
inference(rat,[],[s256,s274,s399]) ).
cnf(s424,plain,
~ spl29_38,
inference(rat,[],[s37,s340,s409]) ).
cnf(s425,plain,
spl29_35,
inference(rat,[],[s34,s338,s410]) ).
cnf(s430,plain,
spl29_222,
inference(rat,[],[s224,s258,s418]) ).
cnf(s440,plain,
~ spl29_249,
inference(rat,[],[s254,s423,s424,s425]) ).
cnf(s446,plain,
spl29_223,
inference(rat,[],[s225,s259,s430]) ).
cnf(s455,plain,
$false,
inference(rat,[],[s253,s272,s440,s446]) ).
fof(f18048,plain,
$false,
inference(avatar_sat_refutation,[],[s455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM793+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 21:26:09 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.33 Running first-order theorem proving
% 0.08/0.33 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.63/1.86 % (2764242)Detected formulas, will run a generic FOF schedule.
% 7.63/1.86 % (2764248)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=2563439924:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.63/1.86 % (2764247)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=1301679857:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.63/1.86 % (2764251)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2381893462:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.63/1.86 % (2764253)dis-21_1_sil=8000:lcm=predicate:random_seed=3704502331: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)
% 7.63/1.86 % (2764252)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3997320674:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.63/1.86 % (2764250)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1647574564:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.63/1.86 % (2764249)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=1806358715:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.63/1.86 % (2764250)Refutation not found, incomplete strategy
% 7.63/1.86 % (2764250)------------------------------
% 7.63/1.86 % (2764250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/1.86 % (2764250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.63/1.86 % (2764250)CaDiCaL version: 2.1.3
% 7.63/1.86 % (2764250)Termination reason: Refutation not found, incomplete strategy
% 7.63/1.86 % (2764250)Time elapsed: 0.003 s
% 7.63/1.86 % (2764250)Peak memory usage: 89 MB
% 7.63/1.86 % (2764250)Instructions burned: 6 (million)
% 7.63/1.86 % (2764251)Refutation not found, incomplete strategy
% 7.63/1.86 % (2764251)------------------------------
% 7.63/1.86 % (2764251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/1.86 % (2764251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.63/1.86 % (2764251)CaDiCaL version: 2.1.3
% 7.63/1.86 % (2764251)Termination reason: Refutation not found, incomplete strategy
% 7.63/1.86 % (2764251)Time elapsed: 0.004 s
% 7.63/1.86 % (2764251)Peak memory usage: 88 MB
% 7.63/1.86 % (2764251)Instructions burned: 7 (million)
% 7.63/1.86 % (2764253)Instruction limit reached!
% 7.63/1.86 % (2764253)------------------------------
% 7.63/1.86 % (2764253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/1.86 % (2764253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.63/1.86 % (2764253)CaDiCaL version: 2.1.3
% 7.63/1.86 % (2764253)Termination reason: Instruction limit
% 7.63/1.86 % (2764253)Termination phase: Saturation
% 7.63/1.86 % (2764253)Time elapsed: 0.030 s
% 7.63/1.86 % (2764253)Peak memory usage: 89 MB
% 7.63/1.86 % (2764253)Instructions burned: 129 (million)
% 7.63/1.86 % (2764252)Instruction limit reached!
% 7.63/1.86 % (2764252)------------------------------
% 7.63/1.86 % (2764252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/1.86 % (2764252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.63/1.86 % (2764252)CaDiCaL version: 2.1.3
% 7.63/1.86 % (2764252)Termination reason: Instruction limit
% 7.63/1.86 % (2764252)Termination phase: Saturation
% 7.63/1.86 % (2764252)Time elapsed: 0.033 s
% 7.63/1.86 % (2764252)Peak memory usage: 90 MB
% 7.63/1.86 % (2764252)Instructions burned: 140 (million)
% 7.63/1.86 % (2764251)------------------------------
% 7.63/1.86 % (2764251)------------------------------
% 7.63/1.86 % (2764250)------------------------------
% 7.63/1.86 % (2764250)------------------------------
% 7.63/1.86 % (2764262)lrs+10_1_sil=32000:urr=on:br=off:random_seed=607733590:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 7.63/1.86 % (2764261)lrs+10_1_sil=8000:sp=occurrence:random_seed=3995030600:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 7.63/1.86 % (2764261)Refutation not found, incomplete strategy
% 7.63/1.86 % (2764261)------------------------------
% 7.63/1.86 % (2764261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/1.86 % (2764261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764261)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764261)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.60 % (2764261)Time elapsed: 0.003 s
% 14.29/2.60 % (2764261)Peak memory usage: 89 MB
% 14.29/2.60 % (2764261)Instructions burned: 6 (million)
% 14.29/2.60 % (2764262)Refutation not found, incomplete strategy
% 14.29/2.60 % (2764262)------------------------------
% 14.29/2.60 % (2764262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.29/2.60 % (2764262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764262)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764262)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.60 % (2764262)Time elapsed: 0.005 s
% 14.29/2.60 % (2764262)Peak memory usage: 89 MB
% 14.29/2.60 % (2764262)Instructions burned: 21 (million)
% 14.29/2.60 % (2764265)lrs+1011_1_sil=32000:sp=occurrence:random_seed=750947938:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 14.29/2.60 % (2764266)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=467500015:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 14.29/2.60 % (2764265)Refutation not found, incomplete strategy
% 14.29/2.60 % (2764265)------------------------------
% 14.29/2.60 % (2764265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.29/2.60 % (2764265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764265)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764265)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.60 % (2764265)Time elapsed: 0.004 s
% 14.29/2.60 % (2764265)Peak memory usage: 90 MB
% 14.29/2.60 % (2764265)Instructions burned: 8 (million)
% 14.29/2.60 % (2764261)------------------------------
% 14.29/2.60 % (2764261)------------------------------
% 14.29/2.60 % (2764262)------------------------------
% 14.29/2.60 % (2764262)------------------------------
% 14.29/2.60 % (2764266)Instruction limit reached!
% 14.29/2.60 % (2764266)------------------------------
% 14.29/2.60 % (2764266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.29/2.60 % (2764266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764266)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764266)Termination reason: Instruction limit
% 14.29/2.60 % (2764266)Termination phase: Saturation
% 14.29/2.60 % (2764266)Time elapsed: 0.073 s
% 14.29/2.60 % (2764266)Peak memory usage: 95 MB
% 14.29/2.60 % (2764266)Instructions burned: 250 (million)
% 14.29/2.60 % (2764269)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2077288757:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 14.29/2.60 % (2764270)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1216782670:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 14.29/2.60 % (2764265)------------------------------
% 14.29/2.60 % (2764265)------------------------------
% 14.29/2.60 % (2764269)Refutation not found, incomplete strategy
% 14.29/2.60 % (2764269)------------------------------
% 14.29/2.60 % (2764269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.29/2.60 % (2764269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764269)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764269)Termination reason: Refutation not found, incomplete strategy
% 14.29/2.60 % (2764269)Time elapsed: 0.005 s
% 14.29/2.60 % (2764269)Peak memory usage: 89 MB
% 14.29/2.60 % (2764269)Instructions burned: 13 (million)
% 14.29/2.60 % (2764271)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=615798138:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 14.29/2.60 % (2764271)Instruction limit reached!
% 14.29/2.60 % (2764271)------------------------------
% 14.29/2.60 % (2764271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.29/2.60 % (2764271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.60 % (2764271)CaDiCaL version: 2.1.3
% 14.29/2.60 % (2764271)Termination reason: Instruction limit
% 14.29/2.60 % (2764271)Termination phase: Saturation
% 14.29/2.60 % (2764271)Time elapsed: 0.029 s
% 14.29/2.60 % (2764271)Peak memory usage: 90 MB
% 14.29/2.60 % (2764271)Instructions burned: 114 (million)
% 14.29/2.60 % (2764274)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3286257286:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 15.98/3.02 % (2764269)------------------------------
% 15.98/3.02 % (2764269)------------------------------
% 15.98/3.02 % (2764274)Instruction limit reached!
% 15.98/3.02 % (2764274)------------------------------
% 15.98/3.02 % (2764274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.98/3.02 % (2764274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.98/3.02 % (2764274)CaDiCaL version: 2.1.3
% 15.98/3.02 % (2764274)Termination reason: Instruction limit
% 15.98/3.02 % (2764274)Termination phase: Property scanning
% 15.98/3.02 % (2764274)Time elapsed: 0.031 s
% 15.98/3.02 % (2764274)Peak memory usage: 89 MB
% 15.98/3.02 % (2764274)Instructions burned: 131 (million)
% 15.98/3.02 % (2764276)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3375233140:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 15.98/3.02 % (2764276)Instruction limit reached!
% 15.98/3.02 % (2764276)------------------------------
% 15.98/3.02 % (2764276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.98/3.02 % (2764276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.98/3.02 % (2764276)CaDiCaL version: 2.1.3
% 15.98/3.02 % (2764276)Termination reason: Instruction limit
% 15.98/3.02 % (2764276)Termination phase: Saturation
% 15.98/3.02 % (2764276)Time elapsed: 0.032 s
% 15.98/3.02 % (2764276)Peak memory usage: 90 MB
% 15.98/3.02 % (2764276)Instructions burned: 117 (million)
% 15.98/3.02 % (2764279)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=934511403:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 15.98/3.02 % (2764278)lrs+10_1_sil=8000:sp=occurrence:random_seed=964336089:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 15.98/3.02 % (2764279)Refutation not found, incomplete strategy
% 15.98/3.02 % (2764279)------------------------------
% 15.98/3.02 % (2764279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.98/3.02 % (2764279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.98/3.02 % (2764279)CaDiCaL version: 2.1.3
% 15.98/3.02 % (2764279)Termination reason: Refutation not found, incomplete strategy
% 15.98/3.02 % (2764279)Time elapsed: 0.052 s
% 12.02/3.02 % (2764279)Peak memory usage: 93 MB
% 12.02/3.02 % (2764279)Instructions burned: 196 (million)
% 12.02/3.02 % (2764281)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2334925496:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 12.02/3.02 % (2764279)------------------------------
% 12.02/3.02 % (2764279)------------------------------
% 12.02/3.02 % (2764278)Instruction limit reached!
% 12.02/3.02 % (2764278)------------------------------
% 12.02/3.02 % (2764278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764278)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764278)Termination reason: Instruction limit
% 12.02/3.02 % (2764278)Termination phase: Saturation
% 12.02/3.02 % (2764278)Time elapsed: 0.304 s
% 12.02/3.02 % (2764278)Peak memory usage: 101 MB
% 12.02/3.02 % (2764278)Instructions burned: 907 (million)
% 12.02/3.02 % (2764285)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1778319610:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 12.02/3.02 % (2764285)Instruction limit reached!
% 12.02/3.02 % (2764285)------------------------------
% 12.02/3.02 % (2764285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764285)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764285)Termination reason: Instruction limit
% 12.02/3.02 % (2764285)Termination phase: Saturation
% 12.02/3.02 % (2764285)Time elapsed: 0.034 s
% 12.02/3.02 % (2764285)Peak memory usage: 91 MB
% 12.02/3.02 % (2764285)Instructions burned: 134 (million)
% 12.02/3.02 % (2764286)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2715057459:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 12.02/3.02 % (2764286)Refutation not found, incomplete strategy
% 12.02/3.02 % (2764286)------------------------------
% 12.02/3.02 % (2764286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764286)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764286)Termination reason: Refutation not found, incomplete strategy
% 12.02/3.02 % (2764286)Time elapsed: 0.012 s
% 12.02/3.02 % (2764286)Peak memory usage: 90 MB
% 12.02/3.02 % (2764286)Instructions burned: 42 (million)
% 12.02/3.02 % (2764270)Instruction limit reached!
% 12.02/3.02 % (2764270)------------------------------
% 12.02/3.02 % (2764270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764270)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764270)Termination reason: Instruction limit
% 12.02/3.02 % (2764270)Termination phase: Saturation
% 12.02/3.02 % (2764270)Time elapsed: 0.774 s
% 12.02/3.02 % (2764270)Peak memory usage: 164 MB
% 12.02/3.02 % (2764270)Instructions burned: 2350 (million)
% 12.02/3.02 % (2764288)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2832800576:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 12.02/3.02 % (2764286)------------------------------
% 12.02/3.02 % (2764286)------------------------------
% 12.02/3.02 % (2764290)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=2271680136:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/125Mi)
% 12.02/3.02 % (2764290)Refutation not found, incomplete strategy
% 12.02/3.02 % (2764290)------------------------------
% 12.02/3.02 % (2764290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764290)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764290)Termination reason: Refutation not found, incomplete strategy
% 12.02/3.02 % (2764290)Time elapsed: 0.008 s
% 12.02/3.02 % (2764290)Peak memory usage: 90 MB
% 12.02/3.02 % (2764290)Instructions burned: 28 (million)
% 12.02/3.02 % (2764292)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2132296981:i=134:gtgl=5:slsql=off:gtg=exists_sym_2985 on theBenchmark for (2985ds/134Mi)
% 12.02/3.02 % (2764292)Instruction limit reached!
% 12.02/3.02 % (2764292)------------------------------
% 12.02/3.02 % (2764292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764292)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764292)Termination reason: Instruction limit
% 12.02/3.02 % (2764292)Termination phase: Twee Goal Transformation
% 12.02/3.02 % (2764292)Time elapsed: 0.035 s
% 12.02/3.02 % (2764292)Peak memory usage: 91 MB
% 12.02/3.02 % (2764292)Instructions burned: 137 (million)
% 12.02/3.02 % (2764290)------------------------------
% 12.02/3.02 % (2764290)------------------------------
% 12.02/3.02 % (2764295)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4112494118:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/141Mi)
% 12.02/3.02 % (2764295)Refutation not found, incomplete strategy
% 12.02/3.02 % (2764295)------------------------------
% 12.02/3.02 % (2764295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764295)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764295)Termination reason: Refutation not found, incomplete strategy
% 12.02/3.02 % (2764295)Time elapsed: 0.003 s
% 12.02/3.02 % (2764295)Peak memory usage: 89 MB
% 12.02/3.02 % (2764295)Instructions burned: 6 (million)
% 12.02/3.02 % (2764296)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3919387153:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2983 on theBenchmark for (2983ds/431Mi)
% 12.02/3.02 % (2764296)Refutation not found, incomplete strategy
% 12.02/3.02 % (2764296)------------------------------
% 12.02/3.02 % (2764296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764296)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764296)Termination reason: Refutation not found, incomplete strategy
% 12.02/3.02 % (2764296)Time elapsed: 0.004 s
% 12.02/3.02 % (2764296)Peak memory usage: 90 MB
% 12.02/3.02 % (2764296)Instructions burned: 9 (million)
% 12.02/3.02 % (2764295)------------------------------
% 12.02/3.02 % (2764295)------------------------------
% 12.02/3.02 % (2764296)------------------------------
% 12.02/3.02 % (2764296)------------------------------
% 12.02/3.02 % (2764299)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=1983893589:i=6060:aac=none:ins=25_2980 on theBenchmark for (2980ds/6060Mi)
% 12.02/3.02 % (2764300)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=208692354:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2980 on theBenchmark for (2980ds/150Mi)
% 12.02/3.02 % (2764300)Instruction limit reached!
% 12.02/3.02 % (2764300)------------------------------
% 12.02/3.02 % (2764300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.02/3.02 % (2764300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.02/3.02 % (2764300)CaDiCaL version: 2.1.3
% 12.02/3.02 % (2764300)Termination reason: Instruction limit
% 12.02/3.02 % (2764300)Termination phase: Saturation
% 12.02/3.02 % (2764300)Time elapsed: 0.037 s
% 12.02/3.02 % (2764300)Peak memory usage: 91 MB
% 12.02/3.02 % (2764300)Instructions burned: 153 (million)
% 12.02/3.02 % (2764303)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=814604061:i=14155:bd=all_2978 on theBenchmark for (2978ds/14155Mi)
% 12.02/3.02 % (2764249)First to succeed.
% 12.02/3.02 % (2764249)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2764242"
% 12.02/3.02 % (2764249)Refutation found. Thanks to Tanya!
% 12.02/3.02 % SZS status Theorem for theBenchmark
% 12.02/3.02 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/3.12 % (2764249)------------------------------
% 0.08/3.12 % (2764249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.08/3.12 % (2764249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/3.12 % (2764249)CaDiCaL version: 2.1.3
% 0.08/3.12 % (2764249)Termination reason: Refutation
% 0.08/3.12 % (2764249)Time elapsed: 2.151 s
% 0.08/3.12 % (2764249)Peak memory usage: 189 MB
% 0.08/3.12 % (2764249)Instructions burned: 6520 (million)
% 0.08/3.12 % (2764249)------------------------------
% 0.08/3.12 % (2764249)------------------------------
% 0.08/3.12 % (2764242)Success in time 2.487 s
% 0.08/3.12 % Vampire exiting
%------------------------------------------------------------------------------