%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM666+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 : n014.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:20 PM UTC 2026
% Result : Theorem 24.53s 4.36s
% Output : Refutation 25.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 42
% Syntax : Number of formulae : 246 ( 39 unt; 28 def)
% Number of atoms : 636 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 682 ( 292 ~; 305 |; 32 &)
% ( 46 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 32 ( 31 usr; 29 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 154 ( 0 sgn 152 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f29,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc984285568_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f151,axiom,
pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_bz)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz16a) ).
fof(f162,axiom,
pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_cw)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz13) ).
fof(f289,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cw,X0))
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__34) ).
fof(f300,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bz,X0))
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__45) ).
fof(f303,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__48) ).
fof(f324,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__69) ).
fof(f350,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_by,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__95) ).
fof(f353,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__98) ).
fof(f370,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(scratc1388546348_29_ii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__115) ).
fof(f372,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__117) ).
fof(f432,conjecture,
pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f433,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f432]) ).
fof(f434,plain,
~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f433]) ).
fof(f451,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc984285568_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f452,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc984285568_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f451]) ).
fof(f516,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f324]) ).
fof(f532,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(scratc1388546348_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ) ),
inference(ennf_transformation,[],[f370]) ).
fof(f533,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(scratc1388546348_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ) ),
inference(flattening,[],[f532]) ).
fof(f536,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1)) ) ),
inference(ennf_transformation,[],[f372]) ).
fof(f537,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1)) ) ),
inference(flattening,[],[f536]) ).
fof(f565,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f566,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f629,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc984285568_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc984285568_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f452]) ).
fof(f630,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc984285568_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc984285568_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1)) ) ),
inference(rectify,[],[f629]) ).
fof(f631,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc984285568_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc984285568_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f630]) ).
fof(f684,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cw,X0))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,X0))) )
& ( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cw,X0)) ) ),
inference(nnf_transformation,[],[f289]) ).
fof(f695,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bz,X0))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) )
& ( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bz,X0)) ) ),
inference(nnf_transformation,[],[f300]) ).
fof(f698,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f303]) ).
fof(f725,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1)) ) ),
inference(nnf_transformation,[],[f516]) ).
fof(f726,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1)) ) ),
inference(flattening,[],[f725]) ).
fof(f760,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_by,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_by,X0),X1)) ) ),
inference(nnf_transformation,[],[f350]) ).
fof(f763,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc271589209all_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,[],[f353]) ).
fof(f781,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(scratc1388546348_29_ii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f533]) ).
fof(f782,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(scratc1388546348_29_ii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f781]) ).
fof(f785,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f537]) ).
fof(f786,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2)) ) ),
inference(flattening,[],[f785]) ).
fof(f870,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f565]) ).
fof(f871,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f565]) ).
fof(f872,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f566]) ).
fof(f873,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(X0),X1))) ),
inference(cnf_transformation,[],[f566]) ).
fof(f1058,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc984285568_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1)) ),
inference(cnf_transformation,[],[f631]) ).
fof(f1059,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f631]) ).
fof(f1060,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| scratc984285568_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f631]) ).
fof(f1061,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f631]) ).
fof(f1066,plain,
pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_bz)),
inference(cnf_transformation,[],[f151]) ).
fof(f1077,plain,
pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_cw)),
inference(cnf_transformation,[],[f162]) ).
fof(f1267,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cw,X0)) ),
inference(cnf_transformation,[],[f684]) ).
fof(f1289,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bz,X0)) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1290,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bz,X0))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1296,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f698]) ).
fof(f1341,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,X0),X1)) ),
inference(cnf_transformation,[],[f726]) ).
fof(f1402,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_by,X0),X1)) ),
inference(cnf_transformation,[],[f760]) ).
fof(f1409,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f763]) ).
fof(f1444,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(scratc1388546348_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f782]) ).
fof(f1445,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(scratc2056971326moreis,X1),X2)) ),
inference(cnf_transformation,[],[f782]) ).
fof(f1446,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(scratc1388546348_29_ii,X0),X2)) ),
inference(cnf_transformation,[],[f782]) ).
fof(f1451,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(X0),X1),X2)) ),
inference(cnf_transformation,[],[f786]) ).
fof(f1575,plain,
~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f434]) ).
fof(f1731,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f1733,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f1731]) ).
fof(f1734,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f1575,f1731]) ).
fof(f1735,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f1733,f1059]) ).
fof(f1736,plain,
( scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f1733,f1060]) ).
fof(f1737,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f1733,f1061]) ).
fof(f1750,definition,
( spl29_2
<=> scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f1752,plain,
( scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f1750]) ).
fof(f1753,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f1736,f1731,f1750]) ).
fof(f1755,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(f1757,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_3 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1758,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f1737,f1731,f1755]) ).
fof(f1759,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_3 ),
inference(resolution,[],[f1757,f1296]) ).
fof(f2239,definition,
( spl29_5
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f2241,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f2239]) ).
fof(f2242,plain,
( spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f1735,f1731,f2239]) ).
fof(f2244,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc271589209all_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(f2246,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f2244]) ).
fof(f2247,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f1759,f1755,f2244]) ).
fof(f2249,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,[],[f2246,f1059]) ).
fof(f2250,plain,
( scratc984285568_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,[],[f2246,f1060]) ).
fof(f2251,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,[],[f2246,f1061]) ).
fof(f2264,definition,
( spl29_7
<=> scratc984285568_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(f2266,plain,
( scratc984285568_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,[],[f2264]) ).
fof(f2267,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f2250,f2244,f2264]) ).
fof(f2269,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(f2271,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,[],[f2269]) ).
fof(f2272,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f2251,f2244,f2269]) ).
fof(f2273,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_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,[],[f2271,f1409]) ).
fof(f2319,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc271589209all_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(f2321,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_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,[],[f2319]) ).
fof(f2322,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f2273,f2269,f2319]) ).
fof(f2324,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,[],[f2321,f1059]) ).
fof(f2325,plain,
( scratc984285568_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,[],[f2321,f1060]) ).
fof(f2326,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,[],[f2321,f1061]) ).
fof(f2339,definition,
( spl29_10
<=> scratc984285568_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(f2341,plain,
( scratc984285568_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,[],[f2339]) ).
fof(f2342,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f2325,f2319,f2339]) ).
fof(f2344,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| ~ spl29_10 ),
inference(resolution,[],[f2341,f1058]) ).
fof(f2345,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| spl29_9
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f2344,f2324]) ).
fof(f2347,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f2266,f1058]) ).
fof(f2348,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f2347,f2249]) ).
fof(f2350,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(scratc271589209all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f2351,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f2350]) ).
fof(f2352,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f2348,f2264,f2244,f2350]) ).
fof(f2635,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_cw))
| pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(resolution,[],[f2351,f1267]) ).
fof(f2712,plain,
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f2635,f1077]) ).
fof(f2789,definition,
( spl29_12
<=> 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_12])],[avatar_definition]) ).
fof(f2791,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f2789]) ).
fof(f2792,plain,
( spl29_12
| spl29_6 ),
inference(avatar_split_clause,[],[f2249,f2244,f2789]) ).
fof(f2794,definition,
( spl29_13
<=> ! [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(scratc271589209all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f2795,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(scratc271589209all_of(aTP_Lamm_a),X0)) )
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f2794]) ).
fof(f2796,plain,
( spl29_13
| spl29_9
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f2345,f2339,f2319,f2794]) ).
fof(f2982,definition,
( spl29_16
<=> 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_16])],[avatar_definition]) ).
fof(f2984,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_16 ),
inference(avatar_component_clause,[],[f2982]) ).
fof(f2985,plain,
( ~ spl29_16
| spl29_9 ),
inference(avatar_split_clause,[],[f2326,f2319,f2982]) ).
fof(f2986,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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,[],[f2984,f1444]) ).
fof(f2987,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,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(resolution,[],[f2984,f1445]) ).
fof(f2988,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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,[],[f2984,f1446]) ).
fof(f3034,definition,
( spl29_17
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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(f3036,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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,[],[f3034]) ).
fof(f3037,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f2988,f2982,f3034]) ).
fof(f3045,plain,
( ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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,[],[f3036,f873]) ).
fof(f3099,definition,
( spl29_19
<=> pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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(f3101,plain,
( ~ pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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,[],[f3099]) ).
fof(f3102,plain,
( ~ spl29_19
| spl29_17 ),
inference(avatar_split_clause,[],[f3045,f3034,f3099]) ).
fof(f3104,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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,[],[f3101,f870]) ).
fof(f3117,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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_20])],[avatar_definition]) ).
fof(f3119,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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_20 ),
inference(avatar_component_clause,[],[f3117]) ).
fof(f3120,plain,
( ~ spl29_20
| spl29_19 ),
inference(avatar_split_clause,[],[f3104,f3099,f3117]) ).
fof(f3180,definition,
( spl29_21
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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_21])],[avatar_definition]) ).
fof(f3182,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1388546348_29_ii,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_21 ),
inference(avatar_component_clause,[],[f3180]) ).
fof(f3183,plain,
( spl29_21
| spl29_16 ),
inference(avatar_split_clause,[],[f2986,f2982,f3180]) ).
fof(f3184,plain,
( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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_21 ),
inference(resolution,[],[f3182,f872]) ).
fof(f3226,definition,
( spl29_22
<=> pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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(f3228,plain,
( pp(aa_fun171081125l_bool(scratc126074659n_some,aa_TPT43085870d_bool(scratc1892179975ffprop(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,[],[f3226]) ).
fof(f3229,plain,
( spl29_22
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f3184,f3180,f3226]) ).
fof(f3231,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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_22 ),
inference(resolution,[],[f3228,f871]) ).
fof(f3316,definition,
( spl29_25
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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_25])],[avatar_definition]) ).
fof(f3318,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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_25 ),
inference(avatar_component_clause,[],[f3316]) ).
fof(f3319,plain,
( spl29_25
| ~ spl29_22 ),
inference(avatar_split_clause,[],[f3231,f3226,f3316]) ).
fof(f3325,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_bx(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_25 ),
inference(resolution,[],[f3318,f1451]) ).
fof(f3503,definition,
( spl29_27
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,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_27])],[avatar_definition]) ).
fof(f3505,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2056971326moreis,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_27 ),
inference(avatar_component_clause,[],[f3503]) ).
fof(f3506,plain,
( spl29_27
| spl29_16 ),
inference(avatar_split_clause,[],[f2987,f2982,f3503]) ).
fof(f3507,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_cv,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_27 ),
inference(resolution,[],[f3505,f1341]) ).
fof(f3890,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aTP_Lamm_bz))
| pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,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_13 ),
inference(resolution,[],[f2795,f1289]) ).
fof(f3989,plain,
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,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_13 ),
inference(forward_subsumption_resolution,[],[f3890,f1066]) ).
fof(f4134,definition,
( spl29_34
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,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(f4136,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cv,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,[],[f4134]) ).
fof(f4138,definition,
( spl29_35
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(f4140,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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,[],[f4138]) ).
fof(f4141,plain,
( ~ spl29_34
| spl29_35
| ~ spl29_27 ),
inference(avatar_split_clause,[],[f3507,f3503,f4138,f4134]) ).
fof(f4150,plain,
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cv,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_13
| spl29_34 ),
inference(resolution,[],[f4136,f2795]) ).
fof(f4189,plain,
( $false
| ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(forward_subsumption_resolution,[],[f4150,f2712]) ).
fof(f4190,plain,
( ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(avatar_contradiction_clause,[],[f4189]) ).
fof(f4804,definition,
( spl29_55
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_bx(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_55])],[avatar_definition]) ).
fof(f4805,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx(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(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_55 ),
inference(avatar_component_clause,[],[f4804]) ).
fof(f4806,plain,
( spl29_55
| ~ spl29_25 ),
inference(avatar_split_clause,[],[f3325,f3316,f4804]) ).
fof(f5261,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_55 ),
inference(resolution,[],[f4805,f1058]) ).
fof(f5296,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_5
| ~ spl29_55 ),
inference(forward_subsumption_resolution,[],[f5261,f2241]) ).
fof(f7672,definition,
( spl29_176
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_bx(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_176])],[avatar_definition]) ).
fof(f7673,plain,
( ! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_bx(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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_176 ),
inference(avatar_component_clause,[],[f7672]) ).
fof(f7674,plain,
( spl29_176
| ~ spl29_5
| ~ spl29_55 ),
inference(avatar_split_clause,[],[f5296,f4804,f2239,f7672]) ).
fof(f7675,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_by,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_176 ),
inference(resolution,[],[f7673,f1402]) ).
fof(f7691,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_by,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_2
| ~ spl29_176 ),
inference(forward_subsumption_resolution,[],[f7675,f1752]) ).
fof(f7693,definition,
( spl29_177
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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_by,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_177])],[avatar_definition]) ).
fof(f7694,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_by,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(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_177 ),
inference(avatar_component_clause,[],[f7693]) ).
fof(f7695,plain,
( spl29_177
| ~ spl29_2
| ~ spl29_176 ),
inference(avatar_split_clause,[],[f7691,f7672,f1750,f7693]) ).
fof(f7707,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_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(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) )
| ~ spl29_177 ),
inference(resolution,[],[f7694,f1058]) ).
fof(f7741,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) )
| ~ spl29_12
| ~ spl29_177 ),
inference(forward_subsumption_resolution,[],[f7707,f2791]) ).
fof(f7887,definition,
( spl29_187
<=> pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,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_187])],[avatar_definition]) ).
fof(f7889,plain,
( pp(aa_fun171081125l_bool(scratc271589209all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_by,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_187 ),
inference(avatar_component_clause,[],[f7887]) ).
fof(f7890,plain,
( spl29_187
| ~ spl29_13 ),
inference(avatar_split_clause,[],[f3989,f2794,f7887]) ).
fof(f7891,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_bz,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_187 ),
inference(resolution,[],[f7889,f1290]) ).
fof(f12223,definition,
( spl29_283
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_283])],[avatar_definition]) ).
fof(f12224,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1922987714lessis,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(scratc1749051690nd_iii,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_by,X0))) )
| ~ spl29_283 ),
inference(avatar_component_clause,[],[f12223]) ).
fof(f12225,plain,
( spl29_283
| ~ spl29_12
| ~ spl29_177 ),
inference(avatar_split_clause,[],[f7741,f7693,f2789,f12223]) ).
fof(f12226,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1749051690nd_iii,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)))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_by,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_283 ),
inference(resolution,[],[f12224,f4140]) ).
fof(f12280,plain,
( ! [X0] :
( ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_by,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_20
| ~ spl29_35
| ~ spl29_283 ),
inference(forward_subsumption_resolution,[],[f12226,f3119]) ).
fof(f12282,definition,
( spl29_284
<=> ! [X0] :
( ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_by,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_284])],[avatar_definition]) ).
fof(f12283,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc271589209all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_by,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))))))))
| ~ scratc984285568_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0) )
| ~ spl29_284 ),
inference(avatar_component_clause,[],[f12282]) ).
fof(f12284,plain,
( spl29_284
| spl29_20
| ~ spl29_35
| ~ spl29_283 ),
inference(avatar_split_clause,[],[f12280,f12223,f4138,f3117,f12282]) ).
fof(f12286,plain,
( ~ scratc984285568_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_bz,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_284 ),
inference(resolution,[],[f12283,f1289]) ).
fof(f12303,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bz,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_284 ),
inference(forward_subsumption_resolution,[],[f12286,f2266]) ).
fof(f12306,plain,
( $false
| ~ spl29_7
| ~ spl29_187
| ~ spl29_284 ),
inference(forward_subsumption_resolution,[],[f12303,f7891]) ).
fof(f12307,plain,
( ~ spl29_7
| ~ spl29_187
| ~ spl29_284 ),
inference(avatar_contradiction_clause,[],[f12306]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f1734]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f1753]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s5,plain,
( spl29_1
| spl29_5 ),
inference(sat_conversion,[],[f2242]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f2272]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f2322]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f2342]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s12,plain,
( spl29_6
| spl29_12 ),
inference(sat_conversion,[],[f2792]) ).
cnf(s13,plain,
( spl29_9
| ~ spl29_10
| spl29_13 ),
inference(sat_conversion,[],[f2796]) ).
cnf(s16,plain,
( spl29_9
| ~ spl29_16 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s17,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f3037]) ).
cnf(s19,plain,
( spl29_17
| ~ spl29_19 ),
inference(sat_conversion,[],[f3102]) ).
cnf(s20,plain,
( spl29_19
| ~ spl29_20 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s21,plain,
( spl29_16
| spl29_21 ),
inference(sat_conversion,[],[f3183]) ).
cnf(s22,plain,
( ~ spl29_21
| spl29_22 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s25,plain,
( ~ spl29_22
| spl29_25 ),
inference(sat_conversion,[],[f3319]) ).
cnf(s27,plain,
( spl29_16
| spl29_27 ),
inference(sat_conversion,[],[f3506]) ).
cnf(s34,plain,
( ~ spl29_27
| ~ spl29_34
| spl29_35 ),
inference(sat_conversion,[],[f4141]) ).
cnf(s35,plain,
( ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(sat_conversion,[],[f4190]) ).
cnf(s55,plain,
( ~ spl29_25
| spl29_55 ),
inference(sat_conversion,[],[f4806]) ).
cnf(s176,plain,
( ~ spl29_5
| ~ spl29_55
| spl29_176 ),
inference(sat_conversion,[],[f7674]) ).
cnf(s177,plain,
( ~ spl29_2
| ~ spl29_176
| spl29_177 ),
inference(sat_conversion,[],[f7695]) ).
cnf(s187,plain,
( ~ spl29_13
| spl29_187 ),
inference(sat_conversion,[],[f7890]) ).
cnf(s282,plain,
( ~ spl29_12
| ~ spl29_177
| spl29_283 ),
inference(sat_conversion,[],[f12225]) ).
cnf(s283,plain,
( spl29_20
| ~ spl29_35
| ~ spl29_283
| spl29_284 ),
inference(sat_conversion,[],[f12284]) ).
cnf(s285,plain,
( ~ spl29_7
| ~ spl29_187
| ~ spl29_284 ),
inference(sat_conversion,[],[f12307]) ).
cnf(s287,plain,
spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s288,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s289,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s300,plain,
~ spl29_6,
inference(rat,[],[s6,s288]) ).
cnf(s306,plain,
spl29_12,
inference(rat,[],[s12,s300]) ).
cnf(s307,plain,
~ spl29_8,
inference(rat,[],[s8,s300]) ).
cnf(s308,plain,
spl29_7,
inference(rat,[],[s7,s300]) ).
cnf(s350,plain,
~ spl29_9,
inference(rat,[],[s9,s307]) ).
cnf(s351,plain,
spl29_11,
inference(rat,[],[s11,s300,s308]) ).
cnf(s382,plain,
~ spl29_16,
inference(rat,[],[s16,s350]) ).
cnf(s384,plain,
spl29_10,
inference(rat,[],[s10,s350]) ).
cnf(s427,plain,
spl29_27,
inference(rat,[],[s27,s382]) ).
cnf(s428,plain,
spl29_21,
inference(rat,[],[s21,s382]) ).
cnf(s429,plain,
~ spl29_17,
inference(rat,[],[s17,s382]) ).
cnf(s432,plain,
spl29_13,
inference(rat,[],[s13,s350,s384]) ).
cnf(s441,plain,
spl29_22,
inference(rat,[],[s22,s428]) ).
cnf(s443,plain,
~ spl29_19,
inference(rat,[],[s19,s429]) ).
cnf(s458,plain,
spl29_187,
inference(rat,[],[s187,s432]) ).
cnf(s487,plain,
spl29_34,
inference(rat,[],[s35,s351,s432]) ).
cnf(s495,plain,
spl29_25,
inference(rat,[],[s25,s441]) ).
cnf(s496,plain,
~ spl29_20,
inference(rat,[],[s20,s443]) ).
cnf(s498,plain,
~ spl29_284,
inference(rat,[],[s285,s308,s458]) ).
cnf(s500,plain,
spl29_35,
inference(rat,[],[s34,s427,s487]) ).
cnf(s509,plain,
spl29_55,
inference(rat,[],[s55,s495]) ).
cnf(s519,plain,
~ spl29_283,
inference(rat,[],[s283,s498,s496,s500]) ).
cnf(s529,plain,
spl29_176,
inference(rat,[],[s176,s287,s509]) ).
cnf(s532,plain,
~ spl29_177,
inference(rat,[],[s282,s306,s519]) ).
cnf(s538,plain,
$false,
inference(rat,[],[s177,s289,s532,s529]) ).
fof(f12308,plain,
$false,
inference(avatar_sat_refutation,[],[s538]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM666+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 21:01:32 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 12.52/2.76 % (1157891)Detected formulas, will run a generic FOF schedule.
% 12.52/2.76 % (1157938)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=3065881227:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.52/2.76 % (1157939)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=1688566697:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.52/2.76 % (1157940)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=1085668951:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.52/2.76 % (1157943)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4090645317:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.52/2.76 % (1157941)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2234168504:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.52/2.76 % (1157944)dis-21_1_sil=8000:lcm=predicate:random_seed=979013800: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)
% 12.52/2.76 % (1157942)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=53713085:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.52/2.76 % (1157941)Refutation not found, incomplete strategy
% 12.52/2.76 % (1157941)------------------------------
% 12.52/2.76 % (1157941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.76 % (1157941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.76 % (1157941)CaDiCaL version: 2.1.3
% 12.52/2.76 % (1157941)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.76 % (1157941)Time elapsed: 0.002 s
% 12.52/2.76 % (1157941)Peak memory usage: 88 MB
% 12.52/2.76 % (1157941)Instructions burned: 2 (million)
% 12.52/2.76 % (1157942)Refutation not found, incomplete strategy
% 12.52/2.76 % (1157942)------------------------------
% 12.52/2.76 % (1157942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.76 % (1157942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.76 % (1157942)CaDiCaL version: 2.1.3
% 12.52/2.76 % (1157942)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.76 % (1157942)Time elapsed: 0.002 s
% 12.52/2.76 % (1157942)Peak memory usage: 88 MB
% 12.52/2.76 % (1157942)Instructions burned: 2 (million)
% 12.52/2.76 % (1157944)Instruction limit reached!
% 12.52/2.76 % (1157944)------------------------------
% 12.52/2.76 % (1157944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.76 % (1157944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.76 % (1157944)CaDiCaL version: 2.1.3
% 12.52/2.76 % (1157944)Termination reason: Instruction limit
% 12.52/2.76 % (1157944)Termination phase: Saturation
% 12.52/2.76 % (1157944)Time elapsed: 0.076 s
% 12.52/2.76 % (1157944)Peak memory usage: 90 MB
% 12.52/2.76 % (1157944)Instructions burned: 129 (million)
% 12.52/2.76 % (1157943)Instruction limit reached!
% 12.52/2.76 % (1157943)------------------------------
% 12.52/2.76 % (1157943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.76 % (1157943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.76 % (1157943)CaDiCaL version: 2.1.3
% 12.52/2.76 % (1157943)Termination reason: Instruction limit
% 12.52/2.76 % (1157943)Termination phase: Saturation
% 12.52/2.76 % (1157943)Time elapsed: 0.087 s
% 12.52/2.76 % (1157943)Peak memory usage: 90 MB
% 12.52/2.76 % (1157943)Instructions burned: 140 (million)
% 12.52/2.76 % (1157952)lrs+10_1_sil=8000:sp=occurrence:random_seed=900891138:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.52/2.76 % (1157952)Refutation not found, incomplete strategy
% 12.52/2.76 % (1157952)------------------------------
% 12.52/2.76 % (1157952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.52/2.76 % (1157952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.52/2.76 % (1157952)CaDiCaL version: 2.1.3
% 12.52/2.76 % (1157952)Termination reason: Refutation not found, incomplete strategy
% 12.52/2.76 % (1157952)Time elapsed: 0.003 s
% 12.52/2.76 % (1157952)Peak memory usage: 88 MB
% 12.52/2.76 % (1157952)Instructions burned: 2 (million)
% 12.52/2.76 % (1157953)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4223854492:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 21.37/3.98 % (1157941)------------------------------
% 21.37/3.98 % (1157941)------------------------------
% 21.37/3.98 % (1157942)------------------------------
% 21.37/3.98 % (1157942)------------------------------
% 21.37/3.98 % (1157953)Refutation not found, incomplete strategy
% 21.37/3.98 % (1157953)------------------------------
% 21.37/3.98 % (1157953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.98 % (1157953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.98 % (1157953)CaDiCaL version: 2.1.3
% 21.37/3.98 % (1157953)Termination reason: Refutation not found, incomplete strategy
% 21.37/3.98 % (1157953)Time elapsed: 0.004 s
% 21.37/3.98 % (1157953)Peak memory usage: 88 MB
% 21.37/3.98 % (1157953)Instructions burned: 7 (million)
% 21.37/3.98 % (1157956)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3166089304:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 21.37/3.98 % (1157957)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=3377688471:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 21.37/3.98 % (1157956)Refutation not found, incomplete strategy
% 21.37/3.98 % (1157956)------------------------------
% 21.37/3.98 % (1157956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.98 % (1157956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.98 % (1157956)CaDiCaL version: 2.1.3
% 21.37/3.98 % (1157956)Termination reason: Refutation not found, incomplete strategy
% 21.37/3.98 % (1157956)Time elapsed: 0.005 s
% 21.37/3.98 % (1157956)Peak memory usage: 89 MB
% 21.37/3.98 % (1157956)Instructions burned: 5 (million)
% 21.37/3.98 % (1157952)------------------------------
% 21.37/3.98 % (1157952)------------------------------
% 21.37/3.98 % (1157953)------------------------------
% 21.37/3.98 % (1157953)------------------------------
% 21.37/3.98 % (1157957)Instruction limit reached!
% 21.37/3.98 % (1157957)------------------------------
% 21.37/3.98 % (1157957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.98 % (1157957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.98 % (1157957)CaDiCaL version: 2.1.3
% 21.37/3.98 % (1157957)Termination reason: Instruction limit
% 21.37/3.98 % (1157957)Termination phase: Saturation
% 21.37/3.98 % (1157957)Time elapsed: 0.129 s
% 21.37/3.98 % (1157957)Peak memory usage: 93 MB
% 21.37/3.98 % (1157957)Instructions burned: 248 (million)
% 21.37/3.98 % (1157960)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=736144516:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 21.37/3.98 % (1157960)Refutation not found, incomplete strategy
% 21.37/3.98 % (1157960)------------------------------
% 21.37/3.98 % (1157960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.98 % (1157960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.98 % (1157960)CaDiCaL version: 2.1.3
% 21.37/3.98 % (1157960)Termination reason: Refutation not found, incomplete strategy
% 21.37/3.98 % (1157960)Time elapsed: 0.005 s
% 21.37/3.98 % (1157960)Peak memory usage: 88 MB
% 21.37/3.98 % (1157960)Instructions burned: 6 (million)
% 21.37/3.98 % (1157956)------------------------------
% 21.37/3.98 % (1157956)------------------------------
% 21.37/3.98 % (1157961)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2516354593:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 21.37/3.98 % (1157962)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1618040766:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 21.37/3.98 % (1157962)Instruction limit reached!
% 21.37/3.98 % (1157962)------------------------------
% 21.37/3.98 % (1157962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.37/3.98 % (1157962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.37/3.98 % (1157962)CaDiCaL version: 2.1.3
% 21.37/3.98 % (1157962)Termination reason: Instruction limit
% 21.37/3.98 % (1157962)Termination phase: Saturation
% 21.37/3.98 % (1157962)Time elapsed: 0.064 s
% 21.37/3.98 % (1157962)Peak memory usage: 90 MB
% 21.37/3.98 % (1157962)Instructions burned: 113 (million)
% 21.37/3.98 % (1157965)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2589354909:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 24.53/4.36 % (1157960)------------------------------
% 24.53/4.36 % (1157960)------------------------------
% 24.53/4.36 % (1157965)Instruction limit reached!
% 24.53/4.36 % (1157965)------------------------------
% 24.53/4.36 % (1157965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157965)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157965)Termination reason: Instruction limit
% 24.53/4.36 % (1157965)Termination phase: Saturation
% 24.53/4.36 % (1157965)Time elapsed: 0.061 s
% 24.53/4.36 % (1157965)Peak memory usage: 89 MB
% 24.53/4.36 % (1157965)Instructions burned: 127 (million)
% 24.53/4.36 % (1157967)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=641804030:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 24.53/4.36 % (1157967)Instruction limit reached!
% 24.53/4.36 % (1157967)------------------------------
% 24.53/4.36 % (1157967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157967)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157967)Termination reason: Instruction limit
% 24.53/4.36 % (1157967)Termination phase: Saturation
% 24.53/4.36 % (1157967)Time elapsed: 0.062 s
% 24.53/4.36 % (1157967)Peak memory usage: 89 MB
% 24.53/4.36 % (1157967)Instructions burned: 115 (million)
% 24.53/4.36 % (1157969)lrs+10_1_sil=8000:sp=occurrence:random_seed=3230855519:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 24.53/4.36 % (1157970)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2233943276:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 24.53/4.36 % (1157970)Refutation not found, incomplete strategy
% 24.53/4.36 % (1157970)------------------------------
% 24.53/4.36 % (1157970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157970)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157970)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.36 % (1157970)Time elapsed: 0.031 s
% 24.53/4.36 % (1157970)Peak memory usage: 90 MB
% 24.53/4.36 % (1157970)Instructions burned: 58 (million)
% 24.53/4.36 % (1157972)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2491974017:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 24.53/4.36 % (1157970)------------------------------
% 24.53/4.36 % (1157970)------------------------------
% 24.53/4.36 % (1157978)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2975233945:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 24.53/4.36 % (1157969)Instruction limit reached!
% 24.53/4.36 % (1157969)------------------------------
% 24.53/4.36 % (1157969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157969)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157969)Termination reason: Instruction limit
% 24.53/4.36 % (1157969)Termination phase: Saturation
% 24.53/4.36 % (1157969)Time elapsed: 0.518 s
% 24.53/4.36 % (1157969)Peak memory usage: 99 MB
% 24.53/4.36 % (1157969)Instructions burned: 909 (million)
% 24.53/4.36 % (1157978)Instruction limit reached!
% 24.53/4.36 % (1157978)------------------------------
% 24.53/4.36 % (1157978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157978)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157978)Termination reason: Instruction limit
% 24.53/4.36 % (1157978)Termination phase: Saturation
% 24.53/4.36 % (1157978)Time elapsed: 0.069 s
% 24.53/4.36 % (1157978)Peak memory usage: 92 MB
% 24.53/4.36 % (1157978)Instructions burned: 134 (million)
% 24.53/4.36 % (1157980)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1795824361:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 24.53/4.36 % (1157980)Refutation not found, incomplete strategy
% 24.53/4.36 % (1157980)------------------------------
% 24.53/4.36 % (1157980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157980)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157980)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.36 % (1157980)Time elapsed: 0.017 s
% 24.53/4.36 % (1157980)Peak memory usage: 89 MB
% 24.53/4.36 % (1157980)Instructions burned: 31 (million)
% 24.53/4.36 % (1157981)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=170873632:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 24.53/4.36 % (1157980)------------------------------
% 24.53/4.36 % (1157980)------------------------------
% 24.53/4.36 % (1157984)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=472096875:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 24.53/4.36 % (1157984)Refutation not found, incomplete strategy
% 24.53/4.36 % (1157984)------------------------------
% 24.53/4.36 % (1157984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157984)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157984)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.36 % (1157984)Time elapsed: 0.006 s
% 24.53/4.36 % (1157984)Peak memory usage: 88 MB
% 24.53/4.36 % (1157984)Instructions burned: 9 (million)
% 24.53/4.36 % (1157961)Instruction limit reached!
% 24.53/4.36 % (1157961)------------------------------
% 24.53/4.36 % (1157961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157961)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157961)Termination reason: Instruction limit
% 24.53/4.36 % (1157961)Termination phase: Saturation
% 24.53/4.36 % (1157961)Time elapsed: 1.595 s
% 24.53/4.36 % (1157961)Peak memory usage: 142 MB
% 24.53/4.36 % (1157961)Instructions burned: 2352 (million)
% 24.53/4.36 % (1157984)------------------------------
% 24.53/4.36 % (1157984)------------------------------
% 24.53/4.36 % (1157986)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3561673399:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 24.53/4.36 % (1157986)Instruction limit reached!
% 24.53/4.36 % (1157986)------------------------------
% 24.53/4.36 % (1157986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157986)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157986)Termination reason: Instruction limit
% 24.53/4.36 % (1157986)Termination phase: Saturation
% 24.53/4.36 % (1157986)Time elapsed: 0.070 s
% 24.53/4.36 % (1157986)Peak memory usage: 92 MB
% 24.53/4.36 % (1157986)Instructions burned: 135 (million)
% 24.53/4.36 % (1157987)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=75258438:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 24.53/4.36 % (1157987)Refutation not found, incomplete strategy
% 24.53/4.36 % (1157987)------------------------------
% 24.53/4.36 % (1157987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157987)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157987)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.36 % (1157987)Time elapsed: 0.002 s
% 24.53/4.36 % (1157987)Peak memory usage: 88 MB
% 24.53/4.36 % (1157987)Instructions burned: 2 (million)
% 24.53/4.36 % (1157989)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1124388550:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 24.53/4.36 % (1157989)Refutation not found, incomplete strategy
% 24.53/4.36 % (1157989)------------------------------
% 24.53/4.36 % (1157989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157989)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157989)Termination reason: Refutation not found, incomplete strategy
% 24.53/4.36 % (1157989)Time elapsed: 0.003 s
% 24.53/4.36 % (1157989)Peak memory usage: 89 MB
% 24.53/4.36 % (1157989)Instructions burned: 2 (million)
% 24.53/4.36 % (1157987)------------------------------
% 24.53/4.36 % (1157987)------------------------------
% 24.53/4.36 % (1157989)------------------------------
% 24.53/4.36 % (1157989)------------------------------
% 24.53/4.36 % (1157992)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=3664881027:i=6060:aac=none:ins=25_2970 on theBenchmark for (2970ds/6060Mi)
% 24.53/4.36 % (1157940)First to succeed.
% 24.53/4.36 % (1157940)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1157891"
% 24.53/4.36 % (1157993)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=4237170788:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 24.53/4.36 % (1157993)Instruction limit reached!
% 24.53/4.36 % (1157993)------------------------------
% 24.53/4.36 % (1157993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.53/4.36 % (1157993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.53/4.36 % (1157993)CaDiCaL version: 2.1.3
% 24.53/4.36 % (1157993)Termination reason: Instruction limit
% 24.53/4.36 % (1157993)Termination phase: Saturation
% 24.53/4.36 % (1157993)Time elapsed: 0.084 s
% 24.53/4.36 % (1157993)Peak memory usage: 91 MB
% 24.53/4.36 % (1157993)Instructions burned: 151 (million)
% 24.53/4.36 % (1157972)Also succeeded, but the first one will report.
% 24.53/4.36 % (1157940)Refutation found. Thanks to Tanya!
% 24.53/4.36 % SZS status Theorem for theBenchmark
% 24.53/4.36 % SZS output start Proof for theBenchmark
% See solution above
% 25.21/4.55 % (1157940)------------------------------
% 25.21/4.55 % (1157940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.21/4.55 % (1157940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.21/4.55 % (1157940)CaDiCaL version: 2.1.3
% 25.21/4.55 % (1157940)Termination reason: Refutation
% 25.21/4.55 % (1157940)Time elapsed: 3.037 s
% 25.21/4.55 % (1157940)Peak memory usage: 169 MB
% 25.21/4.55 % (1157940)Instructions burned: 4972 (million)
% 25.21/4.55 % (1157940)------------------------------
% 25.21/4.55 % (1157940)------------------------------
% 25.21/4.55 % (1157891)Success in time 3.5 s
% 25.21/4.55 % Vampire exiting
%------------------------------------------------------------------------------