%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM749+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:48 PM UTC 2026
% Result : Theorem 13.70s 2.96s
% Output : Refutation 15.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 28
% Syntax : Number of formulae : 152 ( 26 unt; 15 def)
% Number of atoms : 357 ( 2 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 348 ( 143 ~; 153 |; 21 &)
% ( 28 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 16 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 15 con; 0-2 aty)
% Number of variables : 97 ( 0 sgn 95 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__lessf) ).
fof(f35,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__moref) ).
fof(f67,axiom,
! [X0] : scratc1464707514d_n_ts(X0) = aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__n__ts) ).
fof(f80,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X1),X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f81,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f199,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc2064974964_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f201,axiom,
pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_by)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz60) ).
fof(f601,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0))
<=> pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__168) ).
fof(f602,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
<=> pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__169) ).
fof(f649,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__216) ).
fof(f663,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1)),X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__230) ).
fof(f679,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__246) ).
fof(f957,conjecture,
pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f958,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f957]) ).
fof(f959,plain,
~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(flattening,[],[f958]) ).
fof(f976,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc2064974964_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f199]) ).
fof(f977,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc2064974964_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f976]) ).
fof(f1055,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ) ),
inference(ennf_transformation,[],[f649]) ).
fof(f1217,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),X1)) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f1218,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ) ),
inference(nnf_transformation,[],[f35]) ).
fof(f1232,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f1233,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f1296,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc2064974964_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc2064974964_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f977]) ).
fof(f1297,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc2064974964_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc2064974964_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1)) ) ),
inference(rectify,[],[f1296]) ).
fof(f1298,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc2064974964_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc2064974964_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1297]) ).
fof(f1485,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0)) ) ),
inference(nnf_transformation,[],[f601]) ).
fof(f1486,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ) ),
inference(nnf_transformation,[],[f602]) ).
fof(f1551,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1)) ) ),
inference(nnf_transformation,[],[f1055]) ).
fof(f1552,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1)) ) ),
inference(flattening,[],[f1551]) ).
fof(f1578,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1)),X0)) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1)),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1)) ) ),
inference(nnf_transformation,[],[f663]) ).
fof(f1599,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1))) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(nnf_transformation,[],[f679]) ).
fof(f1973,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) ),
inference(cnf_transformation,[],[f1217]) ).
fof(f1974,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(scratc1464707514d_n_ts(aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1)),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ),
inference(cnf_transformation,[],[f1218]) ).
fof(f2011,plain,
! [X0] : scratc1464707514d_n_ts(X0) = aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,X0)),
inference(cnf_transformation,[],[f67]) ).
fof(f2034,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f1232]) ).
fof(f2035,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f1233]) ).
fof(f2221,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc2064974964_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f2222,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f2223,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| scratc2064974964_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f2224,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1298]) ).
fof(f2227,plain,
pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_by)),
inference(cnf_transformation,[],[f201]) ).
fof(f2824,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0)) ),
inference(cnf_transformation,[],[f1485]) ).
fof(f2827,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
inference(cnf_transformation,[],[f1486]) ).
fof(f2936,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1)) ),
inference(cnf_transformation,[],[f1552]) ).
fof(f2937,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ),
inference(cnf_transformation,[],[f1552]) ).
fof(f2977,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1)),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1)) ),
inference(cnf_transformation,[],[f1578]) ).
fof(f3015,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(X0),X1))) ),
inference(cnf_transformation,[],[f1599]) ).
fof(f3682,plain,
~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[],[f959]) ).
fof(f3694,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0)))) ),
inference(definition_unfolding,[],[f1973,f2011,f2011]) ).
fof(f3697,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X0))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X1))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,X1))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,X0))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,X0),X1)) ),
inference(definition_unfolding,[],[f1974,f2011,f2011]) ).
fof(f4027,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f4029,plain,
( ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_ab))
| spl29_1 ),
inference(avatar_component_clause,[],[f4027]) ).
fof(f4030,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f3682,f4027]) ).
fof(f4031,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| spl29_1 ),
inference(resolution,[],[f4029,f2222]) ).
fof(f4032,plain,
( scratc2064974964_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f4029,f2223]) ).
fof(f4033,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_1 ),
inference(resolution,[],[f4029,f2224]) ).
fof(f4046,definition,
( spl29_2
<=> scratc2064974964_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f4048,plain,
( scratc2064974964_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f4046]) ).
fof(f4049,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f4032,f4027,f4046]) ).
fof(f4051,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f4048,f2221]) ).
fof(f4052,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f4051,f4031]) ).
fof(f4054,definition,
( spl29_3
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f4055,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f4054]) ).
fof(f4056,plain,
( spl29_3
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f4052,f4046,f4027,f4054]) ).
fof(f4717,plain,
( ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aTP_Lamm_by))
| pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl29_3 ),
inference(resolution,[],[f4055,f2824]) ).
fof(f4937,plain,
( pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f4717,f2227]) ).
fof(f5014,definition,
( spl29_5
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f5016,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_5 ),
inference(avatar_component_clause,[],[f5014]) ).
fof(f5017,plain,
( ~ spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f4033,f4027,f5014]) ).
fof(f5018,plain,
( ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl29_5 ),
inference(resolution,[],[f5016,f2827]) ).
fof(f5057,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f5059,plain,
( ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl29_6 ),
inference(avatar_component_clause,[],[f5057]) ).
fof(f5060,plain,
( ~ spl29_6
| spl29_5 ),
inference(avatar_split_clause,[],[f5018,f5014,f5057]) ).
fof(f5062,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl29_6 ),
inference(resolution,[],[f5059,f2222]) ).
fof(f5063,plain,
( scratc2064974964_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a)
| spl29_6 ),
inference(resolution,[],[f5059,f2223]) ).
fof(f5064,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)))))
| spl29_6 ),
inference(resolution,[],[f5059,f2224]) ).
fof(f5077,definition,
( spl29_7
<=> scratc2064974964_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,[spl29_7])],[avatar_definition]) ).
fof(f5079,plain,
( scratc2064974964_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))),aTP_Lamm_a)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f5077]) ).
fof(f5080,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f5063,f5057,f5077]) ).
fof(f5082,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,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))))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f5079,f2221]) ).
fof(f5083,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f5082,f5062]) ).
fof(f5085,definition,
( spl29_8
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f5086,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),X0)) )
| ~ spl29_8 ),
inference(avatar_component_clause,[],[f5085]) ).
fof(f5087,plain,
( spl29_8
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f5083,f5077,f5057,f5085]) ).
fof(f6040,definition,
( spl29_9
<=> 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))))) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f6042,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)))))
| spl29_9 ),
inference(avatar_component_clause,[],[f6040]) ).
fof(f6043,plain,
( ~ spl29_9
| spl29_6 ),
inference(avatar_split_clause,[],[f5064,f5057,f6040]) ).
fof(f6044,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ab)),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| spl29_9 ),
inference(resolution,[],[f6042,f3015]) ).
fof(f6280,definition,
( spl29_12
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ab)),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(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,[spl29_12])],[avatar_definition]) ).
fof(f6282,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1886782970_lessf,sK12(aTP_Lamm_a,aTP_Lamm_ab)),aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| spl29_12 ),
inference(avatar_component_clause,[],[f6280]) ).
fof(f6283,plain,
( ~ spl29_12
| spl29_9 ),
inference(avatar_split_clause,[],[f6044,f6040,f6280]) ).
fof(f6285,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_12 ),
inference(resolution,[],[f6282,f2936]) ).
fof(f6300,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| spl29_12 ),
inference(resolution,[],[f6282,f3694]) ).
fof(f6346,definition,
( spl29_13
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f6348,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_fa,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_13 ),
inference(avatar_component_clause,[],[f6346]) ).
fof(f6350,definition,
( spl29_14
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl29_14])],[avatar_definition]) ).
fof(f6352,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_14 ),
inference(avatar_component_clause,[],[f6350]) ).
fof(f6353,plain,
( ~ spl29_13
| ~ spl29_14
| spl29_12 ),
inference(avatar_split_clause,[],[f6285,f6280,f6350,f6346]) ).
fof(f6354,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_13 ),
inference(resolution,[],[f6348,f2937]) ).
fof(f6402,definition,
( spl29_15
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f6404,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1883025206nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| spl29_15 ),
inference(avatar_component_clause,[],[f6402]) ).
fof(f6405,plain,
( ~ spl29_15
| spl29_12 ),
inference(avatar_split_clause,[],[f6300,f6280,f6402]) ).
fof(f6412,plain,
( ~ pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))))))
| spl29_15 ),
inference(resolution,[],[f6404,f2034]) ).
fof(f6492,definition,
( spl29_16
<=> pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(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,[spl29_16])],[avatar_definition]) ).
fof(f6494,plain,
( ~ pp(aa_fun171081125l_bool(scratc1687058735n_some,aa_TPT43085870d_bool(scratc276310267ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))))))
| spl29_16 ),
inference(avatar_component_clause,[],[f6492]) ).
fof(f6495,plain,
( ~ spl29_16
| spl29_15 ),
inference(avatar_split_clause,[],[f6412,f6402,f6492]) ).
fof(f6496,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))))
| spl29_16 ),
inference(resolution,[],[f6494,f2035]) ).
fof(f6510,definition,
( spl29_17
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(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,[spl29_17])],[avatar_definition]) ).
fof(f6512,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1744436536_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1747045378bnd_ap,aa_TPTP_ind_TPTP_ind(scratc1190256787_times,aa_TPTP_ind_TPTP_ind(scratc1925119923nd_num,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),aa_TPTP_ind_TPTP_ind(scratc1841455290nd_den,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))))
| spl29_17 ),
inference(avatar_component_clause,[],[f6510]) ).
fof(f6513,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f6496,f6492,f6510]) ).
fof(f6514,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc85621118_moref,aa_TPTP_ind_TPTP_ind(scratc1464445105d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_17 ),
inference(resolution,[],[f6512,f3697]) ).
fof(f6596,plain,
( $false
| spl29_13
| spl29_17 ),
inference(forward_subsumption_resolution,[],[f6514,f6354]) ).
fof(f6597,plain,
( spl29_13
| spl29_17 ),
inference(avatar_contradiction_clause,[],[f6596]) ).
fof(f6611,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| spl29_14 ),
inference(resolution,[],[f6352,f2977]) ).
fof(f6936,definition,
( spl29_27
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,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,[spl29_27])],[avatar_definition]) ).
fof(f6938,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| spl29_27 ),
inference(avatar_component_clause,[],[f6936]) ).
fof(f6939,plain,
( ~ spl29_27
| spl29_14 ),
inference(avatar_split_clause,[],[f6611,f6350,f6936]) ).
fof(f7132,plain,
( ~ pp(aa_fun171081125l_bool(scratc1832573285all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| ~ spl29_8
| spl29_27 ),
inference(resolution,[],[f6938,f5086]) ).
fof(f7171,plain,
( $false
| ~ spl29_3
| ~ spl29_8
| spl29_27 ),
inference(forward_subsumption_resolution,[],[f7132,f4937]) ).
fof(f7172,plain,
( ~ spl29_3
| ~ spl29_8
| spl29_27 ),
inference(avatar_contradiction_clause,[],[f7171]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f4030]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f4049]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_2
| spl29_3 ),
inference(sat_conversion,[],[f4056]) ).
cnf(s5,plain,
( spl29_1
| ~ spl29_5 ),
inference(sat_conversion,[],[f5017]) ).
cnf(s6,plain,
( spl29_5
| ~ spl29_6 ),
inference(sat_conversion,[],[f5060]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f5080]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_7
| spl29_8 ),
inference(sat_conversion,[],[f5087]) ).
cnf(s9,plain,
( spl29_6
| ~ spl29_9 ),
inference(sat_conversion,[],[f6043]) ).
cnf(s12,plain,
( spl29_9
| ~ spl29_12 ),
inference(sat_conversion,[],[f6283]) ).
cnf(s13,plain,
( spl29_12
| ~ spl29_13
| ~ spl29_14 ),
inference(sat_conversion,[],[f6353]) ).
cnf(s14,plain,
( spl29_12
| ~ spl29_15 ),
inference(sat_conversion,[],[f6405]) ).
cnf(s15,plain,
( spl29_15
| ~ spl29_16 ),
inference(sat_conversion,[],[f6495]) ).
cnf(s16,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f6513]) ).
cnf(s17,plain,
( spl29_13
| spl29_17 ),
inference(sat_conversion,[],[f6597]) ).
cnf(s25,plain,
( spl29_14
| ~ spl29_27 ),
inference(sat_conversion,[],[f6939]) ).
cnf(s35,plain,
( ~ spl29_3
| ~ spl29_8
| spl29_27 ),
inference(sat_conversion,[],[f7172]) ).
cnf(s36,plain,
~ spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s38,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s40,plain,
~ spl29_6,
inference(rat,[],[s6,s36]) ).
cnf(s43,plain,
spl29_3,
inference(rat,[],[s3,s1,s38]) ).
cnf(s45,plain,
~ spl29_9,
inference(rat,[],[s9,s40]) ).
cnf(s46,plain,
spl29_7,
inference(rat,[],[s7,s40]) ).
cnf(s55,plain,
~ spl29_12,
inference(rat,[],[s12,s45]) ).
cnf(s57,plain,
spl29_8,
inference(rat,[],[s8,s40,s46]) ).
cnf(s59,plain,
~ spl29_15,
inference(rat,[],[s14,s55]) ).
cnf(s60,plain,
spl29_27,
inference(rat,[],[s35,s43,s57]) ).
cnf(s63,plain,
~ spl29_16,
inference(rat,[],[s15,s59]) ).
cnf(s64,plain,
spl29_14,
inference(rat,[],[s25,s60]) ).
cnf(s65,plain,
~ spl29_17,
inference(rat,[],[s16,s63]) ).
cnf(s66,plain,
~ spl29_13,
inference(rat,[],[s13,s55,s64]) ).
cnf(s67,plain,
$false,
inference(rat,[],[s17,s65,s66]) ).
fof(f7173,plain,
$false,
inference(avatar_sat_refutation,[],[s67]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM749+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.40 % Computer : n008.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 21:16:55 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.18/2.65 % (1606985)Detected formulas, will run a generic FOF schedule.
% 12.18/2.65 % (1606993)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=652023345:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.18/2.65 % (1606993)Refutation not found, incomplete strategy
% 12.18/2.65 % (1606993)------------------------------
% 12.18/2.65 % (1606993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.65 % (1606993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.65 % (1606993)CaDiCaL version: 2.1.3
% 12.18/2.65 % (1606993)Termination reason: Refutation not found, incomplete strategy
% 12.18/2.65 % (1606993)Time elapsed: 0.002 s
% 12.18/2.65 % (1606993)Peak memory usage: 88 MB
% 12.18/2.65 % (1606993)Instructions burned: 4 (million)
% 12.18/2.65 % (1606994)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4199492039:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.18/2.65 % (1606996)dis-21_1_sil=8000:lcm=predicate:random_seed=2651180486: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.18/2.65 % (1606995)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=368046696:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.18/2.65 % (1606992)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=3822931337:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.18/2.65 % (1606990)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=1458083849:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.18/2.65 % (1606991)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=3954813120:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.18/2.65 % (1606994)Refutation not found, incomplete strategy
% 12.18/2.65 % (1606994)------------------------------
% 12.18/2.65 % (1606994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.65 % (1606994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.65 % (1606994)CaDiCaL version: 2.1.3
% 12.18/2.65 % (1606994)Termination reason: Refutation not found, incomplete strategy
% 12.18/2.65 % (1606994)Time elapsed: 0.004 s
% 12.18/2.65 % (1606994)Peak memory usage: 88 MB
% 12.18/2.65 % (1606994)Instructions burned: 4 (million)
% 12.18/2.65 % (1606996)Instruction limit reached!
% 12.18/2.65 % (1606996)------------------------------
% 12.18/2.65 % (1606996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.65 % (1606996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.65 % (1606996)CaDiCaL version: 2.1.3
% 12.18/2.65 % (1606996)Termination reason: Instruction limit
% 12.18/2.65 % (1606996)Termination phase: Saturation
% 12.18/2.65 % (1606996)Time elapsed: 0.061 s
% 12.18/2.65 % (1606996)Peak memory usage: 90 MB
% 12.18/2.65 % (1606996)Instructions burned: 130 (million)
% 12.18/2.65 % (1606995)Instruction limit reached!
% 12.18/2.65 % (1606995)------------------------------
% 12.18/2.65 % (1606995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.65 % (1606995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.65 % (1606995)CaDiCaL version: 2.1.3
% 12.18/2.65 % (1606995)Termination reason: Instruction limit
% 12.18/2.65 % (1606995)Termination phase: Saturation
% 12.18/2.65 % (1606995)Time elapsed: 0.070 s
% 12.18/2.65 % (1606995)Peak memory usage: 91 MB
% 12.18/2.65 % (1606995)Instructions burned: 139 (million)
% 12.18/2.65 % (1606993)------------------------------
% 12.18/2.65 % (1606993)------------------------------
% 12.18/2.65 % (1607004)lrs+10_1_sil=8000:sp=occurrence:random_seed=1505244152:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.18/2.65 % (1607004)Refutation not found, incomplete strategy
% 12.18/2.65 % (1607004)------------------------------
% 12.18/2.65 % (1607004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.18/2.65 % (1607004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.18/2.65 % (1607004)CaDiCaL version: 2.1.3
% 12.18/2.65 % (1607004)Termination reason: Refutation not found, incomplete strategy
% 12.18/2.65 % (1607004)Time elapsed: 0.013 s
% 12.18/2.65 % (1607004)Peak memory usage: 89 MB
% 13.70/2.95 % (1607004)Instructions burned: 19 (million)
% 13.70/2.95 % (1607005)lrs+10_1_sil=32000:urr=on:br=off:random_seed=958834897:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.70/2.95 % (1607006)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2512061275:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 13.70/2.95 % (1607005)Refutation not found, incomplete strategy
% 13.70/2.95 % (1607005)------------------------------
% 13.70/2.95 % (1607005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607005)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607005)Termination reason: Refutation not found, incomplete strategy
% 13.70/2.95 % (1607005)Time elapsed: 0.008 s
% 13.70/2.95 % (1607005)Peak memory usage: 89 MB
% 13.70/2.95 % (1607005)Instructions burned: 15 (million)
% 13.70/2.95 % (1607006)Refutation not found, incomplete strategy
% 13.70/2.95 % (1607006)------------------------------
% 13.70/2.95 % (1607006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607006)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607006)Termination reason: Refutation not found, incomplete strategy
% 13.70/2.95 % (1607006)Time elapsed: 0.003 s
% 13.70/2.95 % (1607006)Peak memory usage: 89 MB
% 13.70/2.95 % (1607006)Instructions burned: 7 (million)
% 13.70/2.95 % (1606994)------------------------------
% 13.70/2.95 % (1606994)------------------------------
% 13.70/2.95 % (1607006)------------------------------
% 13.70/2.95 % (1607006)------------------------------
% 13.70/2.95 % (1607010)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=2084473496:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.70/2.95 % (1607004)------------------------------
% 13.70/2.95 % (1607004)------------------------------
% 13.70/2.95 % (1607005)------------------------------
% 13.70/2.95 % (1607005)------------------------------
% 13.70/2.95 % (1607011)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3704294116:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 13.70/2.95 % (1607011)Refutation not found, incomplete strategy
% 13.70/2.95 % (1607011)------------------------------
% 13.70/2.95 % (1607011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607011)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607011)Termination reason: Refutation not found, incomplete strategy
% 13.70/2.95 % (1607011)Time elapsed: 0.004 s
% 13.70/2.95 % (1607011)Peak memory usage: 89 MB
% 13.70/2.95 % (1607011)Instructions burned: 10 (million)
% 13.70/2.95 % (1607010)Instruction limit reached!
% 13.70/2.95 % (1607010)------------------------------
% 13.70/2.95 % (1607010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607010)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607010)Termination reason: Instruction limit
% 13.70/2.95 % (1607010)Termination phase: Saturation
% 13.70/2.95 % (1607010)Time elapsed: 0.144 s
% 13.70/2.95 % (1607010)Peak memory usage: 92 MB
% 13.70/2.95 % (1607010)Instructions burned: 249 (million)
% 13.70/2.95 % (1607014)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2216273482:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 13.70/2.95 % (1607015)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4228912753:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 13.70/2.95 % (1607011)------------------------------
% 13.70/2.95 % (1607011)------------------------------
% 13.70/2.95 % (1607015)Instruction limit reached!
% 13.70/2.95 % (1607015)------------------------------
% 13.70/2.95 % (1607015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607015)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607015)Termination reason: Instruction limit
% 13.70/2.95 % (1607015)Termination phase: Saturation
% 13.70/2.95 % (1607015)Time elapsed: 0.058 s
% 13.70/2.95 % (1607015)Peak memory usage: 90 MB
% 13.70/2.95 % (1607015)Instructions burned: 115 (million)
% 13.70/2.95 % (1607017)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3160803604:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 13.70/2.95 % (1607020)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1648150213:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 13.70/2.95 % (1607017)Instruction limit reached!
% 13.70/2.95 % (1607017)------------------------------
% 13.70/2.95 % (1607017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607017)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607017)Termination reason: Instruction limit
% 13.70/2.95 % (1607017)Termination phase: Saturation
% 13.70/2.95 % (1607017)Time elapsed: 0.058 s
% 13.70/2.95 % (1607017)Peak memory usage: 90 MB
% 13.70/2.95 % (1607017)Instructions burned: 128 (million)
% 13.70/2.95 % (1607020)Instruction limit reached!
% 13.70/2.95 % (1607020)------------------------------
% 13.70/2.95 % (1607020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.95 % (1607020)CaDiCaL version: 2.1.3
% 13.70/2.95 % (1607020)Termination reason: Instruction limit
% 13.70/2.95 % (1607020)Termination phase: Saturation
% 13.70/2.95 % (1607020)Time elapsed: 0.033 s
% 13.70/2.95 % (1607020)Peak memory usage: 90 MB
% 13.70/2.95 % (1607020)Instructions burned: 116 (million)
% 13.70/2.95 % (1607021)lrs+10_1_sil=8000:sp=occurrence:random_seed=1538061986:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 13.70/2.95 % (1607024)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1413503641:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 13.70/2.95 % (1607025)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=138343582:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 13.70/2.95 % (1607024)Refutation not found, incomplete strategy
% 13.70/2.95 % (1607024)------------------------------
% 13.70/2.95 % (1607024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.95 % (1607024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.96 % (1607024)CaDiCaL version: 2.1.3
% 13.70/2.96 % (1607024)Termination reason: Refutation not found, incomplete strategy
% 13.70/2.96 % (1607024)Time elapsed: 0.067 s
% 13.70/2.96 % (1607024)Peak memory usage: 92 MB
% 13.70/2.96 % (1607024)Instructions burned: 138 (million)
% 13.70/2.96 % (1607024)------------------------------
% 13.70/2.96 % (1607024)------------------------------
% 13.70/2.96 % (1607021)Instruction limit reached!
% 13.70/2.96 % (1607021)------------------------------
% 13.70/2.96 % (1607021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.96 % (1607021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.96 % (1607021)CaDiCaL version: 2.1.3
% 13.70/2.96 % (1607021)Termination reason: Instruction limit
% 13.70/2.96 % (1607021)Termination phase: Saturation
% 13.70/2.96 % (1607021)Time elapsed: 0.527 s
% 13.70/2.96 % (1607021)Peak memory usage: 102 MB
% 13.70/2.96 % (1607021)Instructions burned: 908 (million)
% 13.70/2.96 % (1607029)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=679516755:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 13.70/2.96 % (1607029)Instruction limit reached!
% 13.70/2.96 % (1607029)------------------------------
% 13.70/2.96 % (1607029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.96 % (1607029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.96 % (1607029)CaDiCaL version: 2.1.3
% 13.70/2.96 % (1607029)Termination reason: Instruction limit
% 13.70/2.96 % (1607029)Termination phase: Saturation
% 13.70/2.96 % (1607029)Time elapsed: 0.068 s
% 13.70/2.96 % (1607029)Peak memory usage: 92 MB
% 13.70/2.96 % (1607029)Instructions burned: 136 (million)
% 13.70/2.96 % (1607030)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3713370946:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 13.70/2.96 % (1607030)Refutation not found, incomplete strategy
% 13.70/2.96 % (1607030)------------------------------
% 13.70/2.96 % (1607030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.70/2.96 % (1607030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.70/2.96 % (1607030)CaDiCaL version: 2.1.3
% 13.70/2.96 % (1607030)Termination reason: Refutation not found, incomplete strategy
% 13.70/2.96 % (1607030)Time elapsed: 0.018 s
% 13.70/2.96 % (1607030)Peak memory usage: 89 MB
% 13.70/2.96 % (1607030)Instructions burned: 33 (million)
% 13.70/2.96 % (1606992)First to succeed.
% 13.70/2.96 % (1606992)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1606985"
% 13.70/2.96 % (1607032)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1359752090:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 13.70/2.96 % (1607030)------------------------------
% 13.70/2.96 % (1607030)------------------------------
% 13.70/2.96 % (1606992)Refutation found. Thanks to Tanya!
% 13.70/2.96 % SZS status Theorem for theBenchmark
% 13.70/2.96 % SZS output start Proof for theBenchmark
% See solution above
% 15.02/3.15 % (1606992)------------------------------
% 15.02/3.15 % (1606992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.02/3.15 % (1606992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.02/3.15 % (1606992)CaDiCaL version: 2.1.3
% 15.02/3.15 % (1606992)Termination reason: Refutation
% 15.02/3.15 % (1606992)Time elapsed: 1.600 s
% 15.02/3.15 % (1606992)Peak memory usage: 152 MB
% 15.02/3.15 % (1606992)Instructions burned: 2785 (million)
% 15.02/3.15 % (1606992)------------------------------
% 15.02/3.15 % (1606992)------------------------------
% 15.02/3.15 % (1606985)Success in time 2.074 s
% 15.02/3.15 % Vampire exiting
%------------------------------------------------------------------------------