%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM665+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 : n007.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:19 PM UTC 2026
% Result : Theorem 29.12s 5.04s
% Output : Refutation 30.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 14
% Syntax : Number of formulae : 100 ( 10 unt; 0 def)
% Number of atoms : 375 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 484 ( 209 ~; 218 |; 32 &)
% ( 18 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-2 aty)
% Number of variables : 201 ( 199 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X1),X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f29,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc268048172_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f149,axiom,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_bt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz16b) ).
fof(f161,axiom,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ct)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz13) ).
fof(f288,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0))
<=> pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__34) ).
fof(f300,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0))
<=> pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__46) ).
fof(f301,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__47) ).
fof(f322,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__68) ).
fof(f349,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__95) ).
fof(f350,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__96) ).
fof(f367,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__113) ).
fof(f370,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__116) ).
fof(f428,conjecture,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f429,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f428]) ).
fof(f430,plain,
~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f429]) ).
fof(f457,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f370]) ).
fof(f458,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ) ),
inference(flattening,[],[f457]) ).
fof(f467,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f367]) ).
fof(f468,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) ),
inference(flattening,[],[f467]) ).
fof(f508,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f322]) ).
fof(f509,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc268048172_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f510,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc268048172_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f509]) ).
fof(f549,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f301]) ).
fof(f572,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1)) ) ),
inference(nnf_transformation,[],[f350]) ).
fof(f588,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f589,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f594,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f458]) ).
fof(f595,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2)) ) ),
inference(flattening,[],[f594]) ).
fof(f612,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f468]) ).
fof(f613,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f612]) ).
fof(f718,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1)) ) ),
inference(nnf_transformation,[],[f508]) ).
fof(f719,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1)) ) ),
inference(flattening,[],[f718]) ).
fof(f720,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1)) ) ),
inference(nnf_transformation,[],[f349]) ).
fof(f740,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc268048172_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc268048172_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f510]) ).
fof(f741,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc268048172_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc268048172_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1)) ) ),
inference(rectify,[],[f740]) ).
fof(f742,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK11(X0,X1)))
& scratc268048172_is_of(sK11(X0,X1),X0)
& gg_TPTP_ind(sK11(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc268048172_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11(X0,X1))],[f741]) ).
fof(f781,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0))
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs,X0))) )
& ( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ) ),
inference(nnf_transformation,[],[f288]) ).
fof(f782,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0))
| ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0))) )
& ( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0)) ) ),
inference(nnf_transformation,[],[f300]) ).
fof(f800,plain,
~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f430]) ).
fof(f815,plain,
! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ),
inference(cnf_transformation,[],[f549]) ).
fof(f865,plain,
! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1)) ),
inference(cnf_transformation,[],[f572]) ).
fof(f936,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f588]) ).
fof(f937,plain,
! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f588]) ).
fof(f938,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f589]) ).
fof(f939,plain,
! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc463869047n_some,aa_TPT43085870d_bool(scratc982474675ffprop(X1),X0)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f589]) ).
fof(f948,plain,
! [X2,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X2)) ),
inference(cnf_transformation,[],[f595]) ).
fof(f979,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ),
inference(cnf_transformation,[],[f613]) ).
fof(f980,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X2)) ),
inference(cnf_transformation,[],[f613]) ).
fof(f981,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X2)) ),
inference(cnf_transformation,[],[f613]) ).
fof(f1222,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1)) ),
inference(cnf_transformation,[],[f719]) ).
fof(f1225,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1)) ),
inference(cnf_transformation,[],[f720]) ).
fof(f1278,plain,
! [X3,X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
| ~ scratc268048172_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| pp(aa_TPTP_ind_bool(X1,X3)) ),
inference(cnf_transformation,[],[f742]) ).
fof(f1279,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1))
| gg_TPTP_ind(sK11(X0,X1)) ),
inference(cnf_transformation,[],[f742]) ).
fof(f1280,plain,
! [X0,X1] :
( scratc268048172_is_of(sK11(X0,X1),X0)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1)) ),
inference(cnf_transformation,[],[f742]) ).
fof(f1281,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X1,sK11(X0,X1)))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),X1)) ),
inference(cnf_transformation,[],[f742]) ).
fof(f1389,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ),
inference(cnf_transformation,[],[f781]) ).
fof(f1391,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bs,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0)) ),
inference(cnf_transformation,[],[f782]) ).
fof(f1453,plain,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ct)),
inference(cnf_transformation,[],[f161]) ).
fof(f1454,plain,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_bt)),
inference(cnf_transformation,[],[f149]) ).
fof(f1596,plain,
! [X2,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))) ),
inference(resolution,[],[f1281,f981]) ).
fof(f1597,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X1),X2)) ),
inference(resolution,[],[f1281,f979]) ).
fof(f1598,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X2),sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))) ),
inference(resolution,[],[f1281,f980]) ).
fof(f1602,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),X1)) ),
inference(resolution,[],[f1597,f865]) ).
fof(f1603,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0))))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(resolution,[],[f1602,f1281]) ).
fof(f1634,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),X0)) ),
inference(resolution,[],[f939,f936]) ).
fof(f1642,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X1),X0)) ),
inference(resolution,[],[f937,f938]) ).
fof(f1643,plain,
! [X2,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))),X1))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))) ),
inference(resolution,[],[f1642,f1596]) ).
fof(f1728,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_br(X0),X1),X2))
| ~ scratc268048172_is_of(X2,aTP_Lamm_a)
| ~ gg_TPTP_ind(X2)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1)) ),
inference(resolution,[],[f1225,f1278]) ).
fof(f1891,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f1453,f1278]) ).
fof(f1982,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0))
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f1454,f1278]) ).
fof(f2131,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),X1))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ),
inference(resolution,[],[f1389,f1278]) ).
fof(f2268,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X0),X1))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,X0)) ),
inference(resolution,[],[f1391,f1278]) ).
fof(f2472,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X2),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,X2),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X0),X1))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,X2),X0)) ),
inference(resolution,[],[f948,f1728]) ).
fof(f2478,plain,
! [X2,X3,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bs,sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X3),X1))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))),X3))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X2))) ),
inference(resolution,[],[f2472,f1643]) ).
fof(f2524,plain,
! [X2,X3,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc865899134nd_iii,sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X3))),X0))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X0),X1))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X3)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X3)))) ),
inference(resolution,[],[f2478,f2268]) ).
fof(f2536,plain,
! [X2,X3,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2053665920_29_ii,X1),sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X3))))
| ~ gg_TPTP_ind(X0)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X3)))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X3))))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f2524,f1634]) ).
fof(f2541,plain,
! [X2,X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(resolution,[],[f2536,f1598]) ).
fof(f2548,plain,
! [X2,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bt,sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(duplicate_literal_removal,[],[f2541]) ).
fof(f2550,plain,
! [X2,X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X0),X1))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1)
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X0)))
| ~ scratc268048172_is_of(sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X0)),aTP_Lamm_a) ),
inference(resolution,[],[f2548,f1982]) ).
fof(f2552,plain,
! [X2,X0,X1] :
( ~ scratc268048172_is_of(sK11(X2,aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X2),aa_TPT43085870d_bool(aTP_Lamm_aa(X1),X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1)
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X0),X1)) ),
inference(forward_subsumption_resolution,[],[f2550,f1279]) ).
fof(f2553,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0))
| pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(resolution,[],[f2552,f1280]) ).
fof(f2554,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1)))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X1),X0)) ),
inference(duplicate_literal_removal,[],[f2553]) ).
fof(f2555,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X1),X0))
| ~ gg_TPTP_ind(X0)
| ~ gg_TPTP_ind(X1)
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,X0),X1))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(resolution,[],[f2554,f865]) ).
fof(f2558,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_ab,X1)))
| ~ gg_TPTP_ind(X1)
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_ab,X1))),X1))
| ~ scratc268048172_is_of(sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_ab,X1)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_ab,X1))) ),
inference(resolution,[],[f2555,f1281]) ).
fof(f2560,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1206750318lessis,sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_ab,X1))),X1))
| ~ scratc268048172_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ scratc268048172_is_of(sK11(X0,aa_TPT43085870d_bool(aTP_Lamm_ab,X1)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_ab,X1))) ),
inference(forward_subsumption_resolution,[],[f2558,f1279]) ).
fof(f2569,plain,
! [X0,X1] :
( ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1340733930moreis,X0),sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))) ),
inference(resolution,[],[f2560,f1222]) ).
fof(f2573,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs,X0),sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0))))
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(forward_subsumption_resolution,[],[f2569,f1603]) ).
fof(f2576,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| ~ gg_TPTP_ind(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ),
inference(resolution,[],[f2573,f2131]) ).
fof(f2578,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ),
inference(duplicate_literal_removal,[],[f2576]) ).
fof(f2579,plain,
! [X0,X1] :
( ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ct,X0)) ),
inference(forward_subsumption_resolution,[],[f2578,f1279]) ).
fof(f2580,plain,
! [X0,X1] :
( ~ scratc268048172_is_of(sK11(X1,aa_TPT43085870d_bool(aTP_Lamm_ab,X0)),aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(forward_subsumption_resolution,[],[f2579,f1891]) ).
fof(f2581,plain,
! [X0] :
( ~ gg_TPTP_ind(X0)
| pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(resolution,[],[f2580,f1280]) ).
fof(f2582,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ gg_TPTP_ind(X0)
| ~ scratc268048172_is_of(X0,aTP_Lamm_a) ),
inference(duplicate_literal_removal,[],[f2581]) ).
fof(f2583,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ scratc268048172_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0) ),
inference(resolution,[],[f2582,f815]) ).
fof(f2585,plain,
! [X0] :
( ~ scratc268048172_is_of(sK11(X0,aTP_Lamm_ac),aTP_Lamm_a)
| ~ gg_TPTP_ind(sK11(X0,aTP_Lamm_ac))
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aTP_Lamm_ac)) ),
inference(resolution,[],[f2583,f1281]) ).
fof(f2587,plain,
! [X0] :
( ~ scratc268048172_is_of(sK11(X0,aTP_Lamm_ac),aTP_Lamm_a)
| pp(aa_fun171081125l_bool(scratc609383597all_of(X0),aTP_Lamm_ac)) ),
inference(forward_subsumption_resolution,[],[f2585,f1279]) ).
fof(f2588,plain,
( pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac))
| pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
inference(resolution,[],[f2587,f1280]) ).
fof(f2589,plain,
pp(aa_fun171081125l_bool(scratc609383597all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(duplicate_literal_removal,[],[f2588]) ).
fof(f2590,plain,
$false,
inference(forward_subsumption_resolution,[],[f2589,f800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM665+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.14/0.42 % Computer : n007.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Sun Sep 27 20:58:55 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.48 Running first-order theorem proving
% 0.14/0.48 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
% 18.29/3.41 % (1772519)Detected formulas, will run a generic FOF schedule.
% 18.29/3.41 % (1772529)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=734344765:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 18.29/3.41 % (1772528)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=406583936:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 18.29/3.41 % (1772524)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=1165590997:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 18.29/3.41 % (1772527)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=881418497:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 18.29/3.41 % (1772530)dis-21_1_sil=8000:lcm=predicate:random_seed=1895109717: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)
% 18.29/3.41 % (1772525)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=782594876:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 18.29/3.41 % (1772526)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=4217186856:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 18.29/3.41 % (1772527)Refutation not found, incomplete strategy
% 18.29/3.41 % (1772527)------------------------------
% 18.29/3.41 % (1772527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.41 % (1772527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.41 % (1772527)CaDiCaL version: 2.1.3
% 18.29/3.41 % (1772527)Termination reason: Refutation not found, incomplete strategy
% 18.29/3.41 % (1772527)Time elapsed: 0.003 s
% 18.29/3.41 % (1772527)Peak memory usage: 88 MB
% 18.29/3.41 % (1772527)Instructions burned: 2 (million)
% 18.29/3.41 % (1772528)Refutation not found, incomplete strategy
% 18.29/3.41 % (1772528)------------------------------
% 18.29/3.41 % (1772528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.41 % (1772528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.41 % (1772528)CaDiCaL version: 2.1.3
% 18.29/3.41 % (1772528)Termination reason: Refutation not found, incomplete strategy
% 18.29/3.41 % (1772528)Time elapsed: 0.004 s
% 18.29/3.41 % (1772528)Peak memory usage: 88 MB
% 18.29/3.41 % (1772528)Instructions burned: 2 (million)
% 18.29/3.41 % (1772529)Instruction limit reached!
% 18.29/3.41 % (1772529)------------------------------
% 18.29/3.41 % (1772529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.41 % (1772529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.41 % (1772529)CaDiCaL version: 2.1.3
% 18.29/3.41 % (1772529)Termination reason: Instruction limit
% 18.29/3.41 % (1772529)Termination phase: Saturation
% 18.29/3.41 % (1772529)Time elapsed: 0.077 s
% 18.29/3.41 % (1772529)Peak memory usage: 90 MB
% 18.29/3.41 % (1772529)Instructions burned: 139 (million)
% 18.29/3.41 % (1772530)Instruction limit reached!
% 18.29/3.41 % (1772530)------------------------------
% 18.29/3.41 % (1772530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.41 % (1772530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.41 % (1772530)CaDiCaL version: 2.1.3
% 18.29/3.41 % (1772530)Termination reason: Instruction limit
% 18.29/3.41 % (1772530)Termination phase: Saturation
% 18.29/3.41 % (1772530)Time elapsed: 0.131 s
% 18.29/3.41 % (1772530)Peak memory usage: 90 MB
% 18.29/3.41 % (1772530)Instructions burned: 129 (million)
% 18.29/3.41 % (1772540)lrs+10_1_sil=8000:sp=occurrence:random_seed=1964491757:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 18.29/3.41 % (1772540)Refutation not found, incomplete strategy
% 18.29/3.41 % (1772540)------------------------------
% 18.29/3.41 % (1772540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.29/3.41 % (1772540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.29/3.41 % (1772540)CaDiCaL version: 2.1.3
% 18.29/3.41 % (1772540)Termination reason: Refutation not found, incomplete strategy
% 18.29/3.41 % (1772540)Time elapsed: 0.002 s
% 18.29/3.41 % (1772540)Peak memory usage: 88 MB
% 18.29/3.41 % (1772540)Instructions burned: 2 (million)
% 18.29/3.41 % (1772528)------------------------------
% 29.12/5.04 % (1772528)------------------------------
% 29.12/5.04 % (1772527)------------------------------
% 29.12/5.04 % (1772527)------------------------------
% 29.12/5.04 % (1772541)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3210096668:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 29.12/5.04 % (1772541)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772541)------------------------------
% 29.12/5.04 % (1772541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772541)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772541)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772541)Time elapsed: 0.008 s
% 29.12/5.04 % (1772541)Peak memory usage: 88 MB
% 29.12/5.04 % (1772541)Instructions burned: 7 (million)
% 29.12/5.04 % (1772540)------------------------------
% 29.12/5.04 % (1772540)------------------------------
% 29.12/5.04 % (1772545)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2240665410:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 29.12/5.04 % (1772545)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772545)------------------------------
% 29.12/5.04 % (1772545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772545)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772545)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772545)Time elapsed: 0.007 s
% 29.12/5.04 % (1772545)Peak memory usage: 89 MB
% 29.12/5.04 % (1772545)Instructions burned: 4 (million)
% 29.12/5.04 % (1772546)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=2183465217:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 29.12/5.04 % (1772548)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=558349542:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 29.12/5.04 % (1772548)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772548)------------------------------
% 29.12/5.04 % (1772548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772548)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772548)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772548)Time elapsed: 0.004 s
% 29.12/5.04 % (1772548)Peak memory usage: 88 MB
% 29.12/5.04 % (1772548)Instructions burned: 5 (million)
% 29.12/5.04 % (1772541)------------------------------
% 29.12/5.04 % (1772541)------------------------------
% 29.12/5.04 % (1772546)Instruction limit reached!
% 29.12/5.04 % (1772546)------------------------------
% 29.12/5.04 % (1772546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772546)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772546)Termination reason: Instruction limit
% 29.12/5.04 % (1772546)Termination phase: Saturation
% 29.12/5.04 % (1772546)Time elapsed: 0.243 s
% 29.12/5.04 % (1772546)Peak memory usage: 93 MB
% 29.12/5.04 % (1772546)Instructions burned: 248 (million)
% 29.12/5.04 % (1772548)------------------------------
% 29.12/5.04 % (1772548)------------------------------
% 29.12/5.04 % (1772545)------------------------------
% 29.12/5.04 % (1772545)------------------------------
% 29.12/5.04 % (1772552)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1317487159:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 29.12/5.04 % (1772556)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2083064447:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 29.12/5.04 % (1772555)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2109380566:cts=off:i=113:fsr=off:ss=included:sgt=4_2988 on theBenchmark for (2988ds/113Mi)
% 29.12/5.04 % (1772556)Instruction limit reached!
% 29.12/5.04 % (1772556)------------------------------
% 29.12/5.04 % (1772556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772556)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772556)Termination reason: Instruction limit
% 29.12/5.04 % (1772556)Termination phase: Saturation
% 29.12/5.04 % (1772556)Time elapsed: 0.059 s
% 29.12/5.04 % (1772556)Peak memory usage: 89 MB
% 29.12/5.04 % (1772556)Instructions burned: 129 (million)
% 29.12/5.04 % (1772555)Instruction limit reached!
% 29.12/5.04 % (1772555)------------------------------
% 29.12/5.04 % (1772555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772555)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772555)Termination reason: Instruction limit
% 29.12/5.04 % (1772555)Termination phase: Saturation
% 29.12/5.04 % (1772555)Time elapsed: 0.113 s
% 29.12/5.04 % (1772555)Peak memory usage: 90 MB
% 29.12/5.04 % (1772555)Instructions burned: 113 (million)
% 29.12/5.04 % (1772557)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2507440391:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 29.12/5.04 % (1772557)Instruction limit reached!
% 29.12/5.04 % (1772557)------------------------------
% 29.12/5.04 % (1772557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772557)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772557)Termination reason: Instruction limit
% 29.12/5.04 % (1772557)Termination phase: Saturation
% 29.12/5.04 % (1772557)Time elapsed: 0.115 s
% 29.12/5.04 % (1772557)Peak memory usage: 89 MB
% 29.12/5.04 % (1772557)Instructions burned: 115 (million)
% 29.12/5.04 % (1772561)lrs+10_1_sil=8000:sp=occurrence:random_seed=3490732367:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 29.12/5.04 % (1772562)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2401348355:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 29.12/5.04 % (1772562)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772562)------------------------------
% 29.12/5.04 % (1772562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772562)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772562)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772562)Time elapsed: 0.054 s
% 29.12/5.04 % (1772562)Peak memory usage: 90 MB
% 29.12/5.04 % (1772562)Instructions burned: 57 (million)
% 29.12/5.04 % (1772565)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=181035200:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 29.12/5.04 % (1772561)Instruction limit reached!
% 29.12/5.04 % (1772561)------------------------------
% 29.12/5.04 % (1772561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772561)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772561)Termination reason: Instruction limit
% 29.12/5.04 % (1772561)Termination phase: Saturation
% 29.12/5.04 % (1772561)Time elapsed: 0.457 s
% 29.12/5.04 % (1772561)Peak memory usage: 99 MB
% 29.12/5.04 % (1772561)Instructions burned: 907 (million)
% 29.12/5.04 % (1772562)------------------------------
% 29.12/5.04 % (1772562)------------------------------
% 29.12/5.04 % (1772568)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1610817649:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 29.12/5.04 % (1772568)Instruction limit reached!
% 29.12/5.04 % (1772568)------------------------------
% 29.12/5.04 % (1772568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772568)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772568)Termination reason: Instruction limit
% 29.12/5.04 % (1772568)Termination phase: Saturation
% 29.12/5.04 % (1772568)Time elapsed: 0.063 s
% 29.12/5.04 % (1772568)Peak memory usage: 92 MB
% 29.12/5.04 % (1772568)Instructions burned: 135 (million)
% 29.12/5.04 % (1772569)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2407951032:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 29.12/5.04 % (1772569)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772569)------------------------------
% 29.12/5.04 % (1772569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772569)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772569)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772569)Time elapsed: 0.029 s
% 29.12/5.04 % (1772569)Peak memory usage: 89 MB
% 29.12/5.04 % (1772569)Instructions burned: 31 (million)
% 29.12/5.04 % (1772571)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3279844057:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 29.12/5.04 % (1772569)------------------------------
% 29.12/5.04 % (1772569)------------------------------
% 29.12/5.04 % (1772574)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=2893267004:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/125Mi)
% 29.12/5.04 % (1772574)Instruction limit reached!
% 29.12/5.04 % (1772574)------------------------------
% 29.12/5.04 % (1772574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772574)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772574)Termination reason: Instruction limit
% 29.12/5.04 % (1772574)Termination phase: Saturation
% 29.12/5.04 % (1772574)Time elapsed: 0.116 s
% 29.12/5.04 % (1772574)Peak memory usage: 92 MB
% 29.12/5.04 % (1772574)Instructions burned: 125 (million)
% 29.12/5.04 % (1772576)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=487631098:i=134:gtgl=5:slsql=off:gtg=exists_sym_2965 on theBenchmark for (2965ds/134Mi)
% 29.12/5.04 % (1772565)First to succeed.
% 29.12/5.04 % (1772565)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1772519"
% 29.12/5.04 % (1772576)Instruction limit reached!
% 29.12/5.04 % (1772576)------------------------------
% 29.12/5.04 % (1772576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772576)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772576)Termination reason: Instruction limit
% 29.12/5.04 % (1772576)Termination phase: Saturation
% 29.12/5.04 % (1772576)Time elapsed: 0.126 s
% 29.12/5.04 % (1772576)Peak memory usage: 92 MB
% 29.12/5.04 % (1772576)Instructions burned: 135 (million)
% 29.12/5.04 % (1772552)Instruction limit reached!
% 29.12/5.04 % (1772552)------------------------------
% 29.12/5.04 % (1772552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772552)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772552)Termination reason: Instruction limit
% 29.12/5.04 % (1772552)Termination phase: Saturation
% 29.12/5.04 % (1772552)Time elapsed: 2.724 s
% 29.12/5.04 % (1772552)Peak memory usage: 142 MB
% 29.12/5.04 % (1772552)Instructions burned: 2351 (million)
% 29.12/5.04 % (1772578)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4191556908:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/141Mi)
% 29.12/5.04 % (1772578)Refutation not found, incomplete strategy
% 29.12/5.04 % (1772578)------------------------------
% 29.12/5.04 % (1772578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.12/5.04 % (1772578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.12/5.04 % (1772578)CaDiCaL version: 2.1.3
% 29.12/5.04 % (1772578)Termination reason: Refutation not found, incomplete strategy
% 29.12/5.04 % (1772578)Time elapsed: 0.004 s
% 29.12/5.04 % (1772578)Peak memory usage: 88 MB
% 29.12/5.04 % (1772578)Instructions burned: 2 (million)
% 29.12/5.04 % (1772565)Refutation found. Thanks to Tanya!
% 29.12/5.04 % SZS status Theorem for theBenchmark
% 29.12/5.04 % SZS output start Proof for theBenchmark
% See solution above
% 30.61/5.32 % (1772565)------------------------------
% 30.61/5.32 % (1772565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.61/5.32 % (1772565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.61/5.32 % (1772565)CaDiCaL version: 2.1.3
% 30.61/5.32 % (1772565)Termination reason: Refutation
% 30.61/5.32 % (1772565)Time elapsed: 1.853 s
% 30.61/5.32 % (1772565)Peak memory usage: 139 MB
% 30.61/5.32 % (1772565)Instructions burned: 1690 (million)
% 30.61/5.32 % (1772565)------------------------------
% 30.61/5.32 % (1772565)------------------------------
% 30.61/5.32 % (1772519)Success in time 4.237 s
% 30.61/5.32 % Vampire exiting
%------------------------------------------------------------------------------