%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM673+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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:16:23 PM UTC 2026
% Result : Theorem 172.72s 29.28s
% Output : Refutation 201.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 65
% Syntax : Number of formulae : 359 ( 71 unt; 45 def)
% Number of atoms : 927 ( 19 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1010 ( 442 ~; 475 |; 27 &)
% ( 61 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 46 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 16 con; 0-2 aty)
% Number of variables : 238 ( 0 sgn 236 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : gg_TPTP_ind(aa_TPTP_ind_TPTP_ind(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_aa_001t__TPTP____Interpret__Oind_001t__TPTP____Interpret__Oind) ).
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(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(scratc2026358273_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f33,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__26__prop1) ).
fof(f35,axiom,
! [X0] : scratc1565645440d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__pl) ).
fof(f53,axiom,
scratc1565186254d_n_is = scratc2046525893d_e_is(scratc1623441687nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f100,axiom,
! [X0] : scratc2046525893d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc685917419_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f149,axiom,
pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_bt)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz19c) ).
fof(f184,axiom,
pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ev)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz6) ).
fof(f287,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ev,X0))
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__23) ).
fof(f320,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0))
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__56) ).
fof(f321,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__57) ).
fof(f340,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__76) ).
fof(f377,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__113) ).
fof(f378,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__114) ).
fof(f396,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(scratc2026358273_29_ii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__132) ).
fof(f403,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__139) ).
fof(f458,axiom,
! [X0,X1] :
( ( gg_TPTP_ind(X0)
& gg_TPTP_ind(X1) )
=> ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fequal_1_1_fequal_001t__TPTP____Interpret__Oind_T) ).
fof(f462,conjecture,
pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f463,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f462]) ).
fof(f464,plain,
~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f463]) ).
fof(f481,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc685917419_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f482,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc685917419_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f481]) ).
fof(f563,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(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1)) ) ),
inference(ennf_transformation,[],[f396]) ).
fof(f574,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f403]) ).
fof(f596,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(ennf_transformation,[],[f458]) ).
fof(f597,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(flattening,[],[f596]) ).
fof(f601,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f602,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f606,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0))) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f665,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc685917419_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc685917419_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f482]) ).
fof(f666,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc685917419_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc685917419_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1)) ) ),
inference(rectify,[],[f665]) ).
fof(f667,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc685917419_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc685917419_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f666]) ).
fof(f709,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ev,X0))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ev,X0)) ) ),
inference(nnf_transformation,[],[f287]) ).
fof(f742,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0)) ) ),
inference(nnf_transformation,[],[f320]) ).
fof(f743,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f321]) ).
fof(f767,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0))) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1)) ) ),
inference(nnf_transformation,[],[f340]) ).
fof(f814,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1)) ) ),
inference(nnf_transformation,[],[f377]) ).
fof(f815,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1932834478all_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,[],[f378]) ).
fof(f835,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(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f563]) ).
fof(f836,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(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f835]) ).
fof(f849,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f574]) ).
fof(f850,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ) ),
inference(flattening,[],[f849]) ).
fof(f919,plain,
! [X0,X1] : gg_TPTP_ind(aa_TPTP_ind_TPTP_ind(X0,X1)),
inference(cnf_transformation,[],[f18]) ).
fof(f932,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f601]) ).
fof(f933,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f601]) ).
fof(f934,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f602]) ).
fof(f935,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(X0),X1))) ),
inference(cnf_transformation,[],[f602]) ).
fof(f942,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) ),
inference(cnf_transformation,[],[f606]) ).
fof(f943,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0))) ),
inference(cnf_transformation,[],[f606]) ).
fof(f946,plain,
! [X0] : scratc1565645440d_n_pl(X0) = aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),
inference(cnf_transformation,[],[f35]) ).
fof(f972,plain,
scratc1565186254d_n_is = scratc2046525893d_e_is(scratc1623441687nd_nat),
inference(cnf_transformation,[],[f53]) ).
fof(f1036,plain,
! [X0] : scratc2046525893d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f100]) ).
fof(f1120,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc685917419_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1)) ),
inference(cnf_transformation,[],[f667]) ).
fof(f1121,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f667]) ).
fof(f1122,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| scratc685917419_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f667]) ).
fof(f1123,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f667]) ).
fof(f1126,plain,
pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_bt)),
inference(cnf_transformation,[],[f149]) ).
fof(f1161,plain,
pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ev)),
inference(cnf_transformation,[],[f184]) ).
fof(f1316,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ev,X0)) ),
inference(cnf_transformation,[],[f709]) ).
fof(f1382,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0)) ),
inference(cnf_transformation,[],[f742]) ).
fof(f1385,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f743]) ).
fof(f1425,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X1)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1)) ),
inference(cnf_transformation,[],[f767]) ).
fof(f1509,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1)) ),
inference(cnf_transformation,[],[f814]) ).
fof(f1512,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f815]) ).
fof(f1550,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(scratc2026358273_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f836]) ).
fof(f1551,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(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X0)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X2),X1))) ),
inference(cnf_transformation,[],[f836]) ).
fof(f1574,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1565645440d_n_pl(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ),
inference(cnf_transformation,[],[f850]) ).
fof(f1690,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(cnf_transformation,[],[f597]) ).
fof(f1694,plain,
~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f464]) ).
fof(f1710,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0))) ),
inference(definition_unfolding,[],[f943,f946,f946]) ).
fof(f1711,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) ),
inference(definition_unfolding,[],[f942,f946,f946]) ).
fof(f1719,plain,
scratc1565186254d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f972,f1036]) ).
fof(f1770,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1)) ),
inference(definition_unfolding,[],[f1425,f946,f946]) ).
fof(f1799,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(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X2)),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X2)),X1))) ),
inference(definition_unfolding,[],[f1551,f946,f946]) ).
fof(f1806,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ),
inference(definition_unfolding,[],[f1574,f946,f946]) ).
fof(f1862,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f1864,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f1862]) ).
fof(f1865,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f1694,f1862]) ).
fof(f1866,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f1864,f1121]) ).
fof(f1867,plain,
( scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f1864,f1122]) ).
fof(f1868,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f1864,f1123]) ).
fof(f1881,definition,
( spl29_2
<=> scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f1883,plain,
( scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f1881]) ).
fof(f1884,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f1867,f1862,f1881]) ).
fof(f1886,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(f1888,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_3 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1889,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f1868,f1862,f1886]) ).
fof(f1890,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_3 ),
inference(resolution,[],[f1888,f1385]) ).
fof(f1928,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f1883,f1120]) ).
fof(f1929,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f1928,f1866]) ).
fof(f1931,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f1932,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f1931]) ).
fof(f1933,plain,
( spl29_4
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f1929,f1881,f1862,f1931]) ).
fof(f2409,definition,
( spl29_5
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f2411,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f2409]) ).
fof(f2412,plain,
( spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f1866,f1862,f2409]) ).
fof(f2414,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc1932834478all_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(f2416,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f2414]) ).
fof(f2417,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f1890,f1886,f2414]) ).
fof(f2419,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,[],[f2416,f1121]) ).
fof(f2420,plain,
( scratc685917419_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,[],[f2416,f1122]) ).
fof(f2421,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,[],[f2416,f1123]) ).
fof(f2434,definition,
( spl29_7
<=> scratc685917419_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(f2436,plain,
( scratc685917419_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,[],[f2434]) ).
fof(f2437,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f2420,f2414,f2434]) ).
fof(f2439,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(f2441,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,[],[f2439]) ).
fof(f2442,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f2421,f2414,f2439]) ).
fof(f2443,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_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,[],[f2441,f1512]) ).
fof(f2489,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc1932834478all_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(f2491,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_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,[],[f2489]) ).
fof(f2492,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f2443,f2439,f2489]) ).
fof(f2494,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,[],[f2491,f1121]) ).
fof(f2495,plain,
( scratc685917419_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,[],[f2491,f1122]) ).
fof(f2496,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,[],[f2491,f1123]) ).
fof(f2509,definition,
( spl29_10
<=> scratc685917419_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(f2511,plain,
( scratc685917419_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,[],[f2509]) ).
fof(f2512,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f2495,f2489,f2509]) ).
fof(f2514,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_10 ),
inference(resolution,[],[f2511,f1120]) ).
fof(f2515,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| spl29_9
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f2514,f2494]) ).
fof(f2517,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f2436,f1120]) ).
fof(f2518,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f2517,f2419]) ).
fof(f2520,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(scratc1932834478all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f2521,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f2520]) ).
fof(f2522,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f2518,f2434,f2414,f2520]) ).
fof(f2709,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0))) )
| ~ spl29_11 ),
inference(resolution,[],[f2521,f1770]) ).
fof(f2813,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_bt))
| pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(resolution,[],[f2521,f1382]) ).
fof(f2934,plain,
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f2813,f1126]) ).
fof(f2998,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(scratc1932834478all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f2999,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(scratc1932834478all_of(aTP_Lamm_a),X0)) )
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f2998]) ).
fof(f3000,plain,
( spl29_12
| spl29_9
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f2515,f2509,f2489,f2998]) ).
fof(f3011,definition,
( spl29_15
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f3013,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_15 ),
inference(avatar_component_clause,[],[f3011]) ).
fof(f3014,plain,
( ~ spl29_15
| spl29_9 ),
inference(avatar_split_clause,[],[f2496,f2489,f3011]) ).
fof(f3015,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_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_15 ),
inference(resolution,[],[f3013,f1550]) ).
fof(f3016,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_15 ),
inference(resolution,[],[f3013,f1799]) ).
fof(f3062,definition,
( spl29_16
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_16])],[avatar_definition]) ).
fof(f3064,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_16 ),
inference(avatar_component_clause,[],[f3062]) ).
fof(f3065,plain,
( ~ spl29_16
| spl29_15 ),
inference(avatar_split_clause,[],[f3016,f3011,f3062]) ).
fof(f3067,plain,
( ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_16 ),
inference(resolution,[],[f3064,f935]) ).
fof(f3123,definition,
( spl29_17
<=> pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_17])],[avatar_definition]) ).
fof(f3125,plain,
( ~ pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_17 ),
inference(avatar_component_clause,[],[f3123]) ).
fof(f3126,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f3067,f3062,f3123]) ).
fof(f3128,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_17 ),
inference(resolution,[],[f3125,f932]) ).
fof(f3141,definition,
( spl29_18
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_18])],[avatar_definition]) ).
fof(f3143,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_18 ),
inference(avatar_component_clause,[],[f3141]) ).
fof(f3144,plain,
( ~ spl29_18
| spl29_17 ),
inference(avatar_split_clause,[],[f3128,f3123,f3141]) ).
fof(f3389,definition,
( spl29_20
<=> 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)))))) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f3391,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_20 ),
inference(avatar_component_clause,[],[f3389]) ).
fof(f3392,plain,
( spl29_20
| spl29_9 ),
inference(avatar_split_clause,[],[f2494,f2489,f3389]) ).
fof(f3394,definition,
( spl29_21
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_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(f3396,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2026358273_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,[],[f3394]) ).
fof(f3397,plain,
( spl29_21
| spl29_15 ),
inference(avatar_split_clause,[],[f3015,f3011,f3394]) ).
fof(f3398,plain,
( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(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,[],[f3396,f934]) ).
fof(f3442,definition,
( spl29_22
<=> pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(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(f3444,plain,
( pp(aa_fun171081125l_bool(scratc1787319928n_some,aa_TPT43085870d_bool(scratc1715379698ffprop(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,[],[f3442]) ).
fof(f3445,plain,
( spl29_22
| ~ spl29_21 ),
inference(avatar_split_clause,[],[f3398,f3394,f3442]) ).
fof(f3447,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_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,[],[f3444,f933]) ).
fof(f3871,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aTP_Lamm_ev))
| pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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,[],[f2999,f1316]) ).
fof(f3922,plain,
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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,[],[f3871,f1161]) ).
fof(f4021,definition,
( spl29_26
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_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_26])],[avatar_definition]) ).
fof(f4023,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_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_26 ),
inference(avatar_component_clause,[],[f4021]) ).
fof(f4024,plain,
( spl29_26
| ~ spl29_22 ),
inference(avatar_split_clause,[],[f3447,f3442,f4021]) ).
fof(f4037,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0)) )
| ~ spl29_26 ),
inference(resolution,[],[f4023,f1806]) ).
fof(f5991,definition,
( spl29_118
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_118])],[avatar_definition]) ).
fof(f5993,plain,
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_118 ),
inference(avatar_component_clause,[],[f5991]) ).
fof(f5994,plain,
( spl29_118
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f2934,f2520,f5991]) ).
fof(f5996,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0))
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0) )
| ~ spl29_118 ),
inference(resolution,[],[f5993,f1120]) ).
fof(f6923,definition,
( spl29_156
<=> pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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_156])],[avatar_definition]) ).
fof(f6925,plain,
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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_156 ),
inference(avatar_component_clause,[],[f6923]) ).
fof(f6926,plain,
( spl29_156
| ~ spl29_12 ),
inference(avatar_split_clause,[],[f3922,f2998,f6923]) ).
fof(f20382,definition,
( spl29_513
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0))
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_513])],[avatar_definition]) ).
fof(f20383,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0))
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0) )
| ~ spl29_513 ),
inference(avatar_component_clause,[],[f20382]) ).
fof(f20384,plain,
( spl29_513
| ~ spl29_118 ),
inference(avatar_split_clause,[],[f5996,f5991,f20382]) ).
fof(f21066,plain,
( ! [X0] :
( ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0))) )
| ~ spl29_513 ),
inference(resolution,[],[f20383,f1509]) ).
fof(f21125,definition,
( spl29_529
<=> ! [X0] :
( ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_529])],[avatar_definition]) ).
fof(f21126,plain,
( ! [X0] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0)))
| ~ gg_TPTP_ind(X0)
| ~ scratc685917419_is_of(X0,aTP_Lamm_a) )
| ~ spl29_529 ),
inference(avatar_component_clause,[],[f21125]) ).
fof(f21127,plain,
( spl29_529
| ~ spl29_513 ),
inference(avatar_split_clause,[],[f21066,f20382,f21125]) ).
fof(f37414,definition,
( spl29_999
<=> ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_999])],[avatar_definition]) ).
fof(f37415,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
| ~ spl29_999 ),
inference(avatar_component_clause,[],[f37414]) ).
fof(f37416,plain,
( spl29_999
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f2709,f2520,f37414]) ).
fof(f62186,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(forward_demodulation,[],[f1690,f1719]) ).
fof(f63825,definition,
( spl29_1059
<=> ! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1059])],[avatar_definition]) ).
fof(f63826,plain,
( ! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) )
| ~ spl29_1059 ),
inference(avatar_component_clause,[],[f63825]) ).
fof(f63827,plain,
spl29_1059,
inference(avatar_split_clause,[],[f1121,f63825]) ).
fof(f64322,definition,
( spl29_1060
<=> ! [X0,X1,X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc685917419_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1060])],[avatar_definition]) ).
fof(f64323,plain,
( ! [X3,X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(X0),X1))
| ~ scratc685917419_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| pp(aa_TPTP_ind_bool(X1,X3)) )
| ~ spl29_1060 ),
inference(avatar_component_clause,[],[f64322]) ).
fof(f64324,plain,
spl29_1060,
inference(avatar_split_clause,[],[f1120,f64322]) ).
fof(f64325,plain,
( ! [X2,X0,X1] :
( ~ scratc685917419_is_of(X0,X1)
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(X2,X0))
| gg_TPTP_ind(sK12(X1,X2)) )
| ~ spl29_1059
| ~ spl29_1060 ),
inference(resolution,[],[f64323,f63826]) ).
fof(f64673,definition,
( spl29_1063
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ) ),
introduced(definition,[new_symbols(definition,[spl29_1063])],[avatar_definition]) ).
fof(f64674,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) )
| ~ spl29_1063 ),
inference(avatar_component_clause,[],[f64673]) ).
fof(f64675,plain,
spl29_1063,
inference(avatar_split_clause,[],[f62186,f64673]) ).
fof(f91769,definition,
( spl29_1157
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1157])],[avatar_definition]) ).
fof(f91770,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),X0)) )
| ~ spl29_1157 ),
inference(avatar_component_clause,[],[f91769]) ).
fof(f91771,plain,
( spl29_1157
| ~ spl29_26 ),
inference(avatar_split_clause,[],[f4037,f4021,f91769]) ).
fof(f91957,plain,
( ! [X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ scratc685917419_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0),X1)) )
| ~ spl29_529
| ~ spl29_1060 ),
inference(resolution,[],[f21126,f64323]) ).
fof(f94138,definition,
( spl29_1404
<=> ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1404])],[avatar_definition]) ).
fof(f94139,plain,
( ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) )
| ~ spl29_1404 ),
inference(avatar_component_clause,[],[f94138]) ).
fof(f94140,plain,
spl29_1404,
inference(avatar_split_clause,[],[f1711,f94138]) ).
fof(f94141,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1) = aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)
| ~ gg_TPTP_ind(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1))
| ~ gg_TPTP_ind(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)) )
| ~ spl29_1063
| ~ spl29_1404 ),
inference(resolution,[],[f94139,f64674]) ).
fof(f94164,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1) = aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)
| ~ gg_TPTP_ind(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)) )
| ~ spl29_1063
| ~ spl29_1404 ),
inference(forward_subsumption_resolution,[],[f94141,f919]) ).
fof(f94165,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1) = aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0) )
| ~ spl29_1063
| ~ spl29_1404 ),
inference(forward_subsumption_resolution,[],[f94164,f919]) ).
fof(f94273,definition,
( spl29_1421
<=> ! [X2,X0,X1] :
( ~ scratc685917419_is_of(X0,X1)
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(X2,X0))
| gg_TPTP_ind(sK12(X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1421])],[avatar_definition]) ).
fof(f94274,plain,
( ! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(X2,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc685917419_is_of(X0,X1)
| gg_TPTP_ind(sK12(X1,X2)) )
| ~ spl29_1421 ),
inference(avatar_component_clause,[],[f94273]) ).
fof(f94275,plain,
( spl29_1421
| ~ spl29_1059
| ~ spl29_1060 ),
inference(avatar_split_clause,[],[f64325,f64322,f63825,f94273]) ).
fof(f94313,definition,
( spl29_1428
<=> ! [X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ scratc685917419_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1428])],[avatar_definition]) ).
fof(f94314,plain,
( ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),X0),X1))
| ~ scratc685917419_is_of(X0,aTP_Lamm_a)
| ~ scratc685917419_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ gg_TPTP_ind(X0) )
| ~ spl29_1428 ),
inference(avatar_component_clause,[],[f94313]) ).
fof(f94315,plain,
( spl29_1428
| ~ spl29_529
| ~ spl29_1060 ),
inference(avatar_split_clause,[],[f91957,f64322,f21125,f94313]) ).
fof(f94404,definition,
( spl29_1440
<=> ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_1440])],[avatar_definition]) ).
fof(f94405,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) )
| ~ spl29_1440 ),
inference(avatar_component_clause,[],[f94404]) ).
fof(f94406,plain,
spl29_1440,
inference(avatar_split_clause,[],[f1710,f94404]) ).
fof(f94407,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
| ~ spl29_999
| ~ spl29_1440 ),
inference(resolution,[],[f94405,f37415]) ).
fof(f94461,definition,
( spl29_1445
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_1445])],[avatar_definition]) ).
fof(f94462,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
| ~ spl29_1445 ),
inference(avatar_component_clause,[],[f94461]) ).
fof(f94463,plain,
( spl29_1445
| ~ spl29_999
| ~ spl29_1440 ),
inference(avatar_split_clause,[],[f94407,f94404,f37414,f94461]) ).
fof(f96524,definition,
( spl29_1642
<=> ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1642])],[avatar_definition]) ).
fof(f96525,plain,
( ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1565186254d_n_is,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1)) )
| ~ spl29_1642 ),
inference(avatar_component_clause,[],[f96524]) ).
fof(f96526,plain,
spl29_1642,
inference(avatar_split_clause,[],[f1770,f96524]) ).
fof(f96527,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) )
| ~ spl29_1440
| ~ spl29_1642 ),
inference(resolution,[],[f96525,f94405]) ).
fof(f96554,definition,
( spl29_1643
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[spl29_1643])],[avatar_definition]) ).
fof(f96555,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_eu,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) )
| ~ spl29_1643 ),
inference(avatar_component_clause,[],[f96554]) ).
fof(f96556,plain,
( spl29_1643
| ~ spl29_1440
| ~ spl29_1642 ),
inference(avatar_split_clause,[],[f96527,f96524,f94404,f96554]) ).
fof(f96572,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
| ~ spl29_4
| ~ spl29_1643 ),
inference(resolution,[],[f96555,f1932]) ).
fof(f96594,definition,
( spl29_1647
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_1647])],[avatar_definition]) ).
fof(f96595,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,X0))) )
| ~ spl29_1647 ),
inference(avatar_component_clause,[],[f96594]) ).
fof(f96596,plain,
( spl29_1647
| ~ spl29_4
| ~ spl29_1643 ),
inference(avatar_split_clause,[],[f96572,f96554,f1931,f96594]) ).
fof(f100457,plain,
( ! [X0] :
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| gg_TPTP_ind(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| spl29_15
| ~ spl29_1421 ),
inference(resolution,[],[f94274,f3013]) ).
fof(f100492,plain,
( ! [X0] :
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X0)
| gg_TPTP_ind(sK12(X0,aTP_Lamm_ac)) )
| spl29_3
| ~ spl29_1421 ),
inference(resolution,[],[f94274,f1888]) ).
fof(f100599,plain,
( ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X0)
| gg_TPTP_ind(sK12(X0,aTP_Lamm_ac)) )
| spl29_3
| ~ spl29_5
| ~ spl29_1421 ),
inference(forward_subsumption_resolution,[],[f100492,f2411]) ).
fof(f100617,plain,
( ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| gg_TPTP_ind(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| spl29_15
| ~ spl29_20
| ~ spl29_1421 ),
inference(forward_subsumption_resolution,[],[f100457,f3391]) ).
fof(f100727,definition,
( spl29_2087
<=> ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| gg_TPTP_ind(sK12(X0,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_2087])],[avatar_definition]) ).
fof(f100728,plain,
( ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| gg_TPTP_ind(sK12(X0,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_2087 ),
inference(avatar_component_clause,[],[f100727]) ).
fof(f100729,plain,
( spl29_2087
| spl29_15
| ~ spl29_20
| ~ spl29_1421 ),
inference(avatar_split_clause,[],[f100617,f94273,f3389,f3011,f100727]) ).
fof(f100734,definition,
( spl29_2088
<=> ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X0)
| gg_TPTP_ind(sK12(X0,aTP_Lamm_ac)) ) ),
introduced(definition,[new_symbols(definition,[spl29_2088])],[avatar_definition]) ).
fof(f100735,plain,
( ! [X0] :
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X0)
| gg_TPTP_ind(sK12(X0,aTP_Lamm_ac)) )
| ~ spl29_2088 ),
inference(avatar_component_clause,[],[f100734]) ).
fof(f100736,plain,
( spl29_2088
| spl29_3
| ~ spl29_5
| ~ spl29_1421 ),
inference(avatar_split_clause,[],[f100599,f94273,f2409,f1886,f100734]) ).
fof(f229167,definition,
( spl29_4182
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1))
| aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1) = aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0) ) ),
introduced(definition,[new_symbols(definition,[spl29_4182])],[avatar_definition]) ).
fof(f229168,plain,
( ! [X0,X1] :
( aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X0)),X1) = aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,X1)),X0)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,X0),X1)) )
| ~ spl29_4182 ),
inference(avatar_component_clause,[],[f229167]) ).
fof(f229169,plain,
( spl29_4182
| ~ spl29_1063
| ~ spl29_1404 ),
inference(avatar_split_clause,[],[f94165,f94138,f64673,f229167]) ).
fof(f229400,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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(scratc210450928_prop1,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_18
| ~ spl29_4182 ),
inference(superposition,[],[f3143,f229168]) ).
fof(f229969,definition,
( spl29_4184
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4184])],[avatar_definition]) ).
fof(f229970,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4184 ),
inference(avatar_component_clause,[],[f229969]) ).
fof(f229971,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4184 ),
inference(avatar_component_clause,[],[f229969]) ).
fof(f229977,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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_1445
| spl29_4184 ),
inference(resolution,[],[f229971,f94462]) ).
fof(f229991,plain,
( $false
| ~ spl29_156
| ~ spl29_1445
| spl29_4184 ),
inference(forward_subsumption_resolution,[],[f229977,f6925]) ).
fof(f229992,plain,
( ~ spl29_156
| ~ spl29_1445
| spl29_4184 ),
inference(avatar_contradiction_clause,[],[f229991]) ).
fof(f229998,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_18
| ~ spl29_4182
| ~ spl29_4184 ),
inference(backward_subsumption_resolution,[],[f229400,f229970]) ).
fof(f230154,definition,
( spl29_4189
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_4189])],[avatar_definition]) ).
fof(f230156,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,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_4189 ),
inference(avatar_component_clause,[],[f230154]) ).
fof(f230157,plain,
( ~ spl29_4189
| spl29_18
| ~ spl29_4182
| ~ spl29_4184 ),
inference(avatar_split_clause,[],[f229998,f229969,f229167,f3141,f230154]) ).
fof(f230194,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4182
| spl29_4189 ),
inference(superposition,[],[f230156,f229168]) ).
fof(f230454,definition,
( spl29_4198
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4198])],[avatar_definition]) ).
fof(f230455,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4198 ),
inference(avatar_component_clause,[],[f230454]) ).
fof(f230456,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc210450928_prop1,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_4198 ),
inference(avatar_component_clause,[],[f230454]) ).
fof(f230463,plain,
( ~ pp(aa_fun171081125l_bool(scratc1932834478all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_eu,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_1647
| spl29_4198 ),
inference(resolution,[],[f230456,f96595]) ).
fof(f230481,plain,
( $false
| ~ spl29_156
| ~ spl29_1647
| spl29_4198 ),
inference(forward_subsumption_resolution,[],[f230463,f6925]) ).
fof(f230482,plain,
( ~ spl29_156
| ~ spl29_1647
| spl29_4198 ),
inference(avatar_contradiction_clause,[],[f230481]) ).
fof(f230584,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| ~ spl29_4182
| spl29_4189
| ~ spl29_4198 ),
inference(backward_subsumption_resolution,[],[f230194,f230455]) ).
fof(f231130,definition,
( spl29_4226
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_4226])],[avatar_definition]) ).
fof(f231132,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1582658943nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc713417593bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1941754212d_plus,sK12(aTP_Lamm_a,aTP_Lamm_ac))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_4226 ),
inference(avatar_component_clause,[],[f231130]) ).
fof(f231133,plain,
( ~ spl29_4226
| ~ spl29_4182
| spl29_4189
| ~ spl29_4198 ),
inference(avatar_split_clause,[],[f230584,f230454,f230154,f229167,f231130]) ).
fof(f231134,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_1157
| spl29_4226 ),
inference(resolution,[],[f231132,f91770]) ).
fof(f231148,definition,
( spl29_4227
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_4227])],[avatar_definition]) ).
fof(f231150,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_4227 ),
inference(avatar_component_clause,[],[f231148]) ).
fof(f231151,plain,
( ~ spl29_4227
| ~ spl29_1157
| spl29_4226 ),
inference(avatar_split_clause,[],[f231134,f231130,f91769,f231148]) ).
fof(f231153,plain,
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ scratc685917419_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)
| ~ 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))))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_1428
| spl29_4227 ),
inference(resolution,[],[f231150,f94314]) ).
fof(f231160,plain,
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ scratc685917419_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)
| ~ 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_1428
| ~ spl29_2088
| spl29_4227 ),
inference(forward_subsumption_resolution,[],[f231153,f100735]) ).
fof(f231161,plain,
( ~ scratc685917419_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ scratc685917419_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_1428
| ~ spl29_2087
| ~ spl29_2088
| spl29_4227 ),
inference(forward_subsumption_resolution,[],[f231160,f100728]) ).
fof(f231162,plain,
( ~ scratc685917419_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_2
| ~ spl29_1428
| ~ spl29_2087
| ~ spl29_2088
| spl29_4227 ),
inference(forward_subsumption_resolution,[],[f231161,f1883]) ).
fof(f231163,plain,
( $false
| ~ spl29_2
| ~ spl29_10
| ~ spl29_1428
| ~ spl29_2087
| ~ spl29_2088
| spl29_4227 ),
inference(forward_subsumption_resolution,[],[f231162,f2511]) ).
fof(f231164,plain,
( ~ spl29_2
| ~ spl29_10
| ~ spl29_1428
| ~ spl29_2087
| ~ spl29_2088
| spl29_4227 ),
inference(avatar_contradiction_clause,[],[f231163]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f1865]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s4,plain,
( spl29_1
| ~ spl29_2
| spl29_4 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s5,plain,
( spl29_1
| spl29_5 ),
inference(sat_conversion,[],[f2412]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f2417]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f2437]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f2492]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f2512]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f2522]) ).
cnf(s12,plain,
( spl29_9
| ~ spl29_10
| spl29_12 ),
inference(sat_conversion,[],[f3000]) ).
cnf(s15,plain,
( spl29_9
| ~ spl29_15 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s16,plain,
( spl29_15
| ~ spl29_16 ),
inference(sat_conversion,[],[f3065]) ).
cnf(s17,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s18,plain,
( spl29_17
| ~ spl29_18 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s20,plain,
( spl29_9
| spl29_20 ),
inference(sat_conversion,[],[f3392]) ).
cnf(s21,plain,
( spl29_15
| spl29_21 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s22,plain,
( ~ spl29_21
| spl29_22 ),
inference(sat_conversion,[],[f3445]) ).
cnf(s26,plain,
( ~ spl29_22
| spl29_26 ),
inference(sat_conversion,[],[f4024]) ).
cnf(s116,plain,
( ~ spl29_11
| spl29_118 ),
inference(sat_conversion,[],[f5994]) ).
cnf(s154,plain,
( ~ spl29_12
| spl29_156 ),
inference(sat_conversion,[],[f6926]) ).
cnf(s526,plain,
( ~ spl29_118
| spl29_513 ),
inference(sat_conversion,[],[f20384]) ).
cnf(s541,plain,
( ~ spl29_513
| spl29_529 ),
inference(sat_conversion,[],[f21127]) ).
cnf(s1021,plain,
( ~ spl29_11
| spl29_999 ),
inference(sat_conversion,[],[f37416]) ).
cnf(s3528,plain,
spl29_1059,
inference(sat_conversion,[],[f63827]) ).
cnf(s3529,plain,
spl29_1060,
inference(sat_conversion,[],[f64324]) ).
cnf(s3532,plain,
spl29_1063,
inference(sat_conversion,[],[f64675]) ).
cnf(s7709,plain,
( ~ spl29_26
| spl29_1157 ),
inference(sat_conversion,[],[f91771]) ).
cnf(s7985,plain,
spl29_1404,
inference(sat_conversion,[],[f94140]) ).
cnf(s8000,plain,
( ~ spl29_1059
| ~ spl29_1060
| spl29_1421 ),
inference(sat_conversion,[],[f94275]) ).
cnf(s8007,plain,
( ~ spl29_529
| ~ spl29_1060
| spl29_1428 ),
inference(sat_conversion,[],[f94315]) ).
cnf(s8018,plain,
spl29_1440,
inference(sat_conversion,[],[f94406]) ).
cnf(s8023,plain,
( ~ spl29_999
| ~ spl29_1440
| spl29_1445 ),
inference(sat_conversion,[],[f94463]) ).
cnf(s8224,plain,
spl29_1642,
inference(sat_conversion,[],[f96526]) ).
cnf(s8225,plain,
( ~ spl29_1440
| ~ spl29_1642
| spl29_1643 ),
inference(sat_conversion,[],[f96556]) ).
cnf(s8229,plain,
( ~ spl29_4
| ~ spl29_1643
| spl29_1647 ),
inference(sat_conversion,[],[f96596]) ).
cnf(s8658,plain,
( spl29_15
| ~ spl29_20
| ~ spl29_1421
| spl29_2087 ),
inference(sat_conversion,[],[f100729]) ).
cnf(s8659,plain,
( spl29_3
| ~ spl29_5
| ~ spl29_1421
| spl29_2088 ),
inference(sat_conversion,[],[f100736]) ).
cnf(s20598,plain,
( ~ spl29_1063
| ~ spl29_1404
| spl29_4182 ),
inference(sat_conversion,[],[f229169]) ).
cnf(s20602,plain,
( ~ spl29_156
| ~ spl29_1445
| spl29_4184 ),
inference(sat_conversion,[],[f229992]) ).
cnf(s20608,plain,
( spl29_18
| ~ spl29_4182
| ~ spl29_4184
| ~ spl29_4189 ),
inference(sat_conversion,[],[f230157]) ).
cnf(s20619,plain,
( ~ spl29_156
| ~ spl29_1647
| spl29_4198 ),
inference(sat_conversion,[],[f230482]) ).
cnf(s20648,plain,
( ~ spl29_4182
| spl29_4189
| ~ spl29_4198
| ~ spl29_4226 ),
inference(sat_conversion,[],[f231133]) ).
cnf(s20649,plain,
( ~ spl29_1157
| spl29_4226
| ~ spl29_4227 ),
inference(sat_conversion,[],[f231151]) ).
cnf(s20650,plain,
( ~ spl29_2
| ~ spl29_10
| ~ spl29_1428
| ~ spl29_2087
| ~ spl29_2088
| spl29_4227 ),
inference(sat_conversion,[],[f231164]) ).
cnf(s20653,plain,
spl29_1643,
inference(rat,[],[s8225,s8224,s8018]) ).
cnf(s20670,plain,
spl29_4182,
inference(rat,[],[s20598,s7985,s3532]) ).
cnf(s20735,plain,
spl29_1421,
inference(rat,[],[s8000,s3529,s3528]) ).
cnf(s20862,plain,
spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s20863,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s20864,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s20885,plain,
spl29_2088,
inference(rat,[],[s8659,s20862,s20735,s20863]) ).
cnf(s20897,plain,
~ spl29_6,
inference(rat,[],[s6,s20863]) ).
cnf(s20899,plain,
spl29_4,
inference(rat,[],[s4,s1,s20864]) ).
cnf(s20954,plain,
~ spl29_8,
inference(rat,[],[s8,s20897]) ).
cnf(s20955,plain,
spl29_7,
inference(rat,[],[s7,s20897]) ).
cnf(s21000,plain,
spl29_1647,
inference(rat,[],[s8229,s20653,s20899]) ).
cnf(s21118,plain,
~ spl29_9,
inference(rat,[],[s9,s20954]) ).
cnf(s21120,plain,
spl29_11,
inference(rat,[],[s11,s20897,s20955]) ).
cnf(s21318,plain,
spl29_20,
inference(rat,[],[s20,s21118]) ).
cnf(s21319,plain,
~ spl29_15,
inference(rat,[],[s15,s21118]) ).
cnf(s21320,plain,
spl29_10,
inference(rat,[],[s10,s21118]) ).
cnf(s21361,plain,
spl29_999,
inference(rat,[],[s1021,s21120]) ).
cnf(s21390,plain,
spl29_118,
inference(rat,[],[s116,s21120]) ).
cnf(s21735,plain,
spl29_2087,
inference(rat,[],[s8658,s21318,s20735,s21319]) ).
cnf(s21743,plain,
spl29_21,
inference(rat,[],[s21,s21319]) ).
cnf(s21745,plain,
~ spl29_16,
inference(rat,[],[s16,s21319]) ).
cnf(s21749,plain,
spl29_12,
inference(rat,[],[s12,s21118,s21320]) ).
cnf(s21769,plain,
spl29_1445,
inference(rat,[],[s8023,s8018,s21361]) ).
cnf(s21830,plain,
spl29_513,
inference(rat,[],[s526,s21390]) ).
cnf(s22085,plain,
spl29_22,
inference(rat,[],[s22,s21743]) ).
cnf(s22100,plain,
~ spl29_17,
inference(rat,[],[s17,s21745]) ).
cnf(s22165,plain,
spl29_156,
inference(rat,[],[s154,s21749]) ).
cnf(s22276,plain,
spl29_529,
inference(rat,[],[s541,s21830]) ).
cnf(s22472,plain,
spl29_26,
inference(rat,[],[s26,s22085]) ).
cnf(s22483,plain,
~ spl29_18,
inference(rat,[],[s18,s22100]) ).
cnf(s22571,plain,
spl29_4198,
inference(rat,[],[s20619,s21000,s22165]) ).
cnf(s22572,plain,
spl29_4184,
inference(rat,[],[s20602,s21769,s22165]) ).
cnf(s22642,plain,
spl29_1428,
inference(rat,[],[s8007,s3529,s22276]) ).
cnf(s22778,plain,
spl29_1157,
inference(rat,[],[s7709,s22472]) ).
cnf(s22847,plain,
~ spl29_4189,
inference(rat,[],[s20608,s22483,s20670,s22572]) ).
cnf(s22878,plain,
spl29_4227,
inference(rat,[],[s20650,s21320,s20885,s21735,s20864,s22642]) ).
cnf(s22923,plain,
spl29_4226,
inference(rat,[],[s20649,s22878,s22778]) ).
cnf(s22948,plain,
$false,
inference(rat,[],[s20648,s22571,s20670,s22923,s22847]) ).
fof(f231165,plain,
$false,
inference(avatar_sat_refutation,[],[s22948]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM673+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.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 21:06:01 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.39/2.32 % (2002594)Detected formulas, will run a generic FOF schedule.
% 10.39/2.32 % (2002702)dis-21_1_sil=8000:lcm=predicate:random_seed=1056201: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)
% 10.39/2.32 % (2002699)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2576082438:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.39/2.32 % (2002699)Refutation not found, incomplete strategy
% 10.39/2.32 % (2002699)------------------------------
% 10.39/2.32 % (2002699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.32 % (2002699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.32 % (2002699)CaDiCaL version: 2.1.3
% 10.39/2.32 % (2002699)Termination reason: Refutation not found, incomplete strategy
% 10.39/2.32 % (2002699)Time elapsed: 0.004 s
% 10.39/2.32 % (2002699)Peak memory usage: 88 MB
% 10.39/2.32 % (2002699)Instructions burned: 2 (million)
% 10.39/2.32 % (2002697)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3375604797:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.39/2.32 % (2002697)Refutation not found, incomplete strategy
% 10.39/2.32 % (2002697)------------------------------
% 10.39/2.32 % (2002697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.32 % (2002697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.32 % (2002697)CaDiCaL version: 2.1.3
% 10.39/2.32 % (2002697)Termination reason: Refutation not found, incomplete strategy
% 10.39/2.32 % (2002697)Time elapsed: 0.002 s
% 10.39/2.32 % (2002697)Peak memory usage: 88 MB
% 10.39/2.32 % (2002697)Instructions burned: 2 (million)
% 10.39/2.32 % (2002695)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=268082740:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.39/2.32 % (2002694)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=3292478253:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.39/2.32 % (2002696)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=1237568824:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.39/2.32 % (2002702)Instruction limit reached!
% 10.39/2.32 % (2002702)------------------------------
% 10.39/2.32 % (2002702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.32 % (2002702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.32 % (2002702)CaDiCaL version: 2.1.3
% 10.39/2.32 % (2002702)Termination reason: Instruction limit
% 10.39/2.32 % (2002702)Termination phase: Saturation
% 10.39/2.32 % (2002702)Time elapsed: 0.070 s
% 10.39/2.32 % (2002702)Peak memory usage: 90 MB
% 10.39/2.32 % (2002702)Instructions burned: 129 (million)
% 10.39/2.32 % (2002701)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4073074551:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.39/2.32 % (2002701)Instruction limit reached!
% 10.39/2.32 % (2002701)------------------------------
% 10.39/2.32 % (2002701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.32 % (2002701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.32 % (2002701)CaDiCaL version: 2.1.3
% 10.39/2.32 % (2002701)Termination reason: Instruction limit
% 10.39/2.32 % (2002701)Termination phase: Saturation
% 10.39/2.32 % (2002701)Time elapsed: 0.144 s
% 10.39/2.32 % (2002701)Peak memory usage: 90 MB
% 10.39/2.32 % (2002701)Instructions burned: 139 (million)
% 10.39/2.32 % (2002730)lrs+10_1_sil=8000:sp=occurrence:random_seed=4266295318:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.39/2.32 % (2002730)Refutation not found, incomplete strategy
% 10.39/2.32 % (2002730)------------------------------
% 10.39/2.32 % (2002730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.32 % (2002730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.32 % (2002730)CaDiCaL version: 2.1.3
% 10.39/2.32 % (2002730)Termination reason: Refutation not found, incomplete strategy
% 10.39/2.32 % (2002730)Time elapsed: 0.002 s
% 10.39/2.32 % (2002730)Peak memory usage: 88 MB
% 10.39/2.32 % (2002730)Instructions burned: 2 (million)
% 10.39/2.32 % (2002699)------------------------------
% 18.18/3.42 % (2002699)------------------------------
% 18.18/3.42 % (2002697)------------------------------
% 18.18/3.42 % (2002697)------------------------------
% 18.18/3.42 % (2002745)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2554173156:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 18.18/3.42 % (2002730)------------------------------
% 18.18/3.42 % (2002730)------------------------------
% 18.18/3.42 % (2002745)Refutation not found, incomplete strategy
% 18.18/3.42 % (2002745)------------------------------
% 18.18/3.42 % (2002745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.18/3.42 % (2002745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.18/3.42 % (2002745)CaDiCaL version: 2.1.3
% 18.18/3.42 % (2002745)Termination reason: Refutation not found, incomplete strategy
% 18.18/3.42 % (2002745)Time elapsed: 0.004 s
% 18.18/3.42 % (2002745)Peak memory usage: 88 MB
% 18.18/3.42 % (2002745)Instructions burned: 7 (million)
% 18.18/3.42 % (2002757)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1670716829:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 18.18/3.42 % (2002757)Refutation not found, incomplete strategy
% 18.18/3.42 % (2002757)------------------------------
% 18.18/3.42 % (2002757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.18/3.42 % (2002757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.18/3.42 % (2002757)CaDiCaL version: 2.1.3
% 18.18/3.42 % (2002757)Termination reason: Refutation not found, incomplete strategy
% 18.18/3.42 % (2002757)Time elapsed: 0.005 s
% 18.18/3.42 % (2002757)Peak memory usage: 89 MB
% 18.18/3.42 % (2002757)Instructions burned: 5 (million)
% 18.18/3.42 % (2002758)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=142748957:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 18.18/3.42 % (2002760)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2516522717:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 18.18/3.42 % (2002760)Refutation not found, incomplete strategy
% 18.18/3.42 % (2002760)------------------------------
% 18.18/3.42 % (2002760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.18/3.42 % (2002760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.18/3.42 % (2002760)CaDiCaL version: 2.1.3
% 18.18/3.42 % (2002760)Termination reason: Refutation not found, incomplete strategy
% 18.18/3.42 % (2002760)Time elapsed: 0.002 s
% 18.18/3.42 % (2002760)Peak memory usage: 88 MB
% 18.18/3.42 % (2002760)Instructions burned: 6 (million)
% 18.18/3.42 % (2002758)Instruction limit reached!
% 18.18/3.42 % (2002758)------------------------------
% 18.18/3.42 % (2002758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.18/3.42 % (2002758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.18/3.42 % (2002758)CaDiCaL version: 2.1.3
% 18.18/3.42 % (2002758)Termination reason: Instruction limit
% 18.18/3.42 % (2002758)Termination phase: Saturation
% 18.18/3.42 % (2002758)Time elapsed: 0.130 s
% 18.18/3.42 % (2002758)Peak memory usage: 94 MB
% 18.18/3.42 % (2002758)Instructions burned: 249 (million)
% 18.18/3.42 % (2002760)------------------------------
% 18.18/3.42 % (2002760)------------------------------
% 18.18/3.42 % (2002745)------------------------------
% 18.18/3.42 % (2002745)------------------------------
% 18.18/3.42 % (2002757)------------------------------
% 18.18/3.42 % (2002757)------------------------------
% 18.18/3.42 % (2002813)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2601434878:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 18.18/3.42 % (2002805)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=725247713:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 18.18/3.42 % (2002816)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3995086135:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 18.18/3.42 % (2002813)Instruction limit reached!
% 18.18/3.42 % (2002813)------------------------------
% 18.18/3.42 % (2002813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.18/3.42 % (2002813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.18/3.42 % (2002813)CaDiCaL version: 2.1.3
% 18.18/3.42 % (2002813)Termination reason: Instruction limit
% 18.18/3.42 % (2002813)Termination phase: Saturation
% 18.18/3.42 % (2002813)Time elapsed: 0.035 s
% 35.34/5.91 % (2002813)Peak memory usage: 91 MB
% 35.34/5.91 % (2002813)Instructions burned: 115 (million)
% 35.34/5.91 % (2002816)Instruction limit reached!
% 35.34/5.91 % (2002816)------------------------------
% 35.34/5.91 % (2002816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.34/5.91 % (2002816)CaDiCaL version: 2.1.3
% 35.34/5.91 % (2002816)Termination reason: Instruction limit
% 35.34/5.91 % (2002816)Termination phase: Saturation
% 35.34/5.91 % (2002816)Time elapsed: 0.063 s
% 35.34/5.91 % (2002816)Peak memory usage: 89 MB
% 35.34/5.91 % (2002816)Instructions burned: 129 (million)
% 35.34/5.91 % (2002834)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3991114977:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 35.34/5.91 % (2002849)lrs+10_1_sil=8000:sp=occurrence:random_seed=190577702:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 35.34/5.91 % (2002849)Refutation not found, incomplete strategy
% 35.34/5.91 % (2002849)------------------------------
% 35.34/5.91 % (2002849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.34/5.91 % (2002849)CaDiCaL version: 2.1.3
% 35.34/5.91 % (2002849)Termination reason: Refutation not found, incomplete strategy
% 35.34/5.91 % (2002849)Time elapsed: 0.001 s
% 35.34/5.91 % (2002849)Peak memory usage: 88 MB
% 35.34/5.91 % (2002849)Instructions burned: 2 (million)
% 35.34/5.91 % (2002834)Instruction limit reached!
% 35.34/5.91 % (2002834)------------------------------
% 35.34/5.91 % (2002834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.34/5.91 % (2002834)CaDiCaL version: 2.1.3
% 35.34/5.91 % (2002834)Termination reason: Instruction limit
% 35.34/5.91 % (2002834)Termination phase: Saturation
% 35.34/5.91 % (2002834)Time elapsed: 0.064 s
% 35.34/5.91 % (2002834)Peak memory usage: 90 MB
% 35.34/5.91 % (2002834)Instructions burned: 116 (million)
% 35.34/5.91 % (2002863)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4151583122:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 35.34/5.91 % (2002863)Refutation not found, incomplete strategy
% 35.34/5.91 % (2002863)------------------------------
% 35.34/5.91 % (2002863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.34/5.91 % (2002863)CaDiCaL version: 2.1.3
% 35.34/5.91 % (2002863)Termination reason: Refutation not found, incomplete strategy
% 35.34/5.91 % (2002863)Time elapsed: 0.034 s
% 35.34/5.91 % (2002863)Peak memory usage: 90 MB
% 35.34/5.91 % (2002863)Instructions burned: 62 (million)
% 35.34/5.91 % (2002849)------------------------------
% 35.34/5.91 % (2002849)------------------------------
% 35.34/5.91 % (2002880)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2250738113:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 35.34/5.91 % (2002882)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1947256860:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 35.34/5.91 % (2002882)Instruction limit reached!
% 35.34/5.91 % (2002882)------------------------------
% 35.34/5.91 % (2002882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.34/5.91 % (2002882)CaDiCaL version: 2.1.3
% 35.34/5.91 % (2002882)Termination reason: Instruction limit
% 35.34/5.91 % (2002882)Termination phase: Saturation
% 35.34/5.91 % (2002882)Time elapsed: 0.037 s
% 35.34/5.91 % (2002882)Peak memory usage: 93 MB
% 35.34/5.91 % (2002882)Instructions burned: 135 (million)
% 35.34/5.91 % (2002863)------------------------------
% 35.34/5.91 % (2002863)------------------------------
% 35.34/5.91 % (2002885)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=375330343:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 35.34/5.91 % (2002885)Refutation not found, incomplete strategy
% 35.34/5.91 % (2002885)------------------------------
% 35.34/5.91 % (2002885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.34/5.91 % (2002885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002885)CaDiCaL version: 2.1.3
% 66.56/10.25 % (2002885)Termination reason: Refutation not found, incomplete strategy
% 66.56/10.25 % (2002885)Time elapsed: 0.009 s
% 66.56/10.25 % (2002885)Peak memory usage: 89 MB
% 66.56/10.25 % (2002885)Instructions burned: 31 (million)
% 66.56/10.25 % (2002902)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=758377195:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 66.56/10.25 % (2002885)------------------------------
% 66.56/10.25 % (2002885)------------------------------
% 66.56/10.25 % (2002936)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=1921320680:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 66.56/10.25 % (2002936)Refutation not found, incomplete strategy
% 66.56/10.25 % (2002936)------------------------------
% 66.56/10.25 % (2002936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.56/10.25 % (2002936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002936)CaDiCaL version: 2.1.3
% 66.56/10.25 % (2002936)Termination reason: Refutation not found, incomplete strategy
% 66.56/10.25 % (2002936)Time elapsed: 0.003 s
% 66.56/10.25 % (2002936)Peak memory usage: 88 MB
% 66.56/10.25 % (2002936)Instructions burned: 9 (million)
% 66.56/10.25 % (2002936)------------------------------
% 66.56/10.25 % (2002936)------------------------------
% 66.56/10.25 % (2002938)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=181622396:i=134:gtgl=5:slsql=off:gtg=exists_sym_2981 on theBenchmark for (2981ds/134Mi)
% 66.56/10.25 % (2002938)Instruction limit reached!
% 66.56/10.25 % (2002938)------------------------------
% 66.56/10.25 % (2002938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.56/10.25 % (2002938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002938)CaDiCaL version: 2.1.3
% 66.56/10.25 % (2002938)Termination reason: Instruction limit
% 66.56/10.25 % (2002938)Termination phase: Saturation
% 66.56/10.25 % (2002938)Time elapsed: 0.037 s
% 66.56/10.25 % (2002938)Peak memory usage: 92 MB
% 66.56/10.25 % (2002938)Instructions burned: 136 (million)
% 66.56/10.25 % (2002940)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2399480059:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 66.56/10.25 % (2002940)Refutation not found, incomplete strategy
% 66.56/10.25 % (2002940)------------------------------
% 66.56/10.25 % (2002940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.56/10.25 % (2002940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002940)CaDiCaL version: 2.1.3
% 66.56/10.25 % (2002940)Termination reason: Refutation not found, incomplete strategy
% 66.56/10.25 % (2002940)Time elapsed: 0.001 s
% 66.56/10.25 % (2002940)Peak memory usage: 88 MB
% 66.56/10.25 % (2002940)Instructions burned: 2 (million)
% 66.56/10.25 % (2002940)------------------------------
% 66.56/10.25 % (2002940)------------------------------
% 66.56/10.25 % (2002942)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=255450536:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2977 on theBenchmark for (2977ds/431Mi)
% 66.56/10.25 % (2002942)Refutation not found, incomplete strategy
% 66.56/10.25 % (2002942)------------------------------
% 66.56/10.25 % (2002942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.56/10.25 % (2002942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002942)CaDiCaL version: 2.1.3
% 66.56/10.25 % (2002942)Termination reason: Refutation not found, incomplete strategy
% 66.56/10.25 % (2002942)Time elapsed: 0.001 s
% 66.56/10.25 % (2002942)Peak memory usage: 89 MB
% 66.56/10.25 % (2002942)Instructions burned: 2 (million)
% 66.56/10.25 % (2002942)------------------------------
% 66.56/10.25 % (2002942)------------------------------
% 66.56/10.25 % (2002944)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=3779374401:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 66.56/10.25 % (2002805)Instruction limit reached!
% 66.56/10.25 % (2002805)------------------------------
% 66.56/10.25 % (2002805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.56/10.25 % (2002805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.56/10.25 % (2002805)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002805)Termination reason: Instruction limit
% 77.75/11.95 % (2002805)Termination phase: Saturation
% 77.75/11.95 % (2002805)Time elapsed: 1.611 s
% 77.75/11.95 % (2002805)Peak memory usage: 142 MB
% 77.75/11.95 % (2002805)Instructions burned: 2350 (million)
% 77.75/11.95 % (2002946)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=2586924530:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 77.75/11.95 % (2002946)Instruction limit reached!
% 77.75/11.95 % (2002946)------------------------------
% 77.75/11.95 % (2002946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.75/11.95 % (2002946)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002946)Termination reason: Instruction limit
% 77.75/11.95 % (2002946)Termination phase: Saturation
% 77.75/11.95 % (2002946)Time elapsed: 0.080 s
% 77.75/11.95 % (2002946)Peak memory usage: 91 MB
% 77.75/11.95 % (2002946)Instructions burned: 151 (million)
% 77.75/11.95 % (2002948)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3143233522:i=14155:bd=all_2972 on theBenchmark for (2972ds/14155Mi)
% 77.75/11.95 % (2002880)Instruction limit reached!
% 77.75/11.95 % (2002880)------------------------------
% 77.75/11.95 % (2002880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.75/11.95 % (2002880)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002880)Termination reason: Instruction limit
% 77.75/11.95 % (2002880)Termination phase: Saturation
% 77.75/11.95 % (2002880)Time elapsed: 3.316 s
% 77.75/11.95 % (2002880)Peak memory usage: 162 MB
% 77.75/11.95 % (2002880)Instructions burned: 5202 (million)
% 77.75/11.95 % (2002944)Instruction limit reached!
% 77.75/11.95 % (2002944)------------------------------
% 77.75/11.95 % (2002944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.75/11.95 % (2002944)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002944)Termination reason: Instruction limit
% 77.75/11.95 % (2002944)Termination phase: Saturation
% 77.75/11.95 % (2002944)Time elapsed: 2.123 s
% 77.75/11.95 % (2002944)Peak memory usage: 191 MB
% 77.75/11.95 % (2002944)Instructions burned: 6063 (million)
% 77.75/11.95 % (2002950)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1726957429:i=667:av=off:fsr=off_2954 on theBenchmark for (2954ds/667Mi)
% 77.75/11.95 % (2002951)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4143869635:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 77.75/11.95 % (2002951)Instruction limit reached!
% 77.75/11.95 % (2002951)------------------------------
% 77.75/11.95 % (2002951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.75/11.95 % (2002951)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002951)Termination reason: Instruction limit
% 77.75/11.95 % (2002951)Termination phase: Saturation
% 77.75/11.95 % (2002951)Time elapsed: 0.044 s
% 77.75/11.95 % (2002951)Peak memory usage: 91 MB
% 77.75/11.95 % (2002951)Instructions burned: 187 (million)
% 77.75/11.95 % (2002954)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1977890620:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2951 on theBenchmark for (2951ds/193Mi)
% 77.75/11.95 % (2002954)Refutation not found, incomplete strategy
% 77.75/11.95 % (2002954)------------------------------
% 77.75/11.95 % (2002954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.75/11.95 % (2002954)CaDiCaL version: 2.1.3
% 77.75/11.95 % (2002954)Termination reason: Refutation not found, incomplete strategy
% 77.75/11.95 % (2002954)Time elapsed: 0.002 s
% 77.75/11.95 % (2002954)Peak memory usage: 88 MB
% 77.75/11.95 % (2002954)Instructions burned: 4 (million)
% 77.75/11.95 % (2002950)Instruction limit reached!
% 77.75/11.95 % (2002950)------------------------------
% 77.75/11.95 % (2002950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.75/11.95 % (2002950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002950)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002950)Termination reason: Instruction limit
% 93.74/14.11 % (2002950)Termination phase: Saturation
% 93.74/14.11 % (2002950)Time elapsed: 0.330 s
% 93.74/14.11 % (2002950)Peak memory usage: 100 MB
% 93.74/14.11 % (2002950)Instructions burned: 669 (million)
% 93.74/14.11 % (2002954)------------------------------
% 93.74/14.11 % (2002954)------------------------------
% 93.74/14.11 % (2002957)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3192008093:i=12111:sd=1:ss=included_2949 on theBenchmark for (2949ds/12111Mi)
% 93.74/14.11 % (2002956)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1388582522:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2949 on theBenchmark for (2949ds/4850Mi)
% 93.74/14.11 % (2002956)Instruction limit reached!
% 93.74/14.11 % (2002956)------------------------------
% 93.74/14.11 % (2002956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.74/14.11 % (2002956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002956)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002956)Termination reason: Instruction limit
% 93.74/14.11 % (2002956)Termination phase: Saturation
% 93.74/14.11 % (2002956)Time elapsed: 3.122 s
% 93.74/14.11 % (2002956)Peak memory usage: 152 MB
% 93.74/14.11 % (2002956)Instructions burned: 4851 (million)
% 93.74/14.11 % (2002960)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=793638968:i=319:kws=precedence:fsr=off_2916 on theBenchmark for (2916ds/319Mi)
% 93.74/14.11 % (2002960)Instruction limit reached!
% 93.74/14.11 % (2002960)------------------------------
% 93.74/14.11 % (2002960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.74/14.11 % (2002960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002960)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002960)Termination reason: Instruction limit
% 93.74/14.11 % (2002960)Termination phase: Saturation
% 93.74/14.11 % (2002960)Time elapsed: 0.170 s
% 93.74/14.11 % (2002960)Peak memory usage: 92 MB
% 93.74/14.11 % (2002960)Instructions burned: 319 (million)
% 93.74/14.11 % (2002962)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=450945440:i=2064:ep=RST_2913 on theBenchmark for (2913ds/2064Mi)
% 93.74/14.11 % (2002962)Refutation not found, incomplete strategy
% 93.74/14.11 % (2002962)------------------------------
% 93.74/14.11 % (2002962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.74/14.11 % (2002962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002962)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002962)Termination reason: Refutation not found, incomplete strategy
% 93.74/14.11 % (2002962)Time elapsed: 0.026 s
% 93.74/14.11 % (2002962)Peak memory usage: 89 MB
% 93.74/14.11 % (2002962)Instructions burned: 54 (million)
% 93.74/14.11 % (2002957)Instruction limit reached!
% 93.74/14.11 % (2002957)------------------------------
% 93.74/14.11 % (2002957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.74/14.11 % (2002957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002957)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002957)Termination reason: Instruction limit
% 93.74/14.11 % (2002957)Termination phase: Saturation
% 93.74/14.11 % (2002957)Time elapsed: 3.709 s
% 93.74/14.11 % (2002957)Peak memory usage: 287 MB
% 93.74/14.11 % (2002957)Instructions burned: 12112 (million)
% 93.74/14.11 % (2002964)dis-1011_128_sil=32000:random_seed=3666630646:i=3706:ep=RST:av=off_2911 on theBenchmark for (2911ds/3706Mi)
% 93.74/14.11 % (2002962)------------------------------
% 93.74/14.11 % (2002962)------------------------------
% 93.74/14.11 % (2002966)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=94423446:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2909 on theBenchmark for (2909ds/757Mi)
% 93.74/14.11 % (2002966)Refutation not found, incomplete strategy
% 93.74/14.11 % (2002966)------------------------------
% 93.74/14.11 % (2002966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 93.74/14.11 % (2002966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.74/14.11 % (2002966)CaDiCaL version: 2.1.3
% 93.74/14.11 % (2002966)Termination reason: Refutation not found, incomplete strategy
% 93.74/14.11 % (2002966)Time elapsed: 0.006 s
% 93.74/14.11 % (2002966)Peak memory usage: 89 MB
% 93.74/14.11 % (2002966)Instructions burned: 9 (million)
% 93.74/14.11 % (2002966)------------------------------
% 93.74/14.11 % (2002966)------------------------------
% 112.62/16.80 % (2002968)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3471906856:i=13913:ss=axioms:sgt=8_2906 on theBenchmark for (2906ds/13913Mi)
% 112.62/16.80 % (2002964)Instruction limit reached!
% 112.62/16.80 % (2002964)------------------------------
% 112.62/16.80 % (2002964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.62/16.80 % (2002964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.62/16.80 % (2002964)CaDiCaL version: 2.1.3
% 112.62/16.80 % (2002964)Termination reason: Instruction limit
% 112.62/16.80 % (2002964)Termination phase: Saturation
% 112.62/16.80 % (2002964)Time elapsed: 1.123 s
% 112.62/16.80 % (2002964)Peak memory usage: 112 MB
% 112.62/16.80 % (2002964)Instructions burned: 3710 (million)
% 112.62/16.80 % (2002902)Instruction limit reached!
% 112.62/16.80 % (2002902)------------------------------
% 112.62/16.80 % (2002902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.62/16.80 % (2002902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.62/16.80 % (2002902)CaDiCaL version: 2.1.3
% 112.62/16.80 % (2002902)Termination reason: Instruction limit
% 112.62/16.80 % (2002902)Termination phase: Saturation
% 112.62/16.80 % (2002902)Time elapsed: 8.533 s
% 112.62/16.80 % (2002902)Peak memory usage: 218 MB
% 112.62/16.80 % (2002902)Instructions burned: 13194 (million)
% 112.62/16.80 % (2002968)Refutation not found, incomplete strategy
% 112.62/16.80 % (2002968)------------------------------
% 112.62/16.80 % (2002968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.62/16.80 % (2002968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.62/16.80 % (2002968)CaDiCaL version: 2.1.3
% 112.62/16.80 % (2002968)Termination reason: Refutation not found, incomplete strategy
% 112.62/16.80 % (2002968)Time elapsed: 0.575 s
% 112.62/16.80 % (2002968)Peak memory usage: 129 MB
% 112.62/16.80 % (2002968)Instructions burned: 866 (million)
% 112.62/16.80 % (2002970)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2927263178:i=9925:aac=none_2899 on theBenchmark for (2899ds/9925Mi)
% 112.62/16.80 % (2002971)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2918502939:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2898 on theBenchmark for (2898ds/2479Mi)
% 112.62/16.80 % (2002971)Refutation not found, incomplete strategy
% 112.62/16.80 % (2002971)------------------------------
% 112.62/16.80 % (2002971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.62/16.80 % (2002971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.62/16.80 % (2002971)CaDiCaL version: 2.1.3
% 112.62/16.80 % (2002971)Termination reason: Refutation not found, incomplete strategy
% 112.62/16.80 % (2002971)Time elapsed: 0.004 s
% 112.62/16.80 % (2002971)Peak memory usage: 88 MB
% 112.62/16.80 % (2002971)Instructions burned: 4 (million)
% 112.62/16.80 % (2002968)------------------------------
% 112.62/16.80 % (2002968)------------------------------
% 112.62/16.80 % (2002971)------------------------------
% 112.62/16.80 % (2002971)------------------------------
% 112.62/16.80 % (2002974)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3734469816:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2896 on theBenchmark for (2896ds/440Mi)
% 112.62/16.80 % (2002976)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1661892129:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2894 on theBenchmark for (2894ds/11145Mi)
% 112.62/16.80 % (2002974)Instruction limit reached!
% 112.62/16.80 % (2002974)------------------------------
% 112.62/16.80 % (2002974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.62/16.80 % (2002974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.62/16.80 % (2002974)CaDiCaL version: 2.1.3
% 112.62/16.80 % (2002974)Termination reason: Instruction limit
% 112.62/16.80 % (2002974)Termination phase: Saturation
% 112.62/16.80 % (2002974)Time elapsed: 0.198 s
% 112.62/16.80 % (2002974)Peak memory usage: 92 MB
% 112.62/16.80 % (2002974)Instructions burned: 441 (million)
% 112.62/16.80 % (2002978)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3567448487:cts=off:i=3034:av=off:er=known:fsd=on_2892 on theBenchmark for (2892ds/3034Mi)
% 112.62/16.80 % (2002948)Instruction limit reached!
% 112.62/16.80 % (2002948)------------------------------
% 112.62/16.80 % (2002948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002948)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002948)Termination reason: Instruction limit
% 133.06/19.63 % (2002948)Termination phase: Saturation
% 133.06/19.63 % (2002948)Time elapsed: 8.188 s
% 133.06/19.63 % (2002948)Peak memory usage: 195 MB
% 133.06/19.63 % (2002948)Instructions burned: 14156 (million)
% 133.06/19.63 % (2002976)Refutation not found, incomplete strategy
% 133.06/19.63 % (2002976)------------------------------
% 133.06/19.63 % (2002976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002976)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002976)Termination reason: Refutation not found, incomplete strategy
% 133.06/19.63 % (2002976)Time elapsed: 0.602 s
% 133.06/19.63 % (2002976)Peak memory usage: 128 MB
% 133.06/19.63 % (2002976)Instructions burned: 914 (million)
% 133.06/19.63 % (2002980)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2254544349:st=2:s2a=on:i=524:s2at=2:ss=axioms_2888 on theBenchmark for (2888ds/524Mi)
% 133.06/19.63 % (2002980)Refutation not found, incomplete strategy
% 133.06/19.63 % (2002980)------------------------------
% 133.06/19.63 % (2002980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002980)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002980)Termination reason: Refutation not found, incomplete strategy
% 133.06/19.63 % (2002980)Time elapsed: 0.005 s
% 133.06/19.63 % (2002980)Peak memory usage: 88 MB
% 133.06/19.63 % (2002980)Instructions burned: 6 (million)
% 133.06/19.63 % (2002976)------------------------------
% 133.06/19.63 % (2002976)------------------------------
% 133.06/19.63 % (2002980)------------------------------
% 133.06/19.63 % (2002980)------------------------------
% 133.06/19.63 % (2002982)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=651064365:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2885 on theBenchmark for (2885ds/1016Mi)
% 133.06/19.63 % (2002982)Refutation not found, incomplete strategy
% 133.06/19.63 % (2002982)------------------------------
% 133.06/19.63 % (2002982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002982)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002982)Termination reason: Refutation not found, incomplete strategy
% 133.06/19.63 % (2002982)Time elapsed: 0.003 s
% 133.06/19.63 % (2002982)Peak memory usage: 89 MB
% 133.06/19.63 % (2002982)Instructions burned: 2 (million)
% 133.06/19.63 % (2002983)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3332625775:i=14123:bd=preordered:ins=4_2885 on theBenchmark for (2885ds/14123Mi)
% 133.06/19.63 % (2002982)------------------------------
% 133.06/19.63 % (2002982)------------------------------
% 133.06/19.63 % (2002986)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=188440550:i=5781:kws=precedence:bd=all:rawr=on_2881 on theBenchmark for (2881ds/5781Mi)
% 133.06/19.63 % (2002978)Instruction limit reached!
% 133.06/19.63 % (2002978)------------------------------
% 133.06/19.63 % (2002978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002978)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002978)Termination reason: Instruction limit
% 133.06/19.63 % (2002978)Termination phase: Saturation
% 133.06/19.63 % (2002978)Time elapsed: 1.708 s
% 133.06/19.63 % (2002978)Peak memory usage: 148 MB
% 133.06/19.63 % (2002978)Instructions burned: 3035 (million)
% 133.06/19.63 % (2002990)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=2115615337:i=2448:gtgl=5:bd=preordered:gtg=all_2874 on theBenchmark for (2874ds/2448Mi)
% 133.06/19.63 % (2002970)Instruction limit reached!
% 133.06/19.63 % (2002970)------------------------------
% 133.06/19.63 % (2002970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.06/19.63 % (2002970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.06/19.63 % (2002970)CaDiCaL version: 2.1.3
% 133.06/19.63 % (2002970)Termination reason: Instruction limit
% 133.06/19.63 % (2002970)Termination phase: Saturation
% 133.06/19.63 % (2002970)Time elapsed: 3.060 s
% 133.06/19.63 % (2002970)Peak memory usage: 212 MB
% 133.06/19.63 % (2002970)Instructions burned: 9926 (million)
% 155.27/22.73 % (2003122)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2093840070:i=3223:kws=precedence:fgj=on:av=off_2867 on theBenchmark for (2867ds/3223Mi)
% 155.27/22.73 % (2002990)Instruction limit reached!
% 155.27/22.73 % (2002990)------------------------------
% 155.27/22.73 % (2002990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.27/22.73 % (2002990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.27/22.73 % (2002990)CaDiCaL version: 2.1.3
% 155.27/22.73 % (2002990)Termination reason: Instruction limit
% 155.27/22.73 % (2002990)Termination phase: Saturation
% 155.27/22.73 % (2002990)Time elapsed: 1.398 s
% 155.27/22.73 % (2002990)Peak memory usage: 146 MB
% 155.27/22.73 % (2002990)Instructions burned: 2449 (million)
% 155.27/22.73 % (2003143)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3563413566:st=5.6:i=2033:sd=3:ss=axioms_2859 on theBenchmark for (2859ds/2033Mi)
% 155.27/22.73 % (2003122)Instruction limit reached!
% 155.27/22.73 % (2003122)------------------------------
% 155.27/22.73 % (2003122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.27/22.73 % (2003122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.27/22.73 % (2003122)CaDiCaL version: 2.1.3
% 155.27/22.73 % (2003122)Termination reason: Instruction limit
% 155.27/22.73 % (2003122)Termination phase: Saturation
% 155.27/22.73 % (2003122)Time elapsed: 1.050 s
% 155.27/22.73 % (2003122)Peak memory usage: 146 MB
% 155.27/22.73 % (2003122)Instructions burned: 3223 (million)
% 155.27/22.73 % (2003216)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=304652345:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2855 on theBenchmark for (2855ds/2055Mi)
% 155.27/22.73 % (2003216)Refutation not found, incomplete strategy
% 155.27/22.73 % (2003216)------------------------------
% 155.27/22.73 % (2003216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.27/22.73 % (2003216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.27/22.73 % (2003216)CaDiCaL version: 2.1.3
% 155.27/22.73 % (2003216)Termination reason: Refutation not found, incomplete strategy
% 155.27/22.73 % (2003216)Time elapsed: 0.316 s
% 155.27/22.73 % (2003216)Peak memory usage: 129 MB
% 155.27/22.73 % (2003216)Instructions burned: 875 (million)
% 155.27/22.73 % (2003143)Refutation not found, incomplete strategy
% 155.27/22.73 % (2003143)------------------------------
% 155.27/22.73 % (2003143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.27/22.73 % (2003143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.27/22.73 % (2003143)CaDiCaL version: 2.1.3
% 155.27/22.73 % (2003143)Termination reason: Refutation not found, incomplete strategy
% 155.27/22.73 % (2003143)Time elapsed: 0.696 s
% 155.27/22.73 % (2003143)Peak memory usage: 132 MB
% 155.27/22.73 % (2003143)Instructions burned: 958 (million)
% 155.27/22.73 % (2003216)------------------------------
% 155.27/22.73 % (2003216)------------------------------
% 155.27/22.73 % (2002986)Instruction limit reached!
% 155.27/22.73 % (2002986)------------------------------
% 155.27/22.73 % (2002986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.27/22.73 % (2002986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.27/22.73 % (2002986)CaDiCaL version: 2.1.3
% 155.27/22.73 % (2002986)Termination reason: Instruction limit
% 155.27/22.73 % (2002986)Termination phase: Saturation
% 155.27/22.73 % (2002986)Time elapsed: 3.008 s
% 155.27/22.73 % (2002986)Peak memory usage: 118 MB
% 155.27/22.73 % (2002986)Instructions burned: 5783 (million)
% 155.27/22.73 % (2003243)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=365307530:i=4835:sd=13:ss=axioms:sgt=23_2850 on theBenchmark for (2850ds/4835Mi)
% 155.27/22.73 % (2003242)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=2087860728:i=21611:sd=3:ss=axioms_2850 on theBenchmark for (2850ds/21611Mi)
% 155.27/22.73 % (2003143)------------------------------
% 155.27/22.73 % (2003143)------------------------------
% 155.27/22.73 % (2003246)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3245179877:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2847 on theBenchmark for (2847ds/797Mi)
% 155.27/22.73 % (2003246)Instruction limit reached!
% 155.27/22.73 % (2003246)------------------------------
% 155.27/22.73 % (2003246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003246)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003246)Termination reason: Instruction limit
% 172.72/29.27 % (2003246)Termination phase: Saturation
% 172.72/29.27 % (2003246)Time elapsed: 0.548 s
% 172.72/29.27 % (2003246)Peak memory usage: 91 MB
% 172.72/29.27 % (2003246)Instructions burned: 798 (million)
% 172.72/29.27 % (2003242)Refutation not found, incomplete strategy
% 172.72/29.27 % (2003242)------------------------------
% 172.72/29.27 % (2003242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003242)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003242)Termination reason: Refutation not found, incomplete strategy
% 172.72/29.27 % (2003242)Time elapsed: 0.851 s
% 172.72/29.27 % (2003242)Peak memory usage: 129 MB
% 172.72/29.27 % (2003242)Instructions burned: 912 (million)
% 172.72/29.27 % (2003267)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3866338313:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2840 on theBenchmark for (2840ds/2326Mi)
% 172.72/29.27 % (2003242)------------------------------
% 172.72/29.27 % (2003242)------------------------------
% 172.72/29.27 % (2003275)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3242211515:i=6038:nm=6_2836 on theBenchmark for (2836ds/6038Mi)
% 172.72/29.27 % (2003243)Instruction limit reached!
% 172.72/29.27 % (2003243)------------------------------
% 172.72/29.27 % (2003243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003243)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003243)Termination reason: Instruction limit
% 172.72/29.27 % (2003243)Termination phase: Saturation
% 172.72/29.27 % (2003243)Time elapsed: 2.253 s
% 172.72/29.27 % (2003243)Peak memory usage: 127 MB
% 172.72/29.27 % (2003243)Instructions burned: 4837 (million)
% 172.72/29.27 % (2003290)lrs+10_1_sil=32000:sp=occurrence:random_seed=2832549955:st=2:i=33334:sd=3:ss=included:sgt=32_2826 on theBenchmark for (2826ds/33334Mi)
% 172.72/29.27 % (2003267)Instruction limit reached!
% 172.72/29.27 % (2003267)------------------------------
% 172.72/29.27 % (2003267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003267)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003267)Termination reason: Instruction limit
% 172.72/29.27 % (2003267)Termination phase: Saturation
% 172.72/29.27 % (2003267)Time elapsed: 1.932 s
% 172.72/29.27 % (2003267)Peak memory usage: 101 MB
% 172.72/29.27 % (2003267)Instructions burned: 2326 (million)
% 172.72/29.27 % (2003332)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2583107606:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2818 on theBenchmark for (2818ds/1008Mi)
% 172.72/29.27 % (2003332)Refutation not found, incomplete strategy
% 172.72/29.27 % (2003332)------------------------------
% 172.72/29.27 % (2003332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003332)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003332)Termination reason: Refutation not found, incomplete strategy
% 172.72/29.27 % (2003332)Time elapsed: 0.036 s
% 172.72/29.27 % (2003332)Peak memory usage: 89 MB
% 172.72/29.27 % (2003332)Instructions burned: 58 (million)
% 172.72/29.27 % (2003332)------------------------------
% 172.72/29.27 % (2003332)------------------------------
% 172.72/29.27 % (2003334)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=530830639:i=8327:s2at=5:bd=preordered_2814 on theBenchmark for (2814ds/8327Mi)
% 172.72/29.27 % (2003275)Instruction limit reached!
% 172.72/29.27 % (2003275)------------------------------
% 172.72/29.27 % (2003275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003275)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003275)Termination reason: Instruction limit
% 172.72/29.27 % (2003275)Termination phase: Saturation
% 172.72/29.27 % (2003275)Time elapsed: 2.183 s
% 172.72/29.27 % (2003275)Peak memory usage: 189 MB
% 172.72/29.27 % (2003275)Instructions burned: 6041 (million)
% 172.72/29.27 % (2003336)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1507892486:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2812 on theBenchmark for (2812ds/1083Mi)
% 172.72/29.27 % (2003336)Instruction limit reached!
% 172.72/29.27 % (2003336)------------------------------
% 172.72/29.27 % (2003336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003336)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003336)Termination reason: Instruction limit
% 172.72/29.27 % (2003336)Termination phase: Saturation
% 172.72/29.27 % (2003336)Time elapsed: 0.229 s
% 172.72/29.27 % (2003336)Peak memory usage: 95 MB
% 172.72/29.27 % (2003336)Instructions burned: 1084 (million)
% 172.72/29.27 % (2003338)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2614188507:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2809 on theBenchmark for (2809ds/1084Mi)
% 172.72/29.27 % (2003338)Instruction limit reached!
% 172.72/29.27 % (2003338)------------------------------
% 172.72/29.27 % (2003338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003338)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003338)Termination reason: Instruction limit
% 172.72/29.27 % (2003338)Termination phase: Saturation
% 172.72/29.27 % (2003338)Time elapsed: 0.205 s
% 172.72/29.27 % (2003338)Peak memory usage: 89 MB
% 172.72/29.27 % (2003338)Instructions burned: 1088 (million)
% 172.72/29.27 % (2003340)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=166554233:i=6995:s2at=5:gtg=all_2806 on theBenchmark for (2806ds/6995Mi)
% 172.72/29.27 % (2002983)Instruction limit reached!
% 172.72/29.27 % (2002983)------------------------------
% 172.72/29.27 % (2002983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2002983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2002983)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2002983)Termination reason: Instruction limit
% 172.72/29.27 % (2002983)Termination phase: Saturation
% 172.72/29.27 % (2002983)Time elapsed: 9.113 s
% 172.72/29.27 % (2002983)Peak memory usage: 226 MB
% 172.72/29.27 % (2002983)Instructions burned: 14124 (million)
% 172.72/29.27 % (2003342)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2417724841:st=2:i=6225:sd=15:ss=axioms_2792 on theBenchmark for (2792ds/6225Mi)
% 172.72/29.27 % (2003342)Refutation not found, incomplete strategy
% 172.72/29.27 % (2003342)------------------------------
% 172.72/29.27 % (2003342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003342)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003342)Termination reason: Refutation not found, incomplete strategy
% 172.72/29.27 % (2003342)Time elapsed: 0.003 s
% 172.72/29.27 % (2003342)Peak memory usage: 88 MB
% 172.72/29.27 % (2003342)Instructions burned: 3 (million)
% 172.72/29.27 % (2003342)------------------------------
% 172.72/29.27 % (2003342)------------------------------
% 172.72/29.27 % (2003344)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2148316941:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2788 on theBenchmark for (2788ds/3372Mi)
% 172.72/29.27 % (2003344)Refutation not found, incomplete strategy
% 172.72/29.27 % (2003344)------------------------------
% 172.72/29.27 % (2003344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003344)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003344)Termination reason: Refutation not found, incomplete strategy
% 172.72/29.27 % (2003344)Time elapsed: 0.567 s
% 172.72/29.27 % (2003344)Peak memory usage: 129 MB
% 172.72/29.27 % (2003344)Instructions burned: 875 (million)
% 172.72/29.27 % (2003340)Instruction limit reached!
% 172.72/29.27 % (2003340)------------------------------
% 172.72/29.27 % (2003340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.27 % (2003340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.27 % (2003340)CaDiCaL version: 2.1.3
% 172.72/29.27 % (2003340)Termination reason: Instruction limit
% 172.72/29.28 % (2003340)Termination phase: Saturation
% 172.72/29.28 % (2003340)Time elapsed: 2.365 s
% 172.72/29.28 % (2003340)Peak memory usage: 183 MB
% 172.72/29.28 % (2003340)Instructions burned: 6998 (million)
% 172.72/29.28 % (2003346)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=140694193:st=2.3:i=26457:sd=10:ss=included:sgt=8_2781 on theBenchmark for (2781ds/26457Mi)
% 172.72/29.28 % (2003344)------------------------------
% 172.72/29.28 % (2003344)------------------------------
% 172.72/29.28 % (2003348)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=834883472:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2779 on theBenchmark for (2779ds/13494Mi)
% 172.72/29.28 % (2003334)Instruction limit reached!
% 172.72/29.28 % (2003334)------------------------------
% 172.72/29.28 % (2003334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.28 % (2003334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.28 % (2003334)CaDiCaL version: 2.1.3
% 172.72/29.28 % (2003334)Termination reason: Instruction limit
% 172.72/29.28 % (2003334)Termination phase: Saturation
% 172.72/29.28 % (2003334)Time elapsed: 5.303 s
% 172.72/29.28 % (2003334)Peak memory usage: 197 MB
% 172.72/29.28 % (2003334)Instructions burned: 8328 (million)
% 172.72/29.28 % (2003350)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=24405946:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2760 on theBenchmark for (2760ds/2503Mi)
% 172.72/29.28 % (2003350)Instruction limit reached!
% 172.72/29.28 % (2003350)------------------------------
% 172.72/29.28 % (2003350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.28 % (2003350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.28 % (2003350)CaDiCaL version: 2.1.3
% 172.72/29.28 % (2003350)Termination reason: Instruction limit
% 172.72/29.28 % (2003350)Termination phase: Saturation
% 172.72/29.28 % (2003350)Time elapsed: 1.606 s
% 172.72/29.28 % (2003350)Peak memory usage: 143 MB
% 172.72/29.28 % (2003350)Instructions burned: 2504 (million)
% 172.72/29.28 % (2003352)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=4121703646:i=2559:sd=1:ep=RSTC:ss=axioms_2742 on theBenchmark for (2742ds/2559Mi)
% 172.72/29.28 % (2003352)Refutation not found, incomplete strategy
% 172.72/29.28 % (2003352)------------------------------
% 172.72/29.28 % (2003352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.72/29.28 % (2003352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.72/29.28 % (2003352)CaDiCaL version: 2.1.3
% 172.72/29.28 % (2003352)Termination reason: Refutation not found, incomplete strategy
% 172.72/29.28 % (2003352)Time elapsed: 0.569 s
% 172.72/29.28 % (2003352)Peak memory usage: 129 MB
% 172.72/29.28 % (2003352)Instructions burned: 861 (million)
% 172.72/29.28 % (2003352)------------------------------
% 172.72/29.28 % (2003352)------------------------------
% 172.72/29.28 % (2003354)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4182267606:i=30753:av=off:ss=included_2733 on theBenchmark for (2733ds/30753Mi)
% 172.72/29.28 % (2002696)First to succeed.
% 172.72/29.28 % (2002696)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2002594"
% 172.72/29.28 % (2002696)Refutation found. Thanks to Tanya!
% 172.72/29.28 % SZS status Theorem for theBenchmark
% 172.72/29.28 % SZS output start Proof for theBenchmark
% See solution above
% 201.91/29.47 % (2002696)------------------------------
% 201.91/29.47 % (2002696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.91/29.47 % (2002696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.91/29.47 % (2002696)CaDiCaL version: 2.1.3
% 201.91/29.47 % (2002696)Termination reason: Refutation
% 201.91/29.47 % (2002696)Time elapsed: 27.832 s
% 201.91/29.47 % (2002696)Peak memory usage: 376 MB
% 201.91/29.47 % (2002696)Instructions burned: 42420 (million)
% 201.91/29.47 % (2002696)------------------------------
% 201.91/29.47 % (2002696)------------------------------
% 201.91/29.47 % (2002594)Success in time 28.41 s
% 201.91/29.47 % Vampire exiting
%------------------------------------------------------------------------------