%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM791+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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:03 PM UTC 2026
% Result : Theorem 16.21s 3.18s
% Output : Refutation 16.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 37
% Syntax : Number of formulae : 229 ( 54 unt; 13 def)
% Number of atoms : 554 ( 56 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 552 ( 227 ~; 273 |; 23 &)
% ( 23 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 12 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 20 con; 0-2 aty)
% Number of variables : 170 ( 0 sgn 168 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f24,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(f32,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
<=> pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__rt__lessis) ).
fof(f33,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))
<=> pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__rt__moreis) ).
fof(f47,axiom,
scratc1873729523_rt_is = scratc2107463752d_e_is(scratc943171358nd_rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__rt__is) ).
fof(f128,axiom,
scratc1626124113d_n_is = scratc2107463752d_e_is(scratc910125338nd_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__is) ).
fof(f175,axiom,
! [X0] : scratc2107463752d_e_is(X0) = fequal_TPTP_ind,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__e__is) ).
fof(f185,axiom,
! [X0] : scratc1494872776d_l_or(X0) = aa_boo1142376798l_bool(scratc869604997nd_imp,scratc776381814_d_not(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__or) ).
fof(f190,axiom,
! [X0] :
( pp(scratc776381814_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc869604997nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f191,axiom,
scratc869604997nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f222,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1681461032_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f224,axiom,
pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_cc)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz81j) ).
fof(f775,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
<=> pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__244) ).
fof(f776,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
<=> pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__245) ).
fof(f857,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
<=> ( pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__326) ).
fof(f858,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__327) ).
fof(f1278,axiom,
pp(fTrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_2_1_U) ).
fof(f1282,axiom,
! [X0] :
( gg_bool(X0)
=> ( X0 = fTrue
| X0 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(f1283,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1284,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(f1285,axiom,
! [X0,X1] :
( ~ pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_2_1_U) ).
fof(f1286,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(f1288,axiom,
! [X0,X1] :
( X0 != X1
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fequal_2_1_fequal_001t__TPTP____Interpret__Oind_T) ).
fof(f1289,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(f1293,conjecture,
pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1294,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f1293]) ).
fof(f1295,plain,
~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(flattening,[],[f1294]) ).
fof(f1312,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1681461032_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f222]) ).
fof(f1313,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1681461032_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1312]) ).
fof(f1414,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))) ) ),
inference(ennf_transformation,[],[f857]) ).
fof(f1415,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))) ) ),
inference(ennf_transformation,[],[f858]) ).
fof(f1643,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ gg_bool(X0) ),
inference(ennf_transformation,[],[f1282]) ).
fof(f1644,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ gg_bool(X0) ),
inference(flattening,[],[f1643]) ).
fof(f1645,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,[],[f1289]) ).
fof(f1646,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,[],[f1645]) ).
fof(f1647,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| ~ pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ) ),
inference(nnf_transformation,[],[f32]) ).
fof(f1648,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))
| ~ pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))) )
& ( pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)) ) ),
inference(nnf_transformation,[],[f33]) ).
fof(f1712,plain,
! [X0] :
( ( pp(scratc776381814_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc869604997nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc869604997nd_imp,X0),fFalse))
| ~ pp(scratc776381814_d_not(X0)) ) ),
inference(nnf_transformation,[],[f190]) ).
fof(f1735,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1681461032_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1681461032_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1313]) ).
fof(f1736,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1681461032_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1681461032_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1)) ) ),
inference(rectify,[],[f1735]) ).
fof(f1737,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1681461032_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1681461032_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1736]) ).
fof(f2000,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
| ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) ) ),
inference(nnf_transformation,[],[f775]) ).
fof(f2001,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ) ),
inference(nnf_transformation,[],[f776]) ).
fof(f2121,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
& pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ) ),
inference(nnf_transformation,[],[f1414]) ).
fof(f2122,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
& pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ) ),
inference(flattening,[],[f2121]) ).
fof(f2123,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
& pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(nnf_transformation,[],[f1415]) ).
fof(f2124,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
& pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
| ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(flattening,[],[f2123]) ).
fof(f2704,plain,
! [X0,X1] : gg_bool(aa_TPTP_ind_bool(X0,X1)),
inference(cnf_transformation,[],[f24]) ).
fof(f2713,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| ~ pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))) ),
inference(cnf_transformation,[],[f1647]) ).
fof(f2714,plain,
! [X0,X1] :
( pp(aa_bool_bool(scratc1494872776d_l_or(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)) ),
inference(cnf_transformation,[],[f1648]) ).
fof(f2734,plain,
scratc1873729523_rt_is = scratc2107463752d_e_is(scratc943171358nd_rat),
inference(cnf_transformation,[],[f47]) ).
fof(f2847,plain,
scratc1626124113d_n_is = scratc2107463752d_e_is(scratc910125338nd_nat),
inference(cnf_transformation,[],[f128]) ).
fof(f2911,plain,
! [X0] : scratc2107463752d_e_is(X0) = fequal_TPTP_ind,
inference(cnf_transformation,[],[f175]) ).
fof(f2925,plain,
! [X0] : aa_boo1142376798l_bool(scratc869604997nd_imp,scratc776381814_d_not(X0)) = scratc1494872776d_l_or(X0),
inference(cnf_transformation,[],[f185]) ).
fof(f2931,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc869604997nd_imp,X0),fFalse))
| ~ pp(scratc776381814_d_not(X0)) ),
inference(cnf_transformation,[],[f1712]) ).
fof(f2932,plain,
! [X0] :
( pp(scratc776381814_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc869604997nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f1712]) ).
fof(f2933,plain,
scratc869604997nd_imp = fimplies,
inference(cnf_transformation,[],[f191]) ).
fof(f2995,plain,
! [X3,X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| ~ scratc1681461032_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| pp(aa_TPTP_ind_bool(X1,X3)) ),
inference(cnf_transformation,[],[f1737]) ).
fof(f2996,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1737]) ).
fof(f2997,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1))
| scratc1681461032_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1737]) ).
fof(f2998,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
| pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1737]) ).
fof(f3001,plain,
pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_cc)),
inference(cnf_transformation,[],[f224]) ).
fof(f3825,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) ),
inference(cnf_transformation,[],[f2000]) ).
fof(f3828,plain,
! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(cnf_transformation,[],[f2001]) ).
fof(f4026,plain,
! [X0,X1] :
( ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ),
inference(cnf_transformation,[],[f2122]) ).
fof(f4030,plain,
! [X0,X1] :
( pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(cnf_transformation,[],[f2124]) ).
fof(f4031,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(cnf_transformation,[],[f2124]) ).
fof(f5088,plain,
pp(fTrue),
inference(cnf_transformation,[],[f1278]) ).
fof(f5092,plain,
! [X0] :
( ~ gg_bool(X0)
| fFalse = X0
| fTrue = X0 ),
inference(cnf_transformation,[],[f1644]) ).
fof(f5093,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f1283]) ).
fof(f5094,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f1284]) ).
fof(f5095,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X1),X0))
| ~ pp(X0) ),
inference(cnf_transformation,[],[f1285]) ).
fof(f5096,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| pp(X0) ),
inference(cnf_transformation,[],[f1286]) ).
fof(f5098,plain,
! [X0,X1] :
( X0 != X1
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X0),X1)) ),
inference(cnf_transformation,[],[f1288]) ).
fof(f5099,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,[],[f1646]) ).
fof(f5103,plain,
~ pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[],[f1295]) ).
fof(f5105,plain,
! [X0] : scratc1494872776d_l_or(X0) = aa_boo1142376798l_bool(fimplies,scratc776381814_d_not(X0)),
inference(definition_unfolding,[],[f2925,f2933]) ).
fof(f5110,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ),
inference(definition_unfolding,[],[f2713,f5105]) ).
fof(f5113,plain,
! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)) ),
inference(definition_unfolding,[],[f2714,f5105]) ).
fof(f5118,plain,
scratc1873729523_rt_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f2734,f2911]) ).
fof(f5176,plain,
scratc1626124113d_n_is = fequal_TPTP_ind,
inference(definition_unfolding,[],[f2847,f2911]) ).
fof(f5203,plain,
! [X0] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| pp(scratc776381814_d_not(X0)) ),
inference(definition_unfolding,[],[f2932,f2933]) ).
fof(f5204,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| ~ pp(scratc776381814_d_not(X0)) ),
inference(definition_unfolding,[],[f2931,f2933]) ).
fof(f5451,plain,
! [X1] : pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(fequal_TPTP_ind,X1),X1)),
inference(equality_resolution,[],[f5098]) ).
fof(f5452,definition,
sF25 = scratc1473084337all_of(aTP_Lamm_a),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f5453,plain,
scratc1473084337all_of(aTP_Lamm_a) = sF25,
inference(reorient_equations,[],[f5452]) ).
fof(f5454,definition,
sF26 = aa_fun171081125l_bool(sF25,aTP_Lamm_ab),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f5455,plain,
aa_fun171081125l_bool(sF25,aTP_Lamm_ab) = sF26,
inference(reorient_equations,[],[f5454]) ).
fof(f5456,plain,
~ pp(sF26),
inference(definition_folding,[],[f5103,f5455,f5453]) ).
fof(f5508,plain,
scratc1873729523_rt_is = scratc1626124113d_n_is,
inference(forward_demodulation,[],[f5118,f5176]) ).
fof(f5530,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,[],[f3828,f5453]) ).
fof(f5533,plain,
! [X0] :
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[],[f2996,f3828]) ).
fof(f5534,plain,
! [X0] :
( pp(aa_fun171081125l_bool(sF25,X0))
| gg_TPTP_ind(sK12(aTP_Lamm_a,X0)) ),
inference(superposition,[],[f2996,f5453]) ).
fof(f5536,plain,
( pp(sF26)
| gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab)) ),
inference(superposition,[],[f5534,f5455]) ).
fof(f5537,plain,
gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab)),
inference(forward_subsumption_resolution,[],[f5536,f5456]) ).
fof(f5538,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ),
inference(superposition,[],[f5110,f5508]) ).
fof(f5539,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X1))
| X0 = X1
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1) ),
inference(superposition,[],[f5099,f5176]) ).
fof(f5540,plain,
! [X0,X1] :
( pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ),
inference(resolution,[],[f5096,f5110]) ).
fof(f5541,plain,
! [X0] :
( scratc1681461032_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,[],[f2997,f3828]) ).
fof(f5542,plain,
! [X0] :
( scratc1681461032_is_of(sK12(aTP_Lamm_a,X0),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(sF25,X0)) ),
inference(superposition,[],[f2997,f5453]) ).
fof(f5551,plain,
! [X0] : pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X0)),
inference(superposition,[],[f5451,f5176]) ).
fof(f5615,plain,
! [X0] :
( ~ pp(X0)
| pp(fFalse)
| ~ pp(scratc776381814_d_not(X0)) ),
inference(resolution,[],[f5094,f5204]) ).
fof(f5617,plain,
! [X0,X1] :
( ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1873729523_rt_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)) ),
inference(resolution,[],[f5094,f5113]) ).
fof(f5622,plain,
! [X0,X1] :
( ~ pp(scratc776381814_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1)) ),
inference(forward_demodulation,[],[f5617,f5508]) ).
fof(f5624,plain,
! [X0] :
( ~ pp(scratc776381814_d_not(X0))
| ~ pp(X0) ),
inference(forward_subsumption_resolution,[],[f5615,f5093]) ).
fof(f5626,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(resolution,[],[f5624,f4030]) ).
fof(f5627,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ),
inference(resolution,[],[f5624,f5540]) ).
fof(f5641,plain,
! [X0] :
( pp(scratc776381814_d_not(X0))
| pp(X0) ),
inference(resolution,[],[f5203,f5096]) ).
fof(f5644,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,X0),X1)) ),
inference(resolution,[],[f5641,f5622]) ).
fof(f5664,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1)) ),
inference(resolution,[],[f5095,f5538]) ).
fof(f5673,plain,
! [X0] : pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X0)),
inference(resolution,[],[f5664,f5551]) ).
fof(f5676,plain,
! [X0] : pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X0)),
inference(resolution,[],[f5673,f5626]) ).
fof(f5759,plain,
! [X0,X1] :
( aa_TPTP_ind_bool(X0,X1) = fTrue
| aa_TPTP_ind_bool(X0,X1) = fFalse ),
inference(resolution,[],[f2704,f5092]) ).
fof(f5830,plain,
! [X0,X1] :
( ~ pp(fTrue)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1) ),
inference(superposition,[],[f5627,f5759]) ).
fof(f5912,plain,
! [X0,X1] :
( ~ pp(fTrue)
| pp(aa_fun171081125l_bool(scratc1473084337all_of(X1),X0))
| fFalse = aa_TPTP_ind_bool(X0,sK12(X1,X0)) ),
inference(superposition,[],[f2998,f5759]) ).
fof(f5918,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X1),X0))
| fFalse = aa_TPTP_ind_bool(X0,sK12(X1,X0)) ),
inference(forward_subsumption_resolution,[],[f5912,f5088]) ).
fof(f5996,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1) ),
inference(forward_subsumption_resolution,[],[f5830,f5088]) ).
fof(f6002,definition,
( spl27_19
<=> ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1) ) ),
introduced(definition,[new_symbols(definition,[spl27_19])],[avatar_definition]) ).
fof(f6003,plain,
( ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc705154476lessis,X0),X1))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1) )
| ~ spl27_19 ),
inference(avatar_component_clause,[],[f6002]) ).
fof(f6024,plain,
spl27_19,
inference(avatar_split_clause,[],[f5996,f6002]) ).
fof(f6028,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,[],[f5918,f3828]) ).
fof(f6033,plain,
( ! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),X1) )
| ~ spl27_19 ),
inference(resolution,[],[f6003,f5626]) ).
fof(f6037,plain,
( ! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),sK12(X1,aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
| ~ spl27_19 ),
inference(resolution,[],[f6033,f2998]) ).
fof(f6039,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
| ~ spl27_19 ),
inference(resolution,[],[f6037,f3828]) ).
fof(f6043,plain,
( ! [X0] :
( pp(aa_fun171081125l_bool(scratc1473084337all_of(X0),aTP_Lamm_ab))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,sK12(X0,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(X0,aTP_Lamm_ab)))) )
| ~ spl27_19 ),
inference(resolution,[],[f6039,f2998]) ).
fof(f6046,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,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_19 ),
inference(superposition,[],[f6043,f5453]) ).
fof(f6048,plain,
( pp(sF26)
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,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_19 ),
inference(forward_demodulation,[],[f6046,f5455]) ).
fof(f6049,plain,
( fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,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_19 ),
inference(forward_subsumption_resolution,[],[f6048,f5456]) ).
fof(f6066,definition,
( spl27_23
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,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_23])],[avatar_definition]) ).
fof(f6067,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,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_23 ),
inference(avatar_component_clause,[],[f6066]) ).
fof(f6068,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,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_23 ),
inference(avatar_component_clause,[],[f6066]) ).
fof(f6070,definition,
( spl27_24
<=> pp(scratc776381814_d_not(fFalse)) ),
introduced(definition,[new_symbols(definition,[spl27_24])],[avatar_definition]) ).
fof(f6071,plain,
( pp(scratc776381814_d_not(fFalse))
| ~ spl27_24 ),
inference(avatar_component_clause,[],[f6070]) ).
fof(f6072,plain,
( ~ pp(scratc776381814_d_not(fFalse))
| spl27_24 ),
inference(avatar_component_clause,[],[f6070]) ).
fof(f6092,definition,
( spl27_26
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl27_26])],[avatar_definition]) ).
fof(f6093,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_26 ),
inference(avatar_component_clause,[],[f6092]) ).
fof(f6094,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl27_26 ),
inference(avatar_component_clause,[],[f6092]) ).
fof(f6096,definition,
( spl27_27
<=> scratc1681461032_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl27_27])],[avatar_definition]) ).
fof(f6097,plain,
( scratc1681461032_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a)
| ~ spl27_27 ),
inference(avatar_component_clause,[],[f6096]) ).
fof(f6098,plain,
( ~ scratc1681461032_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a)
| spl27_27 ),
inference(avatar_component_clause,[],[f6096]) ).
fof(f6100,definition,
( spl27_28
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))) ),
introduced(definition,[new_symbols(definition,[spl27_28])],[avatar_definition]) ).
fof(f6101,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_28 ),
inference(avatar_component_clause,[],[f6100]) ).
fof(f6102,plain,
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl27_28 ),
inference(avatar_component_clause,[],[f6100]) ).
fof(f6104,definition,
( spl27_29
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,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_29])],[avatar_definition]) ).
fof(f6106,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,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_29 ),
inference(avatar_component_clause,[],[f6104]) ).
fof(f6135,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)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_23 ),
inference(resolution,[],[f6068,f5539]) ).
fof(f6137,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)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_23 ),
inference(forward_subsumption_resolution,[],[f6135,f5537]) ).
fof(f6139,definition,
( spl27_32
<=> 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_32])],[avatar_definition]) ).
fof(f6141,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_32 ),
inference(avatar_component_clause,[],[f6139]) ).
fof(f6142,plain,
( ~ spl27_28
| spl27_32
| ~ spl27_23 ),
inference(avatar_split_clause,[],[f6137,f6066,f6139,f6100]) ).
fof(f6143,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl27_28 ),
inference(resolution,[],[f6102,f5533]) ).
fof(f6144,plain,
( $false
| spl27_26
| spl27_28 ),
inference(forward_subsumption_resolution,[],[f6143,f6094]) ).
fof(f6145,plain,
( spl27_26
| spl27_28 ),
inference(avatar_contradiction_clause,[],[f6144]) ).
fof(f6146,plain,
( pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aTP_Lamm_ab))
| ~ spl27_26 ),
inference(resolution,[],[f6093,f2998]) ).
fof(f6148,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| ~ spl27_26 ),
inference(forward_demodulation,[],[f6146,f5453]) ).
fof(f6149,plain,
( pp(sF26)
| ~ spl27_26 ),
inference(forward_demodulation,[],[f6148,f5455]) ).
fof(f6150,plain,
( $false
| ~ spl27_26 ),
inference(forward_subsumption_resolution,[],[f6149,f5456]) ).
fof(f6151,plain,
~ spl27_26,
inference(avatar_contradiction_clause,[],[f6150]) ).
fof(f6152,plain,
( pp(fFalse)
| spl27_24 ),
inference(resolution,[],[f6072,f5641]) ).
fof(f6153,plain,
( $false
| spl27_24 ),
inference(forward_subsumption_resolution,[],[f6152,f5093]) ).
fof(f6154,plain,
spl27_24,
inference(avatar_contradiction_clause,[],[f6153]) ).
fof(f6186,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))))
| spl27_26 ),
inference(resolution,[],[f6028,f6094]) ).
fof(f6355,definition,
( spl27_34
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,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_34])],[avatar_definition]) ).
fof(f6356,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,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_34 ),
inference(avatar_component_clause,[],[f6355]) ).
fof(f6357,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,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_34 ),
inference(avatar_component_clause,[],[f6355]) ).
fof(f6445,definition,
( spl27_37
<=> pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))) ),
introduced(definition,[new_symbols(definition,[spl27_37])],[avatar_definition]) ).
fof(f6446,plain,
( ~ pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl27_37 ),
inference(avatar_component_clause,[],[f6445]) ).
fof(f6447,plain,
( pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_37 ),
inference(avatar_component_clause,[],[f6445]) ).
fof(f6572,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_37 ),
inference(resolution,[],[f6447,f5530]) ).
fof(f6575,plain,
( $false
| spl27_26
| ~ spl27_37 ),
inference(forward_subsumption_resolution,[],[f6572,f6094]) ).
fof(f6576,plain,
( spl27_26
| ~ spl27_37 ),
inference(avatar_contradiction_clause,[],[f6575]) ).
fof(f6607,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_32 ),
inference(superposition,[],[f2998,f6141]) ).
fof(f6608,plain,
( pp(aa_fun171081125l_bool(scratc1473084337all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_32 ),
inference(forward_subsumption_resolution,[],[f6607,f5676]) ).
fof(f6617,plain,
( pp(aa_fun171081125l_bool(sF25,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl27_32 ),
inference(forward_demodulation,[],[f6608,f5453]) ).
fof(f6619,plain,
( $false
| ~ spl27_32
| spl27_37 ),
inference(forward_subsumption_resolution,[],[f6617,f6446]) ).
fof(f6620,plain,
( ~ spl27_32
| spl27_37 ),
inference(avatar_contradiction_clause,[],[f6619]) ).
fof(f6622,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1626124113d_n_is,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_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,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_34 ),
inference(resolution,[],[f6357,f5644]) ).
fof(f6624,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc133246942t_more,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_23
| ~ spl27_34 ),
inference(forward_subsumption_resolution,[],[f6622,f6067]) ).
fof(f6625,plain,
( spl27_29
| spl27_23
| ~ spl27_34 ),
inference(avatar_split_clause,[],[f6624,f6355,f6066,f6104]) ).
fof(f6654,plain,
( pp(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)))))
| ~ spl27_29 ),
inference(resolution,[],[f6106,f4031]) ).
fof(f6656,plain,
( pp(fFalse)
| spl27_26
| ~ spl27_29 ),
inference(forward_demodulation,[],[f6654,f6186]) ).
fof(f6657,plain,
( $false
| spl27_26
| ~ spl27_29 ),
inference(forward_subsumption_resolution,[],[f6656,f5093]) ).
fof(f6658,plain,
( spl27_26
| ~ spl27_29 ),
inference(avatar_contradiction_clause,[],[f6657]) ).
fof(f6663,plain,
( ~ pp(fTrue)
| fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,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_34 ),
inference(superposition,[],[f6356,f5759]) ).
fof(f6664,plain,
( fFalse = aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc839138088moreis,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_34 ),
inference(forward_subsumption_resolution,[],[f6663,f5088]) ).
fof(f7176,plain,
( ~ pp(scratc776381814_d_not(fFalse))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,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_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,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_34 ),
inference(superposition,[],[f4026,f6664]) ).
fof(f7183,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1417593954t_less,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_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,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_24
| spl27_34 ),
inference(forward_subsumption_resolution,[],[f7176,f6071]) ).
fof(f7184,plain,
( pp(fFalse)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,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_19
| ~ spl27_24
| spl27_34 ),
inference(forward_demodulation,[],[f7183,f6049]) ).
fof(f7185,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,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_19
| ~ spl27_24
| spl27_34 ),
inference(forward_subsumption_resolution,[],[f7184,f5093]) ).
fof(f11096,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc1681461032_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f3001,f2995]) ).
fof(f14398,definition,
( spl27_242
<=> scratc1681461032_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl27_242])],[avatar_definition]) ).
fof(f14399,plain,
( scratc1681461032_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl27_242 ),
inference(avatar_component_clause,[],[f14398]) ).
fof(f14400,plain,
( ~ scratc1681461032_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl27_242 ),
inference(avatar_component_clause,[],[f14398]) ).
fof(f15192,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl27_27 ),
inference(resolution,[],[f6098,f5541]) ).
fof(f15196,plain,
( $false
| spl27_26
| spl27_27 ),
inference(forward_subsumption_resolution,[],[f15192,f6094]) ).
fof(f15197,plain,
( spl27_26
| spl27_27 ),
inference(avatar_contradiction_clause,[],[f15196]) ).
fof(f15460,plain,
( pp(aa_fun171081125l_bool(sF25,aTP_Lamm_ab))
| spl27_242 ),
inference(resolution,[],[f14400,f5542]) ).
fof(f15461,plain,
( pp(sF26)
| spl27_242 ),
inference(forward_demodulation,[],[f15460,f5455]) ).
fof(f15462,plain,
( $false
| spl27_242 ),
inference(forward_subsumption_resolution,[],[f15461,f5456]) ).
fof(f15463,plain,
spl27_242,
inference(avatar_contradiction_clause,[],[f15462]) ).
fof(f17860,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
| ~ scratc1681461032_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) ),
inference(resolution,[],[f3825,f2995]) ).
fof(f17866,plain,
( ~ scratc1681461032_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_19
| ~ spl27_24
| spl27_34 ),
inference(resolution,[],[f17860,f7185]) ).
fof(f17871,plain,
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| spl27_34 ),
inference(forward_subsumption_resolution,[],[f17866,f6097]) ).
fof(f17872,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34 ),
inference(forward_subsumption_resolution,[],[f17871,f6101]) ).
fof(f17873,plain,
( ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| ~ scratc1681461032_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34 ),
inference(resolution,[],[f17872,f11096]) ).
fof(f17885,plain,
( ~ scratc1681461032_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34 ),
inference(forward_subsumption_resolution,[],[f17873,f5537]) ).
fof(f17887,plain,
( $false
| ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34
| ~ spl27_242 ),
inference(forward_subsumption_resolution,[],[f17885,f14399]) ).
fof(f17888,plain,
( ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34
| ~ spl27_242 ),
inference(avatar_contradiction_clause,[],[f17887]) ).
cnf(s24,plain,
spl27_19,
inference(sat_conversion,[],[f6024]) ).
cnf(s36,plain,
( ~ spl27_23
| ~ spl27_28
| spl27_32 ),
inference(sat_conversion,[],[f6142]) ).
cnf(s37,plain,
( spl27_26
| spl27_28 ),
inference(sat_conversion,[],[f6145]) ).
cnf(s38,plain,
~ spl27_26,
inference(sat_conversion,[],[f6151]) ).
cnf(s39,plain,
spl27_24,
inference(sat_conversion,[],[f6154]) ).
cnf(s50,plain,
( spl27_26
| ~ spl27_37 ),
inference(sat_conversion,[],[f6576]) ).
cnf(s53,plain,
( ~ spl27_32
| spl27_37 ),
inference(sat_conversion,[],[f6620]) ).
cnf(s54,plain,
( spl27_23
| spl27_29
| ~ spl27_34 ),
inference(sat_conversion,[],[f6625]) ).
cnf(s55,plain,
( spl27_26
| ~ spl27_29 ),
inference(sat_conversion,[],[f6658]) ).
cnf(s335,plain,
( spl27_26
| spl27_27 ),
inference(sat_conversion,[],[f15197]) ).
cnf(s358,plain,
spl27_242,
inference(sat_conversion,[],[f15463]) ).
cnf(s484,plain,
( ~ spl27_19
| ~ spl27_24
| ~ spl27_27
| ~ spl27_28
| spl27_34
| ~ spl27_242 ),
inference(sat_conversion,[],[f17888]) ).
cnf(s502,plain,
spl27_27,
inference(rat,[],[s335,s38]) ).
cnf(s504,plain,
~ spl27_29,
inference(rat,[],[s55,s38]) ).
cnf(s505,plain,
~ spl27_37,
inference(rat,[],[s50,s38]) ).
cnf(s509,plain,
~ spl27_32,
inference(rat,[],[s53,s505]) ).
cnf(s510,plain,
spl27_28,
inference(rat,[],[s37,s38]) ).
cnf(s515,plain,
~ spl27_23,
inference(rat,[],[s36,s509,s510]) ).
cnf(s518,plain,
~ spl27_34,
inference(rat,[],[s54,s504,s515]) ).
cnf(s523,plain,
~ spl27_19,
inference(rat,[],[s484,s358,s510,s502,s39,s518]) ).
cnf(s533,plain,
$false,
inference(rat,[],[s24,s523]) ).
fof(f17889,plain,
$false,
inference(avatar_sat_refutation,[],[s533]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM791+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.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 21:25:58 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.91/2.73 % (1318129)Detected formulas, will run a generic FOF schedule.
% 12.91/2.73 % (1318139)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1582964081:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.91/2.73 % (1318139)Instruction limit reached!
% 12.91/2.73 % (1318139)------------------------------
% 12.91/2.73 % (1318139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.91/2.73 % (1318139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.73 % (1318139)CaDiCaL version: 2.1.3
% 12.91/2.73 % (1318139)Termination reason: Instruction limit
% 12.91/2.73 % (1318139)Termination phase: Saturation
% 12.91/2.73 % (1318139)Time elapsed: 0.034 s
% 12.91/2.73 % (1318139)Peak memory usage: 91 MB
% 12.91/2.73 % (1318139)Instructions burned: 140 (million)
% 12.91/2.73 % (1318138)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1948318294:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.91/2.73 % (1318136)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=2070021146:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.91/2.73 % (1318134)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=1179283013:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.91/2.73 % (1318137)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1206554811:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.91/2.73 % (1318135)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=763123801:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.91/2.73 % (1318137)Refutation not found, incomplete strategy
% 12.91/2.73 % (1318137)------------------------------
% 12.91/2.73 % (1318137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.91/2.73 % (1318137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.73 % (1318137)CaDiCaL version: 2.1.3
% 12.91/2.73 % (1318137)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.73 % (1318137)Time elapsed: 0.005 s
% 12.91/2.73 % (1318137)Peak memory usage: 89 MB
% 12.91/2.73 % (1318137)Instructions burned: 6 (million)
% 12.91/2.73 % (1318138)Refutation not found, incomplete strategy
% 12.91/2.73 % (1318138)------------------------------
% 12.91/2.73 % (1318138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.91/2.73 % (1318138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.73 % (1318138)CaDiCaL version: 2.1.3
% 12.91/2.73 % (1318138)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.73 % (1318138)Time elapsed: 0.005 s
% 12.91/2.73 % (1318138)Peak memory usage: 89 MB
% 12.91/2.73 % (1318138)Instructions burned: 7 (million)
% 12.91/2.73 % (1318140)dis-21_1_sil=8000:lcm=predicate:random_seed=3065641138:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.91/2.73 % (1318140)Instruction limit reached!
% 12.91/2.73 % (1318140)------------------------------
% 12.91/2.73 % (1318140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.91/2.73 % (1318140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.73 % (1318140)CaDiCaL version: 2.1.3
% 12.91/2.73 % (1318140)Termination reason: Instruction limit
% 12.91/2.73 % (1318140)Termination phase: Saturation
% 12.91/2.73 % (1318140)Time elapsed: 0.057 s
% 12.91/2.73 % (1318140)Peak memory usage: 90 MB
% 12.91/2.73 % (1318140)Instructions burned: 131 (million)
% 12.91/2.73 % (1318147)lrs+10_1_sil=8000:sp=occurrence:random_seed=3029867148:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.91/2.73 % (1318147)Refutation not found, incomplete strategy
% 12.91/2.73 % (1318147)------------------------------
% 12.91/2.73 % (1318147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.91/2.73 % (1318147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.91/2.73 % (1318147)CaDiCaL version: 2.1.3
% 12.91/2.73 % (1318147)Termination reason: Refutation not found, incomplete strategy
% 12.91/2.73 % (1318147)Time elapsed: 0.003 s
% 12.91/2.73 % (1318147)Peak memory usage: 89 MB
% 12.91/2.73 % (1318147)Instructions burned: 6 (million)
% 12.91/2.73 % (1318149)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1722070130:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 16.21/3.18 % (1318137)------------------------------
% 16.21/3.18 % (1318137)------------------------------
% 16.21/3.18 % (1318138)------------------------------
% 16.21/3.18 % (1318138)------------------------------
% 16.21/3.18 % (1318149)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318149)------------------------------
% 16.21/3.18 % (1318149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318149)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318149)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318149)Time elapsed: 0.010 s
% 16.21/3.18 % (1318149)Peak memory usage: 89 MB
% 16.21/3.18 % (1318149)Instructions burned: 21 (million)
% 16.21/3.18 % (1318147)------------------------------
% 16.21/3.18 % (1318147)------------------------------
% 16.21/3.18 % (1318154)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1729104844:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 16.21/3.18 % (1318152)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1492520367:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 16.21/3.18 % (1318153)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=3165031098:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 16.21/3.18 % (1318154)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318154)------------------------------
% 16.21/3.18 % (1318154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318154)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318154)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318154)Time elapsed: 0.005 s
% 16.21/3.18 % (1318154)Peak memory usage: 89 MB
% 16.21/3.18 % (1318154)Instructions burned: 13 (million)
% 16.21/3.18 % (1318152)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318152)------------------------------
% 16.21/3.18 % (1318152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318152)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318152)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318152)Time elapsed: 0.007 s
% 16.21/3.18 % (1318152)Peak memory usage: 90 MB
% 16.21/3.18 % (1318152)Instructions burned: 8 (million)
% 16.21/3.18 % (1318149)------------------------------
% 16.21/3.18 % (1318149)------------------------------
% 16.21/3.18 % (1318153)Instruction limit reached!
% 16.21/3.18 % (1318153)------------------------------
% 16.21/3.18 % (1318153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318153)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318153)Termination reason: Instruction limit
% 16.21/3.18 % (1318153)Termination phase: Saturation
% 16.21/3.18 % (1318153)Time elapsed: 0.129 s
% 16.21/3.18 % (1318153)Peak memory usage: 96 MB
% 16.21/3.18 % (1318153)Instructions burned: 250 (million)
% 16.21/3.18 % (1318154)------------------------------
% 16.21/3.18 % (1318154)------------------------------
% 16.21/3.18 % (1318158)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=335158558:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 16.21/3.18 % (1318152)------------------------------
% 16.21/3.18 % (1318152)------------------------------
% 16.21/3.18 % (1318159)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3060711580:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 16.21/3.18 % (1318160)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1292924055:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 16.21/3.18 % (1318159)Instruction limit reached!
% 16.21/3.18 % (1318159)------------------------------
% 16.21/3.18 % (1318159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318159)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318159)Termination reason: Instruction limit
% 16.21/3.18 % (1318159)Termination phase: Saturation
% 16.21/3.18 % (1318159)Time elapsed: 0.056 s
% 16.21/3.18 % (1318159)Peak memory usage: 90 MB
% 16.21/3.18 % (1318159)Instructions burned: 115 (million)
% 16.21/3.18 % (1318160)Instruction limit reached!
% 16.21/3.18 % (1318160)------------------------------
% 16.21/3.18 % (1318160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318160)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318160)Termination reason: Instruction limit
% 16.21/3.18 % (1318160)Termination phase: Property scanning
% 16.21/3.18 % (1318160)Time elapsed: 0.057 s
% 16.21/3.18 % (1318160)Peak memory usage: 89 MB
% 16.21/3.18 % (1318160)Instructions burned: 127 (million)
% 16.21/3.18 % (1318162)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=751590407:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 16.21/3.18 % (1318162)Instruction limit reached!
% 16.21/3.18 % (1318162)------------------------------
% 16.21/3.18 % (1318162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318162)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318162)Termination reason: Instruction limit
% 16.21/3.18 % (1318162)Termination phase: Saturation
% 16.21/3.18 % (1318162)Time elapsed: 0.058 s
% 16.21/3.18 % (1318162)Peak memory usage: 90 MB
% 16.21/3.18 % (1318162)Instructions burned: 114 (million)
% 16.21/3.18 % (1318165)lrs+10_1_sil=8000:sp=occurrence:random_seed=2587700112:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 16.21/3.18 % (1318166)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2676097577:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 16.21/3.18 % (1318168)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3599687223:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 16.21/3.18 % (1318166)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318166)------------------------------
% 16.21/3.18 % (1318166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318166)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318166)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318166)Time elapsed: 0.094 s
% 16.21/3.18 % (1318166)Peak memory usage: 93 MB
% 16.21/3.18 % (1318166)Instructions burned: 193 (million)
% 16.21/3.18 % (1318166)------------------------------
% 16.21/3.18 % (1318166)------------------------------
% 16.21/3.18 % (1318172)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1154492110:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 16.21/3.18 % (1318165)Instruction limit reached!
% 16.21/3.18 % (1318165)------------------------------
% 16.21/3.18 % (1318165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318165)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318165)Termination reason: Instruction limit
% 16.21/3.18 % (1318165)Termination phase: Saturation
% 16.21/3.18 % (1318165)Time elapsed: 0.539 s
% 16.21/3.18 % (1318165)Peak memory usage: 102 MB
% 16.21/3.18 % (1318165)Instructions burned: 908 (million)
% 16.21/3.18 % (1318172)Instruction limit reached!
% 16.21/3.18 % (1318172)------------------------------
% 16.21/3.18 % (1318172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318172)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318172)Termination reason: Instruction limit
% 16.21/3.18 % (1318172)Termination phase: Saturation
% 16.21/3.18 % (1318172)Time elapsed: 0.062 s
% 16.21/3.18 % (1318172)Peak memory usage: 91 MB
% 16.21/3.18 % (1318172)Instructions burned: 136 (million)
% 16.21/3.18 % (1318174)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3001998362:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 16.21/3.18 % (1318174)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318174)------------------------------
% 16.21/3.18 % (1318174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318174)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318174)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318174)Time elapsed: 0.022 s
% 16.21/3.18 % (1318174)Peak memory usage: 90 MB
% 16.21/3.18 % (1318174)Instructions burned: 40 (million)
% 16.21/3.18 % (1318175)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1978374112:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 16.21/3.18 % (1318174)------------------------------
% 16.21/3.18 % (1318174)------------------------------
% 16.21/3.18 % (1318134)First to succeed.
% 16.21/3.18 % (1318134)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1318129"
% 16.21/3.18 % (1318136)Also succeeded, but the first one will report.
% 16.21/3.18 % (1318158)Instruction limit reached!
% 16.21/3.18 % (1318158)------------------------------
% 16.21/3.18 % (1318158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318158)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318158)Termination reason: Instruction limit
% 16.21/3.18 % (1318158)Termination phase: Saturation
% 16.21/3.18 % (1318158)Time elapsed: 1.383 s
% 16.21/3.18 % (1318158)Peak memory usage: 167 MB
% 16.21/3.18 % (1318158)Instructions burned: 2350 (million)
% 16.21/3.18 % (1318242)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=2250913378:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 16.21/3.18 % (1318168)Also succeeded, but the first one will report.
% 16.21/3.18 % (1318242)Refutation not found, incomplete strategy
% 16.21/3.18 % (1318242)------------------------------
% 16.21/3.18 % (1318242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.21/3.18 % (1318242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.21/3.18 % (1318242)CaDiCaL version: 2.1.3
% 16.21/3.18 % (1318242)Termination reason: Refutation not found, incomplete strategy
% 16.21/3.18 % (1318242)Time elapsed: 0.015 s
% 16.21/3.18 % (1318242)Peak memory usage: 90 MB
% 16.21/3.18 % (1318242)Instructions burned: 28 (million)
% 16.21/3.18 % (1318134)Refutation found. Thanks to Tanya!
% 16.21/3.18 % SZS status Theorem for theBenchmark
% 16.21/3.18 % SZS output start Proof for theBenchmark
% See solution above
% 16.67/3.37 % (1318134)------------------------------
% 16.67/3.37 % (1318134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.67/3.37 % (1318134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.67/3.37 % (1318134)CaDiCaL version: 2.1.3
% 16.67/3.37 % (1318134)Termination reason: Refutation
% 16.67/3.37 % (1318134)Time elapsed: 1.938 s
% 16.67/3.37 % (1318134)Peak memory usage: 167 MB
% 16.67/3.37 % (1318134)Instructions burned: 4811 (million)
% 16.67/3.37 % (1318134)------------------------------
% 16.67/3.37 % (1318134)------------------------------
% 16.67/3.37 % (1318129)Success in time 2.334 s
% 16.67/3.37 % Vampire exiting
%------------------------------------------------------------------------------