%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM655+4 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:14 PM UTC 2026
% Result : Theorem 6.14s 1.86s
% Output : Refutation 7.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 35
% Syntax : Number of formulae : 187 ( 33 unt; 18 def)
% Number of atoms : 449 ( 2 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 449 ( 187 ~; 197 |; 27 &)
% ( 33 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 23 ( 21 usr; 19 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 15 con; 0-2 aty)
% Number of variables : 105 ( 0 sgn 103 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f29,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f115,axiom,
! [X0] :
( pp(scratc855283518_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc15259325nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f116,axiom,
scratc15259325nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f147,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1760362736_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f149,axiom,
pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_br)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz10e) ).
fof(f152,axiom,
pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_bx)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz14) ).
fof(f281,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_bx,X0))
<=> pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__35) ).
fof(f284,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
<=> pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__38) ).
fof(f285,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
<=> pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__39) ).
fof(f307,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__61) ).
fof(f315,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
<=> ( pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__69) ).
fof(f316,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1)))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__70) ).
fof(f390,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f391,axiom,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
fof(f393,axiom,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
fof(f400,conjecture,
pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f401,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f400]) ).
fof(f402,plain,
~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(flattening,[],[f401]) ).
fof(f419,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1760362736_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f147]) ).
fof(f420,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1760362736_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f419]) ).
fof(f485,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1)) ) ),
inference(ennf_transformation,[],[f307]) ).
fof(f489,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1))) ) ),
inference(ennf_transformation,[],[f315]) ).
fof(f490,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))) ) ),
inference(ennf_transformation,[],[f316]) ).
fof(f519,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f520,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f29]) ).
fof(f560,plain,
! [X0] :
( ( pp(scratc855283518_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc15259325nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc15259325nd_imp,X0),fFalse))
| ~ pp(scratc855283518_d_not(X0)) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f583,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1760362736_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1760362736_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f420]) ).
fof(f584,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1760362736_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1760362736_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1)) ) ),
inference(rectify,[],[f583]) ).
fof(f585,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc1760362736_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1760362736_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f584]) ).
fof(f639,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_bx,X0))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bx,X0)) ) ),
inference(nnf_transformation,[],[f281]) ).
fof(f642,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0)) ) ),
inference(nnf_transformation,[],[f284]) ).
fof(f643,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ) ),
inference(nnf_transformation,[],[f285]) ).
fof(f672,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1)) ) ),
inference(nnf_transformation,[],[f485]) ).
fof(f673,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1)) ) ),
inference(flattening,[],[f672]) ).
fof(f683,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
& pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ) ),
inference(nnf_transformation,[],[f489]) ).
fof(f684,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
& pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ) ),
inference(flattening,[],[f683]) ).
fof(f685,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1))
& pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(nnf_transformation,[],[f490]) ).
fof(f686,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1))
& pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(flattening,[],[f685]) ).
fof(f793,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f519]) ).
fof(f794,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f520]) ).
fof(f916,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc15259325nd_imp,X0),fFalse))
| ~ pp(scratc855283518_d_not(X0)) ),
inference(cnf_transformation,[],[f560]) ).
fof(f917,plain,
! [X0] :
( pp(scratc855283518_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc15259325nd_imp,X0),fFalse)) ),
inference(cnf_transformation,[],[f560]) ).
fof(f918,plain,
scratc15259325nd_imp = fimplies,
inference(cnf_transformation,[],[f116]) ).
fof(f980,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1760362736_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1)) ),
inference(cnf_transformation,[],[f585]) ).
fof(f981,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f585]) ).
fof(f982,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| scratc1760362736_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f585]) ).
fof(f983,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f585]) ).
fof(f986,plain,
pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_br)),
inference(cnf_transformation,[],[f149]) ).
fof(f989,plain,
pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_bx)),
inference(cnf_transformation,[],[f152]) ).
fof(f1182,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_bx,X0)) ),
inference(cnf_transformation,[],[f639]) ).
fof(f1188,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_br,X0)) ),
inference(cnf_transformation,[],[f642]) ).
fof(f1191,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
inference(cnf_transformation,[],[f643]) ).
fof(f1239,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,X0),X1)) ),
inference(cnf_transformation,[],[f673]) ).
fof(f1258,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,X0),X1))
| ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,X0),X1)) ),
inference(cnf_transformation,[],[f684]) ).
fof(f1262,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,X0),X1))) ),
inference(cnf_transformation,[],[f686]) ).
fof(f1263,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,X0),X1)) ),
inference(cnf_transformation,[],[f686]) ).
fof(f1418,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f390]) ).
fof(f1419,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f391]) ).
fof(f1421,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f393]) ).
fof(f1428,plain,
~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[],[f402]) ).
fof(f1480,plain,
! [X0] :
( pp(scratc855283518_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse)) ),
inference(definition_unfolding,[],[f917,f918]) ).
fof(f1481,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),fFalse))
| ~ pp(scratc855283518_d_not(X0)) ),
inference(definition_unfolding,[],[f916,f918]) ).
fof(f1584,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f1586,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_ab))
| spl29_1 ),
inference(avatar_component_clause,[],[f1584]) ).
fof(f1587,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f1428,f1584]) ).
fof(f1588,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ab))
| spl29_1 ),
inference(resolution,[],[f1586,f981]) ).
fof(f1589,plain,
( scratc1760362736_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f1586,f982]) ).
fof(f1590,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_1 ),
inference(resolution,[],[f1586,f983]) ).
fof(f1603,definition,
( spl29_2
<=> scratc1760362736_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f1605,plain,
( scratc1760362736_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f1603]) ).
fof(f1606,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f1589,f1584,f1603]) ).
fof(f1608,definition,
( spl29_3
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab))) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f1610,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| spl29_3 ),
inference(avatar_component_clause,[],[f1608]) ).
fof(f1611,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f1590,f1584,f1608]) ).
fof(f1612,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl29_3 ),
inference(resolution,[],[f1610,f1191]) ).
fof(f1650,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(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f1605,f980]) ).
fof(f1651,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| spl29_1
| ~ spl29_2 ),
inference(forward_subsumption_resolution,[],[f1650,f1588]) ).
fof(f1653,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f1654,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ab)))
| ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f1653]) ).
fof(f1655,plain,
( spl29_4
| spl29_1
| ~ spl29_2 ),
inference(avatar_split_clause,[],[f1651,f1603,f1584,f1653]) ).
fof(f2046,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc1910373353all_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(f2048,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))
| spl29_6 ),
inference(avatar_component_clause,[],[f2046]) ).
fof(f2049,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f1612,f1608,f2046]) ).
fof(f2051,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,[],[f2048,f981]) ).
fof(f2052,plain,
( scratc1760362736_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,[],[f2048,f982]) ).
fof(f2053,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,[],[f2048,f983]) ).
fof(f2066,definition,
( spl29_7
<=> scratc1760362736_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(f2068,plain,
( scratc1760362736_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,[],[f2066]) ).
fof(f2069,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f2052,f2046,f2066]) ).
fof(f2071,definition,
( spl29_8
<=> 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_8])],[avatar_definition]) ).
fof(f2073,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_8 ),
inference(avatar_component_clause,[],[f2071]) ).
fof(f2074,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f2053,f2046,f2071]) ).
fof(f2075,plain,
( pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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_8 ),
inference(resolution,[],[f2073,f1262]) ).
fof(f2076,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,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_8 ),
inference(resolution,[],[f2073,f1263]) ).
fof(f2122,definition,
( spl29_9
<=> pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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(f2124,plain,
( pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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,[],[f2122]) ).
fof(f2125,plain,
( spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f2075,f2071,f2122]) ).
fof(f2129,plain,
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),fFalse))
| ~ spl29_9 ),
inference(resolution,[],[f2124,f1481]) ).
fof(f2140,definition,
( spl29_10
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),fFalse)) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f2142,plain,
( pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))),fFalse))
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f2140]) ).
fof(f2143,plain,
( spl29_10
| ~ spl29_9 ),
inference(avatar_split_clause,[],[f2129,f2122,f2140]) ).
fof(f2145,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ab)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))))
| pp(fFalse)
| ~ spl29_10 ),
inference(resolution,[],[f2142,f1419]) ).
fof(f2156,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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_10 ),
inference(forward_subsumption_resolution,[],[f2145,f1418]) ).
fof(f2158,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(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f2068,f980]) ).
fof(f2159,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(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f2158,f2051]) ).
fof(f2161,definition,
( spl29_11
<=> ! [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(scratc1910373353all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f2162,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(scratc1910373353all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f2161]) ).
fof(f2163,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f2159,f2066,f2046,f2161]) ).
fof(f2400,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_br))
| pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_11 ),
inference(resolution,[],[f2162,f1188]) ).
fof(f2403,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aTP_Lamm_bx))
| pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_11 ),
inference(resolution,[],[f2162,f1182]) ).
fof(f2482,plain,
( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f2403,f989]) ).
fof(f2485,plain,
( pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f2400,f986]) ).
fof(f2549,definition,
( spl29_12
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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(f2551,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc14996922nd_iii,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,[],[f2549]) ).
fof(f2552,plain,
( ~ spl29_12
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f2156,f2140,f2549]) ).
fof(f2564,plain,
( ~ pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(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,[],[f2551,f793]) ).
fof(f2786,definition,
( spl29_15
<=> pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(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_15])],[avatar_definition]) ).
fof(f2788,plain,
( ~ pp(aa_fun171081125l_bool(scratc1764858803n_some,aa_TPT43085870d_bool(scratc1461823351ffprop(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_15 ),
inference(avatar_component_clause,[],[f2786]) ).
fof(f2789,plain,
( ~ spl29_15
| spl29_12 ),
inference(avatar_split_clause,[],[f2564,f2549,f2786]) ).
fof(f2791,definition,
( spl29_16
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,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(f2793,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc685564846moreis,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,[],[f2791]) ).
fof(f2794,plain,
( ~ spl29_16
| spl29_8 ),
inference(avatar_split_clause,[],[f2076,f2071,f2791]) ).
fof(f2800,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,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_bw,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_16 ),
inference(resolution,[],[f2793,f1239]) ).
fof(f2852,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_15 ),
inference(resolution,[],[f2788,f794]) ).
fof(f2904,definition,
( spl29_19
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_19])],[avatar_definition]) ).
fof(f2906,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_19 ),
inference(avatar_component_clause,[],[f2904]) ).
fof(f2907,plain,
( ~ spl29_19
| spl29_15 ),
inference(avatar_split_clause,[],[f2852,f2786,f2904]) ).
fof(f2909,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,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_20])],[avatar_definition]) ).
fof(f2911,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw,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_20 ),
inference(avatar_component_clause,[],[f2909]) ).
fof(f2913,definition,
( spl29_21
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,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_21])],[avatar_definition]) ).
fof(f2915,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc551581234lessis,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_21 ),
inference(avatar_component_clause,[],[f2913]) ).
fof(f2916,plain,
( ~ spl29_20
| ~ spl29_21
| spl29_16 ),
inference(avatar_split_clause,[],[f2800,f2791,f2913,f2909]) ).
fof(f2925,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_4
| spl29_20 ),
inference(resolution,[],[f2911,f1654]) ).
fof(f2964,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_20 ),
inference(forward_subsumption_resolution,[],[f2925,f2482]) ).
fof(f2965,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_20 ),
inference(avatar_contradiction_clause,[],[f2964]) ).
fof(f2966,plain,
( ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_bq,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_21 ),
inference(resolution,[],[f2915,f1258]) ).
fof(f3056,plain,
( ! [X0] : pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),sK12(aTP_Lamm_a,aTP_Lamm_ab))),X0))
| spl29_19 ),
inference(resolution,[],[f2906,f1421]) ).
fof(f3160,definition,
( spl29_25
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,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_25])],[avatar_definition]) ).
fof(f3162,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bq,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_25 ),
inference(avatar_component_clause,[],[f3160]) ).
fof(f3164,definition,
( spl29_26
<=> pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_26])],[avatar_definition]) ).
fof(f3166,plain,
( ~ pp(scratc855283518_d_not(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,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_26 ),
inference(avatar_component_clause,[],[f3164]) ).
fof(f3167,plain,
( ~ spl29_25
| ~ spl29_26
| spl29_21 ),
inference(avatar_split_clause,[],[f2966,f2913,f3164,f3160]) ).
fof(f3176,plain,
( ~ pp(aa_fun171081125l_bool(scratc1910373353all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab))))))
| ~ spl29_4
| spl29_25 ),
inference(resolution,[],[f3162,f1654]) ).
fof(f3215,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_25 ),
inference(forward_subsumption_resolution,[],[f3176,f2485]) ).
fof(f3216,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_25 ),
inference(avatar_contradiction_clause,[],[f3215]) ).
fof(f3220,plain,
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1244405180_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,sK12(aTP_Lamm_a,aTP_Lamm_ab)))),sK12(aTP_Lamm_a,aTP_Lamm_ab))),fFalse))
| spl29_26 ),
inference(resolution,[],[f3166,f1480]) ).
fof(f3232,plain,
( $false
| spl29_19
| spl29_26 ),
inference(forward_subsumption_resolution,[],[f3220,f3056]) ).
fof(f3233,plain,
( spl29_19
| spl29_26 ),
inference(avatar_contradiction_clause,[],[f3232]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f1587]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s4,plain,
( spl29_1
| ~ spl29_2
| spl29_4 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f2074]) ).
cnf(s9,plain,
( spl29_8
| spl29_9 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s10,plain,
( ~ spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f2163]) ).
cnf(s12,plain,
( ~ spl29_10
| ~ spl29_12 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s15,plain,
( spl29_12
| ~ spl29_15 ),
inference(sat_conversion,[],[f2789]) ).
cnf(s16,plain,
( spl29_8
| ~ spl29_16 ),
inference(sat_conversion,[],[f2794]) ).
cnf(s19,plain,
( spl29_15
| ~ spl29_19 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s20,plain,
( spl29_16
| ~ spl29_20
| ~ spl29_21 ),
inference(sat_conversion,[],[f2916]) ).
cnf(s21,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_20 ),
inference(sat_conversion,[],[f2965]) ).
cnf(s25,plain,
( spl29_21
| ~ spl29_25
| ~ spl29_26 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s26,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_25 ),
inference(sat_conversion,[],[f3216]) ).
cnf(s27,plain,
( spl29_19
| spl29_26 ),
inference(sat_conversion,[],[f3233]) ).
cnf(s29,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s30,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s33,plain,
~ spl29_6,
inference(rat,[],[s6,s29]) ).
cnf(s34,plain,
spl29_4,
inference(rat,[],[s4,s1,s30]) ).
cnf(s36,plain,
~ spl29_8,
inference(rat,[],[s8,s33]) ).
cnf(s37,plain,
spl29_7,
inference(rat,[],[s7,s33]) ).
cnf(s39,plain,
~ spl29_16,
inference(rat,[],[s16,s36]) ).
cnf(s41,plain,
spl29_9,
inference(rat,[],[s9,s36]) ).
cnf(s42,plain,
spl29_11,
inference(rat,[],[s11,s33,s37]) ).
cnf(s44,plain,
spl29_10,
inference(rat,[],[s10,s41]) ).
cnf(s45,plain,
spl29_25,
inference(rat,[],[s26,s34,s42]) ).
cnf(s46,plain,
spl29_20,
inference(rat,[],[s21,s34,s42]) ).
cnf(s47,plain,
~ spl29_12,
inference(rat,[],[s12,s44]) ).
cnf(s48,plain,
~ spl29_21,
inference(rat,[],[s20,s39,s46]) ).
cnf(s50,plain,
~ spl29_15,
inference(rat,[],[s15,s47]) ).
cnf(s51,plain,
~ spl29_26,
inference(rat,[],[s25,s45,s48]) ).
cnf(s52,plain,
~ spl29_19,
inference(rat,[],[s19,s50]) ).
cnf(s53,plain,
$false,
inference(rat,[],[s27,s51,s52]) ).
fof(f3234,plain,
$false,
inference(avatar_sat_refutation,[],[s53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM655+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 20:58:30 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.14/1.86 % (2384198)Detected formulas, will run a generic FOF schedule.
% 6.14/1.86 % (2384205)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=1869064678:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 6.14/1.86 % (2384207)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2888332462:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 6.14/1.86 % (2384204)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=4835317:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 6.14/1.86 % (2384206)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=5300052:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 6.14/1.86 % (2384208)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3606124459:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 6.14/1.86 % (2384203)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=1185552058:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 6.14/1.86 % (2384209)dis-21_1_sil=8000:lcm=predicate:random_seed=3008377219: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)
% 6.14/1.86 % (2384206)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384206)------------------------------
% 6.14/1.86 % (2384206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384206)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384206)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384206)Time elapsed: 0.002 s
% 6.14/1.86 % (2384206)Peak memory usage: 87 MB
% 6.14/1.86 % (2384206)Instructions burned: 1 (million)
% 6.14/1.86 % (2384207)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384207)------------------------------
% 6.14/1.86 % (2384207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384207)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384207)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384207)Time elapsed: 0.003 s
% 6.14/1.86 % (2384207)Peak memory usage: 87 MB
% 6.14/1.86 % (2384207)Instructions burned: 2 (million)
% 6.14/1.86 % (2384209)Instruction limit reached!
% 6.14/1.86 % (2384209)------------------------------
% 6.14/1.86 % (2384209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384209)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384209)Termination reason: Instruction limit
% 6.14/1.86 % (2384209)Termination phase: Saturation
% 6.14/1.86 % (2384209)Time elapsed: 0.077 s
% 6.14/1.86 % (2384209)Peak memory usage: 90 MB
% 6.14/1.86 % (2384209)Instructions burned: 129 (million)
% 6.14/1.86 % (2384208)Instruction limit reached!
% 6.14/1.86 % (2384208)------------------------------
% 6.14/1.86 % (2384208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384208)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384208)Termination reason: Instruction limit
% 6.14/1.86 % (2384208)Termination phase: Saturation
% 6.14/1.86 % (2384208)Time elapsed: 0.091 s
% 6.14/1.86 % (2384208)Peak memory usage: 90 MB
% 6.14/1.86 % (2384208)Instructions burned: 139 (million)
% 6.14/1.86 % (2384206)------------------------------
% 6.14/1.86 % (2384206)------------------------------
% 6.14/1.86 % (2384207)------------------------------
% 6.14/1.86 % (2384207)------------------------------
% 6.14/1.86 % (2384218)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4050927169:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.14/1.86 % (2384217)lrs+10_1_sil=8000:sp=occurrence:random_seed=3003575719:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 6.14/1.86 % (2384217)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384217)------------------------------
% 6.14/1.86 % (2384217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384217)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384217)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384217)Time elapsed: 0.003 s
% 6.14/1.86 % (2384217)Peak memory usage: 88 MB
% 6.14/1.86 % (2384217)Instructions burned: 2 (million)
% 6.14/1.86 % (2384218)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384218)------------------------------
% 6.14/1.86 % (2384218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384218)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384218)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384218)Time elapsed: 0.004 s
% 6.14/1.86 % (2384218)Peak memory usage: 88 MB
% 6.14/1.86 % (2384218)Instructions burned: 6 (million)
% 6.14/1.86 % (2384221)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2525899965:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 6.14/1.86 % (2384222)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=3870876626:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 6.14/1.86 % (2384221)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384221)------------------------------
% 6.14/1.86 % (2384221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384221)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384221)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384221)Time elapsed: 0.005 s
% 6.14/1.86 % (2384221)Peak memory usage: 89 MB
% 6.14/1.86 % (2384221)Instructions burned: 4 (million)
% 6.14/1.86 % (2384218)------------------------------
% 6.14/1.86 % (2384218)------------------------------
% 6.14/1.86 % (2384217)------------------------------
% 6.14/1.86 % (2384217)------------------------------
% 6.14/1.86 % (2384222)Instruction limit reached!
% 6.14/1.86 % (2384222)------------------------------
% 6.14/1.86 % (2384222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384222)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384222)Termination reason: Instruction limit
% 6.14/1.86 % (2384222)Termination phase: Saturation
% 6.14/1.86 % (2384222)Time elapsed: 0.146 s
% 6.14/1.86 % (2384222)Peak memory usage: 93 MB
% 6.14/1.86 % (2384222)Instructions burned: 249 (million)
% 6.14/1.86 % (2384205)First to succeed.
% 6.14/1.86 % (2384205)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2384198"
% 6.14/1.86 % (2384225)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2618875923:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 6.14/1.86 % (2384226)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3936086533:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 6.14/1.86 % (2384225)Refutation not found, incomplete strategy
% 6.14/1.86 % (2384225)------------------------------
% 6.14/1.86 % (2384225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384225)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384225)Termination reason: Refutation not found, incomplete strategy
% 6.14/1.86 % (2384225)Time elapsed: 0.004 s
% 6.14/1.86 % (2384225)Peak memory usage: 88 MB
% 6.14/1.86 % (2384225)Instructions burned: 5 (million)
% 6.14/1.86 % (2384221)------------------------------
% 6.14/1.86 % (2384221)------------------------------
% 6.14/1.86 % (2384227)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3025833552:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 6.14/1.86 % (2384227)Instruction limit reached!
% 6.14/1.86 % (2384227)------------------------------
% 6.14/1.86 % (2384227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.14/1.86 % (2384227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.14/1.86 % (2384227)CaDiCaL version: 2.1.3
% 6.14/1.86 % (2384227)Termination reason: Instruction limit
% 6.14/1.86 % (2384227)Termination phase: Saturation
% 6.14/1.86 % (2384227)Time elapsed: 0.068 s
% 6.14/1.86 % (2384227)Peak memory usage: 90 MB
% 6.14/1.86 % (2384227)Instructions burned: 114 (million)
% 6.14/1.86 % (2384205)Refutation found. Thanks to Tanya!
% 6.14/1.86 % SZS status Theorem for theBenchmark
% 6.14/1.86 % SZS output start Proof for theBenchmark
% See solution above
% 7.53/2.05 % (2384205)------------------------------
% 7.53/2.05 % (2384205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.53/2.05 % (2384205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/2.05 % (2384205)CaDiCaL version: 2.1.3
% 7.53/2.05 % (2384205)Termination reason: Refutation
% 7.53/2.05 % (2384205)Time elapsed: 0.672 s
% 7.53/2.05 % (2384205)Peak memory usage: 139 MB
% 7.53/2.05 % (2384205)Instructions burned: 1682 (million)
% 7.53/2.05 % (2384205)------------------------------
% 7.53/2.05 % (2384205)------------------------------
% 7.53/2.05 % (2384198)Success in time 0.996 s
% 7.53/2.05 % Vampire exiting
%------------------------------------------------------------------------------