%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM750+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:49 PM UTC 2026
% Result : Theorem 21.32s 3.75s
% Output : Refutation 22.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 33
% Syntax : Number of formulae : 190 ( 32 unt; 21 def)
% Number of atoms : 472 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 486 ( 204 ~; 217 |; 25 &)
% ( 35 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 25 ( 24 usr; 22 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 117 ( 0 sgn 115 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f199,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc213556589_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f208,axiom,
pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_cu)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz56) ).
fof(f243,axiom,
pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_gd)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_satz37) ).
fof(f456,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0))
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__21) ).
fof(f600,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cu,X0))
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__165) ).
fof(f606,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__171) ).
fof(f773,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__338) ).
fof(f776,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__341) ).
fof(f837,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(scratc541474510d_n_eq,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__402) ).
fof(f889,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__454) ).
fof(f928,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_ATP_Olambda__493) ).
fof(f965,conjecture,
pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f966,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f965]) ).
fof(f967,plain,
~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f966]) ).
fof(f984,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc213556589_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f199]) ).
fof(f985,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc213556589_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f984]) ).
fof(f1135,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(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) ),
inference(ennf_transformation,[],[f837]) ).
fof(f1202,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) ),
inference(ennf_transformation,[],[f928]) ).
fof(f1203,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) ),
inference(flattening,[],[f1202]) ).
fof(f1306,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc213556589_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc213556589_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f985]) ).
fof(f1307,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc213556589_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc213556589_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1)) ) ),
inference(rectify,[],[f1306]) ).
fof(f1308,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc213556589_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc213556589_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1307]) ).
fof(f1348,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X0)) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X0))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0)) ) ),
inference(nnf_transformation,[],[f456]) ).
fof(f1492,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cu,X0))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cu,X0)) ) ),
inference(nnf_transformation,[],[f600]) ).
fof(f1498,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f606]) ).
fof(f1701,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,X0),X1)) ) ),
inference(nnf_transformation,[],[f773]) ).
fof(f1704,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1576304300all_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,[],[f776]) ).
fof(f1802,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(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1135]) ).
fof(f1803,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(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f1802]) ).
fof(f1865,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f889]) ).
fof(f1930,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f1203]) ).
fof(f1931,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1930]) ).
fof(f2239,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc213556589_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1308]) ).
fof(f2240,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1308]) ).
fof(f2241,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| scratc213556589_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1308]) ).
fof(f2242,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1308]) ).
fof(f2252,plain,
pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_cu)),
inference(cnf_transformation,[],[f208]) ).
fof(f2287,plain,
pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_gd)),
inference(cnf_transformation,[],[f243]) ).
fof(f2550,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X0))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_gd,X0)) ),
inference(cnf_transformation,[],[f1348]) ).
fof(f2838,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cu,X0)) ),
inference(cnf_transformation,[],[f1492]) ).
fof(f2851,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f1498]) ).
fof(f3218,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,X0),X1)) ),
inference(cnf_transformation,[],[f1701]) ).
fof(f3225,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f1704]) ).
fof(f3394,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(scratc541474510d_n_eq,X0),X1)) ),
inference(cnf_transformation,[],[f1803]) ).
fof(f3395,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(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X2))) ),
inference(cnf_transformation,[],[f1803]) ).
fof(f3511,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1865]) ).
fof(f3646,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f1931]) ).
fof(f3716,plain,
~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f967]) ).
fof(f4061,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f4063,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f4061]) ).
fof(f4064,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f3716,f4061]) ).
fof(f4065,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f4063,f2240]) ).
fof(f4066,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f4063,f2241]) ).
fof(f4067,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f4063,f2242]) ).
fof(f4080,definition,
( spl29_2
<=> scratc213556589_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f4082,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f4080]) ).
fof(f4083,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f4066,f4061,f4080]) ).
fof(f4085,definition,
( spl29_3
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f4087,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f4085]) ).
fof(f4088,plain,
( spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f4065,f4061,f4085]) ).
fof(f4090,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f4082,f2239]) ).
fof(f4091,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f4090,f4087]) ).
fof(f4093,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f4094,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f4093]) ).
fof(f4095,plain,
( spl29_4
| ~ spl29_2
| ~ spl29_3 ),
inference(avatar_split_clause,[],[f4091,f4085,f4080,f4093]) ).
fof(f4770,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_cu))
| pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(resolution,[],[f4094,f2838]) ).
fof(f4981,plain,
( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f4770,f2252]) ).
fof(f5058,definition,
( spl29_5
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f5060,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_5 ),
inference(avatar_component_clause,[],[f5058]) ).
fof(f5061,plain,
( ~ spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f4067,f4061,f5058]) ).
fof(f5062,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_5 ),
inference(resolution,[],[f5060,f2851]) ).
fof(f5101,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f5103,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f5101]) ).
fof(f5104,plain,
( ~ spl29_6
| spl29_5 ),
inference(avatar_split_clause,[],[f5062,f5058,f5101]) ).
fof(f5106,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(resolution,[],[f5103,f2240]) ).
fof(f5107,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
| spl29_6 ),
inference(resolution,[],[f5103,f2241]) ).
fof(f5108,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_6 ),
inference(resolution,[],[f5103,f2242]) ).
fof(f5121,definition,
( spl29_7
<=> scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f5123,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),aTP_Lamm_a)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f5121]) ).
fof(f5124,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f5107,f5101,f5121]) ).
fof(f5126,definition,
( spl29_8
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f5128,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_8 ),
inference(avatar_component_clause,[],[f5126]) ).
fof(f5129,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f5108,f5101,f5126]) ).
fof(f5130,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_8 ),
inference(resolution,[],[f5128,f3225]) ).
fof(f5176,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f5178,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_9 ),
inference(avatar_component_clause,[],[f5176]) ).
fof(f5179,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f5130,f5126,f5176]) ).
fof(f5181,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_9 ),
inference(resolution,[],[f5178,f2240]) ).
fof(f5182,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
| spl29_9 ),
inference(resolution,[],[f5178,f2241]) ).
fof(f5183,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_9 ),
inference(resolution,[],[f5178,f2242]) ).
fof(f5196,definition,
( spl29_10
<=> scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f5198,plain,
( scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f5196]) ).
fof(f5199,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f5182,f5176,f5196]) ).
fof(f5201,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_10 ),
inference(resolution,[],[f5198,f2239]) ).
fof(f5202,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| spl29_9
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f5201,f5181]) ).
fof(f5204,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f5123,f2239]) ).
fof(f5205,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f5204,f5106]) ).
fof(f5207,definition,
( spl29_11
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f5208,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f5207]) ).
fof(f5209,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f5205,f5121,f5101,f5207]) ).
fof(f6173,definition,
( spl29_12
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f6174,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),X0)) )
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f6173]) ).
fof(f6175,plain,
( spl29_12
| spl29_9
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f5202,f5196,f5176,f6173]) ).
fof(f6366,definition,
( spl29_15
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f6368,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_15 ),
inference(avatar_component_clause,[],[f6366]) ).
fof(f6369,plain,
( spl29_15
| spl29_9 ),
inference(avatar_split_clause,[],[f5181,f5176,f6366]) ).
fof(f7079,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aTP_Lamm_gd))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_12 ),
inference(resolution,[],[f6174,f2550]) ).
fof(f7222,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_12 ),
inference(forward_subsumption_resolution,[],[f7079,f2287]) ).
fof(f7332,definition,
( spl29_16
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
fof(f7334,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_16 ),
inference(avatar_component_clause,[],[f7332]) ).
fof(f7335,plain,
( ~ spl29_16
| spl29_9 ),
inference(avatar_split_clause,[],[f5183,f5176,f7332]) ).
fof(f7336,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_16 ),
inference(resolution,[],[f7334,f3394]) ).
fof(f7337,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_16 ),
inference(resolution,[],[f7334,f3395]) ).
fof(f7384,definition,
( spl29_17
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).
fof(f7386,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))),aa_TPTP_ind_TPTP_ind(scratc542196088d_n_pf(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| spl29_17 ),
inference(avatar_component_clause,[],[f7384]) ).
fof(f7387,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f7337,f7332,f7384]) ).
fof(f7389,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_17 ),
inference(resolution,[],[f7386,f3646]) ).
fof(f7451,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc541474510d_n_eq,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_12
| spl29_17 ),
inference(forward_subsumption_resolution,[],[f7389,f7222]) ).
fof(f7452,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_12
| spl29_16
| spl29_17 ),
inference(forward_subsumption_resolution,[],[f7451,f7336]) ).
fof(f7454,definition,
( spl29_18
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_18])],[avatar_definition]) ).
fof(f7456,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_18 ),
inference(avatar_component_clause,[],[f7454]) ).
fof(f7457,plain,
( ~ spl29_18
| ~ spl29_12
| spl29_16
| spl29_17 ),
inference(avatar_split_clause,[],[f7452,f7384,f7332,f6173,f7454]) ).
fof(f7471,plain,
( ! [X0] :
( ~ scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) )
| spl29_18 ),
inference(resolution,[],[f7456,f2239]) ).
fof(f7505,plain,
( ! [X0] :
( ~ scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) )
| ~ spl29_15
| spl29_18 ),
inference(forward_subsumption_resolution,[],[f7471,f6368]) ).
fof(f7507,definition,
( spl29_19
<=> ! [X0] :
( ~ scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f7508,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_cr(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))))
| ~ scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),X0) )
| ~ spl29_19 ),
inference(avatar_component_clause,[],[f7507]) ).
fof(f7509,plain,
( spl29_19
| ~ spl29_15
| spl29_18 ),
inference(avatar_split_clause,[],[f7505,f7454,f6366,f7507]) ).
fof(f7510,plain,
( ~ scratc213556589_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_19 ),
inference(resolution,[],[f7508,f3511]) ).
fof(f7526,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| ~ spl29_10
| ~ spl29_19 ),
inference(forward_subsumption_resolution,[],[f7510,f5198]) ).
fof(f7528,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f7530,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))))
| spl29_20 ),
inference(avatar_component_clause,[],[f7528]) ).
fof(f7531,plain,
( ~ spl29_20
| ~ spl29_10
| ~ spl29_19 ),
inference(avatar_split_clause,[],[f7526,f7507,f5196,f7528]) ).
fof(f7539,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_12
| spl29_20 ),
inference(resolution,[],[f7530,f6174]) ).
fof(f7671,definition,
( spl29_25
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ),
introduced(definition,[new_symbols(definition,[spl29_25])],[avatar_definition]) ).
fof(f7673,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cs(sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| spl29_25 ),
inference(avatar_component_clause,[],[f7671]) ).
fof(f7674,plain,
( ~ spl29_25
| ~ spl29_12
| spl29_20 ),
inference(avatar_split_clause,[],[f7539,f7528,f6173,f7671]) ).
fof(f7960,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_25 ),
inference(resolution,[],[f7673,f3218]) ).
fof(f9770,definition,
( spl29_118
<=> pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_118])],[avatar_definition]) ).
fof(f9772,plain,
( pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_118 ),
inference(avatar_component_clause,[],[f9770]) ).
fof(f9773,plain,
( spl29_118
| ~ spl29_4 ),
inference(avatar_split_clause,[],[f4981,f4093,f9770]) ).
fof(f10775,definition,
( spl29_165
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_165])],[avatar_definition]) ).
fof(f10777,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| spl29_165 ),
inference(avatar_component_clause,[],[f10775]) ).
fof(f10778,plain,
( ~ spl29_165
| spl29_25 ),
inference(avatar_split_clause,[],[f7960,f7671,f10775]) ).
fof(f11434,plain,
( ~ pp(aa_fun171081125l_bool(scratc1576304300all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ct,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_11
| spl29_165 ),
inference(resolution,[],[f10777,f5208]) ).
fof(f11474,plain,
( $false
| ~ spl29_11
| ~ spl29_118
| spl29_165 ),
inference(forward_subsumption_resolution,[],[f11434,f9772]) ).
fof(f11475,plain,
( ~ spl29_11
| ~ spl29_118
| spl29_165 ),
inference(avatar_contradiction_clause,[],[f11474]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f4064]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f4083]) ).
cnf(s3,plain,
( spl29_1
| spl29_3 ),
inference(sat_conversion,[],[f4088]) ).
cnf(s4,plain,
( ~ spl29_2
| ~ spl29_3
| spl29_4 ),
inference(sat_conversion,[],[f4095]) ).
cnf(s5,plain,
( spl29_1
| ~ spl29_5 ),
inference(sat_conversion,[],[f5061]) ).
cnf(s6,plain,
( spl29_5
| ~ spl29_6 ),
inference(sat_conversion,[],[f5104]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f5124]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f5129]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f5179]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f5199]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f5209]) ).
cnf(s12,plain,
( spl29_9
| ~ spl29_10
| spl29_12 ),
inference(sat_conversion,[],[f6175]) ).
cnf(s15,plain,
( spl29_9
| spl29_15 ),
inference(sat_conversion,[],[f6369]) ).
cnf(s16,plain,
( spl29_9
| ~ spl29_16 ),
inference(sat_conversion,[],[f7335]) ).
cnf(s17,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f7387]) ).
cnf(s18,plain,
( ~ spl29_12
| spl29_16
| spl29_17
| ~ spl29_18 ),
inference(sat_conversion,[],[f7457]) ).
cnf(s19,plain,
( ~ spl29_15
| spl29_18
| spl29_19 ),
inference(sat_conversion,[],[f7509]) ).
cnf(s20,plain,
( ~ spl29_10
| ~ spl29_19
| ~ spl29_20 ),
inference(sat_conversion,[],[f7531]) ).
cnf(s25,plain,
( ~ spl29_12
| spl29_20
| ~ spl29_25 ),
inference(sat_conversion,[],[f7674]) ).
cnf(s116,plain,
( ~ spl29_4
| spl29_118 ),
inference(sat_conversion,[],[f9773]) ).
cnf(s162,plain,
( spl29_25
| ~ spl29_165 ),
inference(sat_conversion,[],[f10778]) ).
cnf(s174,plain,
( ~ spl29_11
| ~ spl29_118
| spl29_165 ),
inference(sat_conversion,[],[f11475]) ).
cnf(s175,plain,
~ spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s176,plain,
spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s177,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s180,plain,
~ spl29_6,
inference(rat,[],[s6,s175]) ).
cnf(s185,plain,
spl29_4,
inference(rat,[],[s4,s176,s177]) ).
cnf(s188,plain,
~ spl29_8,
inference(rat,[],[s8,s180]) ).
cnf(s189,plain,
spl29_7,
inference(rat,[],[s7,s180]) ).
cnf(s195,plain,
spl29_118,
inference(rat,[],[s116,s185]) ).
cnf(s231,plain,
~ spl29_9,
inference(rat,[],[s9,s188]) ).
cnf(s232,plain,
spl29_11,
inference(rat,[],[s11,s180,s189]) ).
cnf(s233,plain,
~ spl29_16,
inference(rat,[],[s16,s231]) ).
cnf(s234,plain,
spl29_15,
inference(rat,[],[s15,s231]) ).
cnf(s235,plain,
spl29_10,
inference(rat,[],[s10,s231]) ).
cnf(s236,plain,
spl29_165,
inference(rat,[],[s174,s195,s232]) ).
cnf(s276,plain,
~ spl29_17,
inference(rat,[],[s17,s233]) ).
cnf(s279,plain,
spl29_12,
inference(rat,[],[s12,s231,s235]) ).
cnf(s280,plain,
spl29_25,
inference(rat,[],[s162,s236]) ).
cnf(s326,plain,
spl29_20,
inference(rat,[],[s25,s280,s279]) ).
cnf(s327,plain,
~ spl29_18,
inference(rat,[],[s18,s276,s233,s279]) ).
cnf(s332,plain,
~ spl29_19,
inference(rat,[],[s20,s235,s326]) ).
cnf(s336,plain,
$false,
inference(rat,[],[s19,s234,s332,s327]) ).
fof(f11476,plain,
$false,
inference(avatar_sat_refutation,[],[s336]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM750+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 21:14:40 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 Running first-order theorem proving
% 0.13/0.38 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
% 11.31/2.22 % (1786780)Detected formulas, will run a generic FOF schedule.
% 11.31/2.22 % (1786790)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=917126021:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.31/2.22 % (1786791)dis-21_1_sil=8000:lcm=predicate:random_seed=1165039879: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)
% 11.31/2.22 % (1786789)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=540346523:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.31/2.22 % (1786785)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=1096255488:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.31/2.22 % (1786788)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3682149726:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.31/2.22 % (1786787)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=66920436:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.31/2.22 % (1786786)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=4285283654:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.31/2.22 % (1786788)Refutation not found, incomplete strategy
% 11.31/2.22 % (1786788)------------------------------
% 11.31/2.22 % (1786788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.22 % (1786788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.22 % (1786788)CaDiCaL version: 2.1.3
% 11.31/2.22 % (1786788)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.22 % (1786788)Time elapsed: 0.004 s
% 11.31/2.22 % (1786788)Peak memory usage: 88 MB
% 11.31/2.22 % (1786788)Instructions burned: 4 (million)
% 11.31/2.22 % (1786789)Refutation not found, incomplete strategy
% 11.31/2.22 % (1786789)------------------------------
% 11.31/2.22 % (1786789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.22 % (1786789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.22 % (1786789)CaDiCaL version: 2.1.3
% 11.31/2.22 % (1786789)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.22 % (1786789)Time elapsed: 0.004 s
% 11.31/2.22 % (1786789)Peak memory usage: 88 MB
% 11.31/2.22 % (1786789)Instructions burned: 5 (million)
% 11.31/2.22 % (1786790)Instruction limit reached!
% 11.31/2.22 % (1786790)------------------------------
% 11.31/2.22 % (1786790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.22 % (1786790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.22 % (1786790)CaDiCaL version: 2.1.3
% 11.31/2.22 % (1786790)Termination reason: Instruction limit
% 11.31/2.22 % (1786790)Termination phase: Saturation
% 11.31/2.22 % (1786790)Time elapsed: 0.037 s
% 11.31/2.22 % (1786790)Peak memory usage: 91 MB
% 11.31/2.22 % (1786790)Instructions burned: 140 (million)
% 11.31/2.22 % (1786791)Instruction limit reached!
% 11.31/2.22 % (1786791)------------------------------
% 11.31/2.22 % (1786791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.22 % (1786791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.22 % (1786791)CaDiCaL version: 2.1.3
% 11.31/2.22 % (1786791)Termination reason: Instruction limit
% 11.31/2.22 % (1786791)Termination phase: Saturation
% 11.31/2.22 % (1786791)Time elapsed: 0.060 s
% 11.31/2.22 % (1786791)Peak memory usage: 90 MB
% 11.31/2.22 % (1786791)Instructions burned: 129 (million)
% 11.31/2.22 % (1786799)lrs+10_1_sil=8000:sp=occurrence:random_seed=1166668306:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.31/2.22 % (1786799)Refutation not found, incomplete strategy
% 11.31/2.22 % (1786799)------------------------------
% 11.31/2.22 % (1786799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.22 % (1786799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.22 % (1786799)CaDiCaL version: 2.1.3
% 11.31/2.22 % (1786799)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.22 % (1786799)Time elapsed: 0.004 s
% 11.31/2.22 % (1786799)Peak memory usage: 89 MB
% 11.31/2.22 % (1786799)Instructions burned: 4 (million)
% 11.31/2.22 % (1786800)lrs+10_1_sil=32000:urr=on:br=off:random_seed=320886991:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 18.00/3.17 % (1786800)Refutation not found, incomplete strategy
% 18.00/3.17 % (1786800)------------------------------
% 18.00/3.17 % (1786800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.17 % (1786800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.17 % (1786800)CaDiCaL version: 2.1.3
% 18.00/3.17 % (1786800)Termination reason: Refutation not found, incomplete strategy
% 18.00/3.17 % (1786800)Time elapsed: 0.008 s
% 18.00/3.17 % (1786800)Peak memory usage: 89 MB
% 18.00/3.17 % (1786800)Instructions burned: 15 (million)
% 18.00/3.17 % (1786788)------------------------------
% 18.00/3.17 % (1786788)------------------------------
% 18.00/3.17 % (1786789)------------------------------
% 18.00/3.17 % (1786789)------------------------------
% 18.00/3.17 % (1786799)------------------------------
% 18.00/3.17 % (1786799)------------------------------
% 18.00/3.17 % (1786804)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=3983764117:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 18.00/3.17 % (1786803)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2626293282:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 18.00/3.17 % (1786803)Refutation not found, incomplete strategy
% 18.00/3.17 % (1786803)------------------------------
% 18.00/3.17 % (1786803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.17 % (1786803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.17 % (1786803)CaDiCaL version: 2.1.3
% 18.00/3.17 % (1786803)Termination reason: Refutation not found, incomplete strategy
% 18.00/3.17 % (1786803)Time elapsed: 0.006 s
% 18.00/3.17 % (1786803)Peak memory usage: 89 MB
% 18.00/3.17 % (1786803)Instructions burned: 7 (million)
% 18.00/3.17 % (1786800)------------------------------
% 18.00/3.17 % (1786800)------------------------------
% 18.00/3.17 % (1786805)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2759599395:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 18.00/3.17 % (1786805)Refutation not found, incomplete strategy
% 18.00/3.17 % (1786805)------------------------------
% 18.00/3.17 % (1786805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.17 % (1786805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.17 % (1786805)CaDiCaL version: 2.1.3
% 18.00/3.17 % (1786805)Termination reason: Refutation not found, incomplete strategy
% 18.00/3.17 % (1786805)Time elapsed: 0.004 s
% 18.00/3.17 % (1786805)Peak memory usage: 89 MB
% 18.00/3.17 % (1786805)Instructions burned: 10 (million)
% 18.00/3.17 % (1786804)Instruction limit reached!
% 18.00/3.17 % (1786804)------------------------------
% 18.00/3.17 % (1786804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.17 % (1786804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.17 % (1786804)CaDiCaL version: 2.1.3
% 18.00/3.17 % (1786804)Termination reason: Instruction limit
% 18.00/3.17 % (1786804)Termination phase: Saturation
% 18.00/3.17 % (1786804)Time elapsed: 0.133 s
% 18.00/3.17 % (1786804)Peak memory usage: 97 MB
% 18.00/3.17 % (1786804)Instructions burned: 248 (million)
% 18.00/3.17 % (1786808)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=311270197:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 18.00/3.17 % (1786805)------------------------------
% 18.00/3.17 % (1786805)------------------------------
% 18.00/3.17 % (1786803)------------------------------
% 18.00/3.17 % (1786803)------------------------------
% 18.00/3.17 % (1786810)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1090063436:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 18.00/3.17 % (1786812)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2292841389:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 18.00/3.17 % (1786810)Instruction limit reached!
% 18.00/3.17 % (1786810)------------------------------
% 18.00/3.17 % (1786810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.00/3.17 % (1786810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.00/3.17 % (1786810)CaDiCaL version: 2.1.3
% 18.00/3.17 % (1786810)Termination reason: Instruction limit
% 18.00/3.17 % (1786810)Termination phase: Saturation
% 18.00/3.17 % (1786810)Time elapsed: 0.056 s
% 21.32/3.75 % (1786810)Peak memory usage: 90 MB
% 21.32/3.75 % (1786810)Instructions burned: 115 (million)
% 21.32/3.75 % (1786812)Instruction limit reached!
% 21.32/3.75 % (1786812)------------------------------
% 21.32/3.75 % (1786812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786812)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786812)Termination reason: Instruction limit
% 21.32/3.75 % (1786812)Termination phase: Saturation
% 21.32/3.75 % (1786812)Time elapsed: 0.030 s
% 21.32/3.75 % (1786812)Peak memory usage: 90 MB
% 21.32/3.75 % (1786812)Instructions burned: 127 (million)
% 21.32/3.75 % (1786813)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3691432569:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 21.32/3.75 % (1786813)Instruction limit reached!
% 21.32/3.75 % (1786813)------------------------------
% 21.32/3.75 % (1786813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786813)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786813)Termination reason: Instruction limit
% 21.32/3.75 % (1786813)Termination phase: Saturation
% 21.32/3.75 % (1786813)Time elapsed: 0.061 s
% 21.32/3.75 % (1786813)Peak memory usage: 90 MB
% 21.32/3.75 % (1786813)Instructions burned: 114 (million)
% 21.32/3.75 % (1786816)lrs+10_1_sil=8000:sp=occurrence:random_seed=4118381599:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 21.32/3.75 % (1786817)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=60675029:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 21.32/3.75 % (1786817)Refutation not found, incomplete strategy
% 21.32/3.75 % (1786817)------------------------------
% 21.32/3.75 % (1786817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786817)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786817)Termination reason: Refutation not found, incomplete strategy
% 21.32/3.75 % (1786817)Time elapsed: 0.037 s
% 21.32/3.75 % (1786817)Peak memory usage: 92 MB
% 21.32/3.75 % (1786817)Instructions burned: 139 (million)
% 21.32/3.75 % (1786819)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1427360898:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 21.32/3.75 % (1786817)------------------------------
% 21.32/3.75 % (1786817)------------------------------
% 21.32/3.75 % (1786823)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=245474545:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 21.32/3.75 % (1786823)Instruction limit reached!
% 21.32/3.75 % (1786823)------------------------------
% 21.32/3.75 % (1786823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786823)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786823)Termination reason: Instruction limit
% 21.32/3.75 % (1786823)Termination phase: Saturation
% 21.32/3.75 % (1786823)Time elapsed: 0.036 s
% 21.32/3.75 % (1786823)Peak memory usage: 92 MB
% 21.32/3.75 % (1786823)Instructions burned: 134 (million)
% 21.32/3.75 % (1786825)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3278517177:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 21.32/3.75 % (1786825)Refutation not found, incomplete strategy
% 21.32/3.75 % (1786825)------------------------------
% 21.32/3.75 % (1786825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786825)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786825)Termination reason: Refutation not found, incomplete strategy
% 21.32/3.75 % (1786825)Time elapsed: 0.009 s
% 21.32/3.75 % (1786825)Peak memory usage: 89 MB
% 21.32/3.75 % (1786825)Instructions burned: 31 (million)
% 21.32/3.75 % (1786816)Instruction limit reached!
% 21.32/3.75 % (1786816)------------------------------
% 21.32/3.75 % (1786816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786816)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786816)Termination reason: Instruction limit
% 21.32/3.75 % (1786816)Termination phase: Saturation
% 21.32/3.75 % (1786816)Time elapsed: 0.541 s
% 21.32/3.75 % (1786816)Peak memory usage: 102 MB
% 21.32/3.75 % (1786816)Instructions burned: 909 (million)
% 21.32/3.75 % (1786825)------------------------------
% 21.32/3.75 % (1786825)------------------------------
% 21.32/3.75 % (1786827)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1966023028:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 21.32/3.75 % (1786828)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=4104063943:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 21.32/3.75 % (1786828)Refutation not found, incomplete strategy
% 21.32/3.75 % (1786828)------------------------------
% 21.32/3.75 % (1786828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786828)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786828)Termination reason: Refutation not found, incomplete strategy
% 21.32/3.75 % (1786828)Time elapsed: 0.006 s
% 21.32/3.75 % (1786828)Peak memory usage: 89 MB
% 21.32/3.75 % (1786828)Instructions burned: 19 (million)
% 21.32/3.75 % (1786828)------------------------------
% 21.32/3.75 % (1786828)------------------------------
% 21.32/3.75 % (1786831)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3761696381:i=134:gtgl=5:slsql=off:gtg=exists_sym_2979 on theBenchmark for (2979ds/134Mi)
% 21.32/3.75 % (1786831)Instruction limit reached!
% 21.32/3.75 % (1786831)------------------------------
% 21.32/3.75 % (1786831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786831)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786831)Termination reason: Instruction limit
% 21.32/3.75 % (1786831)Termination phase: Property scanning
% 21.32/3.75 % (1786831)Time elapsed: 0.034 s
% 21.32/3.75 % (1786831)Peak memory usage: 90 MB
% 21.32/3.75 % (1786831)Instructions burned: 137 (million)
% 21.32/3.75 % (1786808)Instruction limit reached!
% 21.32/3.75 % (1786808)------------------------------
% 21.32/3.75 % (1786808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786808)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786808)Termination reason: Instruction limit
% 21.32/3.75 % (1786808)Termination phase: Saturation
% 21.32/3.75 % (1786808)Time elapsed: 1.481 s
% 21.32/3.75 % (1786808)Peak memory usage: 153 MB
% 21.32/3.75 % (1786808)Instructions burned: 2351 (million)
% 21.32/3.75 % (1786833)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3122107214:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 21.32/3.75 % (1786833)Refutation not found, incomplete strategy
% 21.32/3.75 % (1786833)------------------------------
% 21.32/3.75 % (1786833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786833)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786833)Termination reason: Refutation not found, incomplete strategy
% 21.32/3.75 % (1786833)Time elapsed: 0.002 s
% 21.32/3.75 % (1786833)Peak memory usage: 89 MB
% 21.32/3.75 % (1786833)Instructions burned: 4 (million)
% 21.32/3.75 % (1786833)------------------------------
% 21.32/3.75 % (1786833)------------------------------
% 21.32/3.75 % (1786834)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=661545561:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 21.32/3.75 % (1786834)Refutation not found, incomplete strategy
% 21.32/3.75 % (1786834)------------------------------
% 21.32/3.75 % (1786834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786834)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786834)Termination reason: Refutation not found, incomplete strategy
% 21.32/3.75 % (1786834)Time elapsed: 0.004 s
% 21.32/3.75 % (1786834)Peak memory usage: 89 MB
% 21.32/3.75 % (1786834)Instructions burned: 4 (million)
% 21.32/3.75 % (1786836)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=437631753:i=6060:aac=none:ins=25_2975 on theBenchmark for (2975ds/6060Mi)
% 21.32/3.75 % (1786834)------------------------------
% 21.32/3.75 % (1786834)------------------------------
% 21.32/3.75 % (1786787)First to succeed.
% 21.32/3.75 % (1786787)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1786780"
% 21.32/3.75 % (1786839)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1614021821:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 21.32/3.75 % (1786839)Instruction limit reached!
% 21.32/3.75 % (1786839)------------------------------
% 21.32/3.75 % (1786839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/3.75 % (1786839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/3.75 % (1786839)CaDiCaL version: 2.1.3
% 21.32/3.75 % (1786839)Termination reason: Instruction limit
% 21.32/3.75 % (1786839)Termination phase: Saturation
% 21.32/3.75 % (1786839)Time elapsed: 0.070 s
% 21.32/3.75 % (1786839)Peak memory usage: 91 MB
% 21.32/3.75 % (1786839)Instructions burned: 150 (million)
% 21.32/3.75 % (1786841)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3885536859:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 21.32/3.75 % (1786787)Refutation found. Thanks to Tanya!
% 21.32/3.75 % SZS status Theorem for theBenchmark
% 21.32/3.75 % SZS output start Proof for theBenchmark
% See solution above
% 22.66/3.95 % (1786787)------------------------------
% 22.66/3.95 % (1786787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.66/3.95 % (1786787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.66/3.95 % (1786787)CaDiCaL version: 2.1.3
% 22.66/3.95 % (1786787)Termination reason: Refutation
% 22.66/3.95 % (1786787)Time elapsed: 2.725 s
% 22.66/3.95 % (1786787)Peak memory usage: 169 MB
% 22.66/3.95 % (1786787)Instructions burned: 4567 (million)
% 22.66/3.95 % (1786787)------------------------------
% 22.66/3.95 % (1786787)------------------------------
% 22.66/3.95 % (1786780)Success in time 3.172 s
% 22.66/3.95 % Vampire exiting
%------------------------------------------------------------------------------