%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM653+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 : n002.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:13 PM UTC 2026
% Result : Theorem 5.83s 1.79s
% Output : Refutation 7.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 30
% Syntax : Number of formulae : 184 ( 43 unt; 6 def)
% Number of atoms : 483 ( 58 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 508 ( 209 ~; 250 |; 25 &)
% ( 18 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 5 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 19 con; 0-2 aty)
% Number of variables : 194 ( 0 sgn 192 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [X0,X1] : gg_bool(aa_TPTP_ind_bool(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_aa_001t__TPTP____Interpret__Oind_001t__HOL__Obool) ).
fof(f19,axiom,
! [X0,X1] : gg_bool(aa_fun171081125l_bool(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_aa_001t__fun_It__TPTP____Interpret__Oind_Mt__HOL__Obool_J_001t__HOL__Obool) ).
fof(f25,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1))
<=> pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__lessis) ).
fof(f26,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
<=> pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__moreis) ).
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(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(scratc851743993_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f53,axiom,
scratc1053925318d_n_is = scratc1535264957d_e_is(scratc342656015nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f100,axiom,
! [X0] : scratc1535264957d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f110,axiom,
! [X0] : scratc922673981d_l_or(X0) = aa_boo1142376798l_bool(scratc302135674nd_imp,scratc974312001_d_not(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f115,axiom,
! [X0] :
( pp(scratc974312001_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc302135674nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f116,axiom,
scratc302135674nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1879391219_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(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_br)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz10c) ).
fof(f280,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
<=> pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__36) ).
fof(f281,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
<=> pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__37) ).
fof(f305,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
=> pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__61) ).
fof(f306,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1))
=> pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__62) ).
fof(f379,axiom,
pp(fTrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_2_1_U) ).
fof(f383,axiom,
! [X0] :
( gg_bool(X0)
=> ( X0 = fTrue
| X0 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(f384,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f385,axiom,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
fof(f387,axiom,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
fof(f390,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(f394,conjecture,
pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f395,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f394]) ).
fof(f396,plain,
~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(flattening,[],[f395]) ).
fof(f413,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1879391219_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f414,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1879391219_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f413]) ).
fof(f481,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
<=> ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f305]) ).
fof(f482,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ) ),
inference(ennf_transformation,[],[f306]) ).
fof(f504,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ gg_bool(X0) ),
inference(ennf_transformation,[],[f383]) ).
fof(f505,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ gg_bool(X0) ),
inference(flattening,[],[f504]) ).
fof(f506,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,[],[f390]) ).
fof(f507,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,[],[f506]) ).
fof(f508,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1))
| ~ pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f509,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f511,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f512,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f552,plain,
! [X0] :
( ( pp(scratc974312001_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc302135674nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc302135674nd_imp,X0),fFalse))
| ~ pp(scratc974312001_d_not(X0)) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f575,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1879391219_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1879391219_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f414]) ).
fof(f576,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1879391219_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1879391219_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1)) ) ),
inference(rectify,[],[f575]) ).
fof(f577,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1879391219_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1879391219_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f576]) ).
fof(f632,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
| ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0)) ) ),
inference(nnf_transformation,[],[f280]) ).
fof(f633,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ) ),
inference(nnf_transformation,[],[f281]) ).
fof(f666,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ) )
& ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ) ),
inference(nnf_transformation,[],[f481]) ).
fof(f667,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ) )
& ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ) ),
inference(flattening,[],[f666]) ).
fof(f668,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ) )
& ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(nnf_transformation,[],[f482]) ).
fof(f669,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ) )
& ( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(flattening,[],[f668]) ).
fof(f764,plain,
! [X0,X1] : gg_bool(aa_TPTP_ind_bool(X0,X1)),
inference(cnf_transformation,[],[f17]) ).
fof(f766,plain,
! [X0,X1] : gg_bool(aa_fun171081125l_bool(X0,X1)),
inference(cnf_transformation,[],[f19]) ).
fof(f772,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ),
inference(cnf_transformation,[],[f508]) ).
fof(f775,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_bool_bool(scratc922673981d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))) ),
inference(cnf_transformation,[],[f509]) ).
fof(f779,plain,
! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X1),X0)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f511]) ).
fof(f780,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1663770992n_some,aa_TPT43085870d_bool(scratc1632014586ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f512]) ).
fof(f818,plain,
scratc1053925318d_n_is = scratc1535264957d_e_is(scratc342656015nd_nat),
inference(cnf_transformation,[],[f53]) ).
fof(f882,plain,
! [X0] : scratc1535264957d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f100]) ).
fof(f896,plain,
! [X0] : aa_boo1142376798l_bool(scratc302135674nd_imp,scratc974312001_d_not(X0)) = scratc922673981d_l_or(X0),
inference(cnf_transformation,[],[f110]) ).
fof(f902,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc302135674nd_imp,X0),fFalse))
| ~ pp(scratc974312001_d_not(X0)) ),
inference(cnf_transformation,[],[f552]) ).
fof(f903,plain,
! [X0] :
( pp(scratc974312001_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc302135674nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f552]) ).
fof(f904,plain,
scratc302135674nd_imp = fimplies,
inference(cnf_transformation,[],[f116]) ).
fof(f966,plain,
! [X3,X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| ~ scratc1879391219_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| pp(aa_TPTP_ind_bool(X1,X3)) ),
inference(cnf_transformation,[],[f577]) ).
fof(f967,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f577]) ).
fof(f968,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1))
| scratc1879391219_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f577]) ).
fof(f969,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),X1)) ),
inference(cnf_transformation,[],[f577]) ).
fof(f972,plain,
pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_br)),
inference(cnf_transformation,[],[f149]) ).
fof(f1168,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0)) ),
inference(cnf_transformation,[],[f632]) ).
fof(f1170,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(cnf_transformation,[],[f633]) ).
fof(f1171,plain,
! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(cnf_transformation,[],[f633]) ).
fof(f1225,plain,
! [X0,X1] :
( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ),
inference(cnf_transformation,[],[f667]) ).
fof(f1229,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ),
inference(cnf_transformation,[],[f669]) ).
fof(f1230,plain,
! [X0,X1] :
( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(cnf_transformation,[],[f669]) ).
fof(f1387,plain,
pp(fTrue),
inference(cnf_transformation,[],[f379]) ).
fof(f1391,plain,
! [X0] :
( ~ gg_bool(X0)
| fFalse = X0
| fTrue = X0 ),
inference(cnf_transformation,[],[f505]) ).
fof(f1392,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f384]) ).
fof(f1393,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f385]) ).
fof(f1395,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| pp(X0) ),
inference(cnf_transformation,[],[f387]) ).
fof(f1398,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,[],[f507]) ).
fof(f1402,plain,
~ pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[],[f396]) ).
fof(f1405,plain,
! [X0] : scratc922673981d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc974312001_d_not(X0)),
inference(definition_unfolding,[],[f896,f904]) ).
fof(f1409,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ),
inference(definition_unfolding,[],[f772,f1405]) ).
fof(f1410,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ),
inference(definition_unfolding,[],[f775,f1405]) ).
fof(f1427,plain,
scratc1053925318d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f818,f882]) ).
fof(f1454,plain,
! [X0] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| pp(scratc974312001_d_not(X0)) ),
inference(definition_unfolding,[],[f903,f904]) ).
fof(f1455,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| ~ pp(scratc974312001_d_not(X0)) ),
inference(definition_unfolding,[],[f902,f904]) ).
fof(f1547,definition,
sF25 = scratc1809285542all_of(aTP_Lamm_a),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1548,plain,
scratc1809285542all_of(aTP_Lamm_a) = sF25,
inference(reorient_equations,[],[f1547]) ).
fof(f1549,definition,
sF26 = aa_fun171081125l_bool(sF25,aTP_Lamm_ab),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1550,plain,
aa_fun171081125l_bool(sF25,aTP_Lamm_ab) = sF26,
inference(reorient_equations,[],[f1549]) ).
fof(f1551,plain,
~ pp(sF26),
inference(definition_folding,[],[f1402,f1550,f1548]) ).
fof(f1582,plain,
! [X0] :
( ~ pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(superposition,[],[f1171,f1548]) ).
fof(f1584,plain,
! [X0] :
( pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(superposition,[],[f1170,f1548]) ).
fof(f1587,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(resolution,[],[f969,f1229]) ).
fof(f1597,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(superposition,[],[f1398,f1427]) ).
fof(f1600,plain,
! [X0] :
( pp(aa_fun171081125l_bool(sF25,X0))
| gg_TPTP_ind(sK12(aTP_Lamm_a,X0)) ),
inference(superposition,[],[f967,f1548]) ).
fof(f1603,plain,
( pp(sF26)
| gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab)) ),
inference(superposition,[],[f1600,f1550]) ).
fof(f1604,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab)),
inference(forward_subsumption_resolution,[],[f1603,f1551]) ).
fof(f1605,plain,
! [X0,X1] :
( ~ pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ),
inference(resolution,[],[f1393,f1409]) ).
fof(f1611,plain,
! [X0,X1] :
( pp(scratc974312001_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ),
inference(resolution,[],[f1410,f1395]) ).
fof(f1613,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1)) ),
inference(resolution,[],[f1611,f1230]) ).
fof(f1614,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),sK12(X1,aa_TPT43085870d_bool(aTP_Lamm_aa,X0))))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
inference(resolution,[],[f1613,f969]) ).
fof(f1620,plain,
! [X0] :
( scratc1879391219_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)),aTP_Lamm_a)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[],[f968,f1171]) ).
fof(f1622,plain,
! [X0] :
( scratc1879391219_is_of(sK12(aTP_Lamm_a,X0),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(sF25,X0)) ),
inference(superposition,[],[f968,f1548]) ).
fof(f1626,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X1),X0)) ),
inference(resolution,[],[f780,f779]) ).
fof(f1627,plain,
! [X0] :
( ~ pp(scratc974312001_d_not(X0))
| ~ pp(X0)
| pp(fFalse) ),
inference(resolution,[],[f1455,f1393]) ).
fof(f1628,plain,
! [X0] :
( ~ pp(scratc974312001_d_not(X0))
| ~ pp(X0) ),
inference(forward_subsumption_resolution,[],[f1627,f1392]) ).
fof(f1635,plain,
! [X0,X1] :
( aa_fun171081125l_bool(X0,X1) = fTrue
| aa_fun171081125l_bool(X0,X1) = fFalse ),
inference(resolution,[],[f1391,f766]) ).
fof(f1661,plain,
! [X0] :
( ~ pp(fTrue)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) ),
inference(superposition,[],[f1582,f1635]) ).
fof(f1674,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) ),
inference(forward_subsumption_resolution,[],[f1661,f1387]) ).
fof(f1731,plain,
! [X0] :
( pp(scratc974312001_d_not(X0))
| pp(X0) ),
inference(resolution,[],[f1454,f1395]) ).
fof(f1735,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,X0),X1)) ),
inference(resolution,[],[f1731,f1230]) ).
fof(f1756,plain,
! [X0,X1] :
( aa_TPTP_ind_bool(X0,X1) = fTrue
| aa_TPTP_ind_bool(X0,X1) = fFalse ),
inference(resolution,[],[f764,f1391]) ).
fof(f1802,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X0),X1)) ),
inference(resolution,[],[f1225,f1605]) ).
fof(f1803,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X0),X1)) ),
inference(resolution,[],[f1225,f1628]) ).
fof(f1828,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f972,f966]) ).
fof(f1983,plain,
! [X0,X1] :
( ~ pp(fTrue)
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X1),X0))
| fFalse = aa_TPTP_ind_bool(X0,sK12(X1,X0)) ),
inference(superposition,[],[f969,f1756]) ).
fof(f2098,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X1),X0))
| fFalse = aa_TPTP_ind_bool(X0,sK12(X1,X0)) ),
inference(forward_subsumption_resolution,[],[f1983,f1387]) ).
fof(f2103,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
inference(resolution,[],[f2098,f1171]) ).
fof(f2959,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aTP_Lamm_ab))
| fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(X0,aTP_Lamm_ab))) ),
inference(resolution,[],[f1674,f969]) ).
fof(f2964,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
inference(superposition,[],[f2959,f1548]) ).
fof(f2966,plain,
( pp(sF26)
| fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
inference(forward_demodulation,[],[f2964,f1550]) ).
fof(f2967,plain,
fFalse = aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),
inference(forward_subsumption_resolution,[],[f2966,f1551]) ).
fof(f2969,plain,
( pp(fFalse)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
inference(superposition,[],[f1584,f2967]) ).
fof(f2975,plain,
~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab))),
inference(forward_subsumption_resolution,[],[f2969,f1392]) ).
fof(f2977,plain,
fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),
inference(resolution,[],[f2975,f2103]) ).
fof(f2987,plain,
( pp(fFalse)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))) ),
inference(superposition,[],[f1735,f2977]) ).
fof(f2999,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc851743993_29_ii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),
inference(forward_subsumption_resolution,[],[f2987,f1392]) ).
fof(f3029,plain,
pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),sK12(aTP_Lamm_a,aTP_Lamm_ab))),
inference(resolution,[],[f2999,f1626]) ).
fof(f3052,definition,
( spl27_53
<=> scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl27_53])],[avatar_definition]) ).
fof(f3053,plain,
( scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl27_53 ),
inference(avatar_component_clause,[],[f3052]) ).
fof(f3054,plain,
( ~ scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl27_53 ),
inference(avatar_component_clause,[],[f3052]) ).
fof(f3092,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| spl27_53 ),
inference(resolution,[],[f3054,f1622]) ).
fof(f3093,plain,
( pp(sF26)
| spl27_53 ),
inference(forward_demodulation,[],[f3092,f1550]) ).
fof(f3094,plain,
( $false
| spl27_53 ),
inference(forward_subsumption_resolution,[],[f3093,f1551]) ).
fof(f3095,plain,
spl27_53,
inference(avatar_contradiction_clause,[],[f3094]) ).
fof(f3351,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ~ scratc1879391219_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0)) ),
inference(resolution,[],[f1168,f966]) ).
fof(f3356,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X1),X0))
| ~ gg_TPTP_ind(X0)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X1),X0)) ),
inference(resolution,[],[f3351,f1803]) ).
fof(f3357,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc804593329moreis,X1),X0))
| ~ gg_TPTP_ind(X0)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X1),X0)) ),
inference(resolution,[],[f3351,f1802]) ).
fof(f3362,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(resolution,[],[f3357,f1614]) ).
fof(f3374,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc670609717lessis,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(forward_subsumption_resolution,[],[f3362,f967]) ).
fof(f3375,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1053925318d_n_is,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(forward_subsumption_resolution,[],[f3374,f1587]) ).
fof(f3378,plain,
! [X0,X1] :
( ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1)))
| sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)) = X1
| ~ gg_TPTP_ind(X1)
| ~ gg_TPTP_ind(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(resolution,[],[f3375,f1597]) ).
fof(f3382,plain,
! [X0,X1] :
( ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1)))
| sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)) = X1
| ~ gg_TPTP_ind(X1) ),
inference(forward_subsumption_resolution,[],[f3378,f967]) ).
fof(f3383,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[],[f3382,f1620]) ).
fof(f3387,plain,
! [X0] :
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
| sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(forward_subsumption_resolution,[],[f3383,f1171]) ).
fof(f3388,plain,
! [X0] :
( sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f3387,f1828]) ).
fof(f3394,plain,
! [X0] :
( sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a) ),
inference(duplicate_literal_removal,[],[f3388]) ).
fof(f3401,definition,
( spl27_67
<=> ! [X0] :
( sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a)
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ gg_TPTP_ind(X0) ) ),
introduced(definition,[new_symbols(definition,[spl27_67])],[avatar_definition]) ).
fof(f3402,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ scratc1879391219_is_of(X0,aTP_Lamm_a)
| sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) = X0
| ~ gg_TPTP_ind(X0) )
| ~ spl27_67 ),
inference(avatar_component_clause,[],[f3401]) ).
fof(f3404,plain,
spl27_67,
inference(avatar_split_clause,[],[f3394,f3401]) ).
fof(f3406,plain,
( ! [X0] :
( ~ scratc1879391219_is_of(sK12(X0,aTP_Lamm_ab),aTP_Lamm_a)
| sK12(X0,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(X0,aTP_Lamm_ab)))
| ~ gg_TPTP_ind(sK12(X0,aTP_Lamm_ab))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aTP_Lamm_ab)) )
| ~ spl27_67 ),
inference(resolution,[],[f3402,f969]) ).
fof(f3410,plain,
( ! [X0] :
( ~ scratc1879391219_is_of(sK12(X0,aTP_Lamm_ab),aTP_Lamm_a)
| sK12(X0,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(X0,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aTP_Lamm_ab)) )
| ~ spl27_67 ),
inference(forward_subsumption_resolution,[],[f3406,f967]) ).
fof(f3417,plain,
( sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aTP_Lamm_ab))
| pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| ~ spl27_67 ),
inference(resolution,[],[f3410,f1622]) ).
fof(f3431,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(resolution,[],[f3356,f1614]) ).
fof(f3446,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,X1),sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1))))
| ~ scratc1879391219_is_of(sK12(X0,aa_TPT43085870d_bool(aTP_Lamm_aa,X1)),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X1))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa,X1))) ),
inference(forward_subsumption_resolution,[],[f3431,f967]) ).
fof(f3463,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| ~ spl27_67 ),
inference(forward_demodulation,[],[f3417,f1548]) ).
fof(f3464,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_67 ),
inference(duplicate_literal_removal,[],[f3463]) ).
fof(f3472,plain,
( pp(sF26)
| sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_67 ),
inference(forward_demodulation,[],[f3464,f1550]) ).
fof(f3480,definition,
( spl27_69
<=> sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl27_69])],[avatar_definition]) ).
fof(f3482,plain,
( sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_69 ),
inference(avatar_component_clause,[],[f3480]) ).
fof(f3488,definition,
( spl27_70
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl27_70])],[avatar_definition]) ).
fof(f3490,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl27_70 ),
inference(avatar_component_clause,[],[f3488]) ).
fof(f3492,plain,
( sK12(aTP_Lamm_a,aTP_Lamm_ab) = sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_67 ),
inference(forward_subsumption_resolution,[],[f3472,f1551]) ).
fof(f3496,plain,
( spl27_69
| ~ spl27_67 ),
inference(avatar_split_clause,[],[f3492,f3401,f3480]) ).
fof(f3502,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_69 ),
inference(superposition,[],[f3029,f3482]) ).
fof(f3545,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc301873271nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_69 ),
inference(superposition,[],[f3446,f3482]) ).
fof(f3550,plain,
( ~ scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_69 ),
inference(forward_subsumption_resolution,[],[f3545,f3502]) ).
fof(f3552,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1809285542all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_53
| ~ spl27_69 ),
inference(forward_subsumption_resolution,[],[f3550,f3053]) ).
fof(f3553,plain,
( pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_53
| ~ spl27_69 ),
inference(forward_demodulation,[],[f3552,f1548]) ).
fof(f3554,plain,
( pp(fFalse)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_53
| ~ spl27_69 ),
inference(forward_demodulation,[],[f3553,f2967]) ).
fof(f3555,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_53
| ~ spl27_69 ),
inference(forward_subsumption_resolution,[],[f3554,f1392]) ).
fof(f3556,plain,
( ~ spl27_70
| ~ spl27_53
| ~ spl27_69 ),
inference(avatar_split_clause,[],[f3555,f3480,f3052,f3488]) ).
fof(f3557,plain,
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| ~ scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl27_70 ),
inference(resolution,[],[f3490,f1828]) ).
fof(f3564,plain,
( ~ scratc1879391219_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl27_70 ),
inference(forward_subsumption_resolution,[],[f3557,f1604]) ).
fof(f3567,plain,
( $false
| ~ spl27_53
| spl27_70 ),
inference(forward_subsumption_resolution,[],[f3564,f3053]) ).
fof(f3568,plain,
( ~ spl27_53
| spl27_70 ),
inference(avatar_contradiction_clause,[],[f3567]) ).
cnf(s51,plain,
spl27_53,
inference(sat_conversion,[],[f3095]) ).
cnf(s64,plain,
spl27_67,
inference(sat_conversion,[],[f3404]) ).
cnf(s72,plain,
( ~ spl27_67
| spl27_69 ),
inference(sat_conversion,[],[f3496]) ).
cnf(s74,plain,
( ~ spl27_53
| ~ spl27_69
| ~ spl27_70 ),
inference(sat_conversion,[],[f3556]) ).
cnf(s76,plain,
( ~ spl27_53
| spl27_70 ),
inference(sat_conversion,[],[f3568]) ).
cnf(s78,plain,
spl27_69,
inference(rat,[],[s72,s64]) ).
cnf(s79,plain,
spl27_70,
inference(rat,[],[s76,s51]) ).
cnf(s80,plain,
$false,
inference(rat,[],[s74,s78,s79,s51]) ).
fof(f3570,plain,
$false,
inference(avatar_sat_refutation,[],[s80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM653+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.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 21:00:07 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.39 Running first-order theorem proving
% 0.10/0.39 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
% 5.83/1.79 % (3872809)Detected formulas, will run a generic FOF schedule.
% 5.83/1.79 % (3872814)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=625099259:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.83/1.79 % (3872817)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2795470169:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.83/1.79 % (3872816)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=1169770426:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.83/1.79 % (3872820)dis-21_1_sil=8000:lcm=predicate:random_seed=116959148: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)
% 5.83/1.79 % (3872818)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2273847667:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.83/1.79 % (3872815)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=3323983942:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.83/1.79 % (3872819)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=549859220:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.83/1.79 % (3872817)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872817)------------------------------
% 5.83/1.79 % (3872817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872817)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872817)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872817)Time elapsed: 0.002 s
% 5.83/1.79 % (3872817)Peak memory usage: 88 MB
% 5.83/1.79 % (3872817)Instructions burned: 1 (million)
% 5.83/1.79 % (3872818)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872818)------------------------------
% 5.83/1.79 % (3872818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872818)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872818)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872818)Time elapsed: 0.003 s
% 5.83/1.79 % (3872818)Peak memory usage: 88 MB
% 5.83/1.79 % (3872818)Instructions burned: 2 (million)
% 5.83/1.79 % (3872820)Instruction limit reached!
% 5.83/1.79 % (3872820)------------------------------
% 5.83/1.79 % (3872820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872820)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872820)Termination reason: Instruction limit
% 5.83/1.79 % (3872820)Termination phase: Saturation
% 5.83/1.79 % (3872820)Time elapsed: 0.078 s
% 5.83/1.79 % (3872820)Peak memory usage: 90 MB
% 5.83/1.79 % (3872820)Instructions burned: 130 (million)
% 5.83/1.79 % (3872819)Instruction limit reached!
% 5.83/1.79 % (3872819)------------------------------
% 5.83/1.79 % (3872819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872819)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872819)Termination reason: Instruction limit
% 5.83/1.79 % (3872819)Termination phase: Saturation
% 5.83/1.79 % (3872819)Time elapsed: 0.092 s
% 5.83/1.79 % (3872819)Peak memory usage: 90 MB
% 5.83/1.79 % (3872819)Instructions burned: 139 (million)
% 5.83/1.79 % (3872828)lrs+10_1_sil=8000:sp=occurrence:random_seed=1729347283:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.83/1.79 % (3872828)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872828)------------------------------
% 5.83/1.79 % (3872828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872828)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872828)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872828)Time elapsed: 0.003 s
% 5.83/1.79 % (3872828)Peak memory usage: 88 MB
% 5.83/1.79 % (3872828)Instructions burned: 2 (million)
% 5.83/1.79 % (3872829)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2607585611:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.83/1.79 % (3872829)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872829)------------------------------
% 5.83/1.79 % (3872829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872829)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872829)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872829)Time elapsed: 0.004 s
% 5.83/1.79 % (3872829)Peak memory usage: 88 MB
% 5.83/1.79 % (3872829)Instructions burned: 6 (million)
% 5.83/1.79 % (3872817)------------------------------
% 5.83/1.79 % (3872817)------------------------------
% 5.83/1.79 % (3872818)------------------------------
% 5.83/1.79 % (3872818)------------------------------
% 5.83/1.79 % (3872832)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2983607132:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 5.83/1.79 % (3872833)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=362374783:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.83/1.79 % (3872832)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872832)------------------------------
% 5.83/1.79 % (3872832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872832)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872832)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872832)Time elapsed: 0.004 s
% 5.83/1.79 % (3872832)Peak memory usage: 89 MB
% 5.83/1.79 % (3872832)Instructions burned: 4 (million)
% 5.83/1.79 % (3872828)------------------------------
% 5.83/1.79 % (3872828)------------------------------
% 5.83/1.79 % (3872829)------------------------------
% 5.83/1.79 % (3872829)------------------------------
% 5.83/1.79 % (3872833)Instruction limit reached!
% 5.83/1.79 % (3872833)------------------------------
% 5.83/1.79 % (3872833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872833)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872833)Termination reason: Instruction limit
% 5.83/1.79 % (3872833)Termination phase: Saturation
% 5.83/1.79 % (3872833)Time elapsed: 0.148 s
% 5.83/1.79 % (3872833)Peak memory usage: 93 MB
% 5.83/1.79 % (3872833)Instructions burned: 249 (million)
% 5.83/1.79 % (3872836)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1942149928:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 5.83/1.79 % (3872836)Refutation not found, incomplete strategy
% 5.83/1.79 % (3872836)------------------------------
% 5.83/1.79 % (3872836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872836)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872836)Termination reason: Refutation not found, incomplete strategy
% 5.83/1.79 % (3872836)Time elapsed: 0.004 s
% 5.83/1.79 % (3872836)Peak memory usage: 88 MB
% 5.83/1.79 % (3872836)Instructions burned: 5 (million)
% 5.83/1.79 % (3872814)First to succeed.
% 5.83/1.79 % (3872814)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3872809"
% 5.83/1.79 % (3872837)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=51438846:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.83/1.79 % (3872832)------------------------------
% 5.83/1.79 % (3872832)------------------------------
% 5.83/1.79 % (3872838)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1879452032:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 5.83/1.79 % (3872838)Instruction limit reached!
% 5.83/1.79 % (3872838)------------------------------
% 5.83/1.79 % (3872838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.83/1.79 % (3872838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.83/1.79 % (3872838)CaDiCaL version: 2.1.3
% 5.83/1.79 % (3872838)Termination reason: Instruction limit
% 5.83/1.79 % (3872838)Termination phase: Saturation
% 5.83/1.79 % (3872838)Time elapsed: 0.068 s
% 5.83/1.79 % (3872838)Peak memory usage: 90 MB
% 5.83/1.79 % (3872838)Instructions burned: 114 (million)
% 5.83/1.79 % (3872814)Refutation found. Thanks to Tanya!
% 5.83/1.79 % SZS status Theorem for theBenchmark
% 5.83/1.79 % SZS output start Proof for theBenchmark
% See solution above
% 7.08/1.88 % (3872814)------------------------------
% 7.08/1.88 % (3872814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.08/1.88 % (3872814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.08/1.88 % (3872814)CaDiCaL version: 2.1.3
% 7.08/1.88 % (3872814)Termination reason: Refutation
% 7.08/1.88 % (3872814)Time elapsed: 0.654 s
% 7.08/1.88 % (3872814)Peak memory usage: 139 MB
% 7.08/1.88 % (3872814)Instructions burned: 1746 (million)
% 7.08/1.88 % (3872814)------------------------------
% 7.08/1.88 % (3872814)------------------------------
% 7.08/1.88 % (3872809)Success in time 0.962 s
% 7.08/1.88 % Vampire exiting
%------------------------------------------------------------------------------