%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM792+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:04 PM UTC 2026
% Result : Theorem 32.84s 5.55s
% Output : Refutation 33.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 47
% Syntax : Number of formulae : 271 ( 44 unt; 29 def)
% Number of atoms : 729 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 799 ( 341 ~; 358 |; 40 &)
% ( 51 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 33 ( 32 usr; 30 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 15 con; 0-2 aty)
% Number of variables : 168 ( 0 sgn 166 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f222,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc795021421_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f224,axiom,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ce)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz87b) ).
fof(f228,axiom,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_co)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz84) ).
fof(f237,axiom,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_dg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz83) ).
fof(f238,axiom,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_di)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz82) ).
fof(f773,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_di,X0))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__236) ).
fof(f774,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__237) ).
fof(f783,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_co,X0))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__246) ).
fof(f787,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ce,X0))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__250) ).
fof(f788,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__251) ).
fof(f836,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__299) ).
fof(f838,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__301) ).
fof(f839,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__302) ).
fof(f1034,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cd,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__497) ).
fof(f1035,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__498) ).
fof(f1085,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(scratc1313003373moreis,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__548) ).
fof(f1087,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__550) ).
fof(f1315,conjecture,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1316,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(negated_conjecture,[status(cth)],[f1315]) ).
fof(f1317,plain,
~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(flattening,[],[f1316]) ).
fof(f1334,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc795021421_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f222]) ).
fof(f1335,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc795021421_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1334]) ).
fof(f1410,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f836]) ).
fof(f1412,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1)) ) ),
inference(ennf_transformation,[],[f838]) ).
fof(f1413,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) ),
inference(ennf_transformation,[],[f839]) ).
fof(f1478,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(scratc2116345507t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) ),
inference(ennf_transformation,[],[f1085]) ).
fof(f1479,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(scratc2116345507t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) ),
inference(flattening,[],[f1478]) ).
fof(f1482,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) ),
inference(ennf_transformation,[],[f1087]) ).
fof(f1483,plain,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) ),
inference(flattening,[],[f1482]) ).
fof(f1767,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc795021421_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc795021421_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1335]) ).
fof(f1768,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc795021421_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc795021421_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1)) ) ),
inference(rectify,[],[f1767]) ).
fof(f1769,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc795021421_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc795021421_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1768]) ).
fof(f2024,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_di,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_di,X0)) ) ),
inference(nnf_transformation,[],[f773]) ).
fof(f2025,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0)) ) ),
inference(nnf_transformation,[],[f774]) ).
fof(f2034,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_co,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_co,X0)) ) ),
inference(nnf_transformation,[],[f783]) ).
fof(f2038,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ce,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ce,X0)) ) ),
inference(nnf_transformation,[],[f787]) ).
fof(f2039,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0)) ) ),
inference(nnf_transformation,[],[f788]) ).
fof(f2102,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1)) ) ),
inference(nnf_transformation,[],[f1410]) ).
fof(f2103,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1)) ) ),
inference(flattening,[],[f2102]) ).
fof(f2106,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1)) ) ),
inference(nnf_transformation,[],[f1412]) ).
fof(f2107,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1)) ) ),
inference(flattening,[],[f2106]) ).
fof(f2108,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1)) ) ),
inference(nnf_transformation,[],[f1413]) ).
fof(f2109,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1)) ) ),
inference(flattening,[],[f2108]) ).
fof(f2337,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cd,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cd,X0),X1)) ) ),
inference(nnf_transformation,[],[f1034]) ).
fof(f2338,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc1483262892all_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,[],[f1035]) ).
fof(f2411,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(scratc2116345507t_more,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1479]) ).
fof(f2412,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(scratc2116345507t_more,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1),X2)) ) ),
inference(flattening,[],[f2411]) ).
fof(f2415,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f1483]) ).
fof(f2416,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2)) ) ),
inference(flattening,[],[f2415]) ).
fof(f3049,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc795021421_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3050,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3051,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| scratc795021421_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3052,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f3055,plain,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ce)),
inference(cnf_transformation,[],[f224]) ).
fof(f3059,plain,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_co)),
inference(cnf_transformation,[],[f228]) ).
fof(f3068,plain,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_dg)),
inference(cnf_transformation,[],[f237]) ).
fof(f3069,plain,
pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_di)),
inference(cnf_transformation,[],[f238]) ).
fof(f3869,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_di,X0)) ),
inference(cnf_transformation,[],[f2024]) ).
fof(f3871,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_dg,X0)) ),
inference(cnf_transformation,[],[f2025]) ).
fof(f3889,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_co,X0)) ),
inference(cnf_transformation,[],[f2034]) ).
fof(f3897,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ce,X0)) ),
inference(cnf_transformation,[],[f2038]) ).
fof(f3898,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ce,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) ),
inference(cnf_transformation,[],[f2038]) ).
fof(f3900,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ac,X0))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,X0))) ),
inference(cnf_transformation,[],[f2039]) ).
fof(f4008,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,X0),X1)) ),
inference(cnf_transformation,[],[f2103]) ).
fof(f4014,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,X0),X1)) ),
inference(cnf_transformation,[],[f2107]) ).
fof(f4017,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,X0),X1)) ),
inference(cnf_transformation,[],[f2109]) ).
fof(f4441,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cd,X0),X1)) ),
inference(cnf_transformation,[],[f2337]) ).
fof(f4444,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa(X0),X1))) ),
inference(cnf_transformation,[],[f2338]) ).
fof(f4568,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(scratc1313003373moreis,X0),X1)) ),
inference(cnf_transformation,[],[f2412]) ).
fof(f4569,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(scratc2116345507t_more,X1),X2)) ),
inference(cnf_transformation,[],[f2412]) ).
fof(f4570,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(scratc2116345507t_more,X0),X2)) ),
inference(cnf_transformation,[],[f2412]) ).
fof(f4575,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,X1),X2))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),X1),X2)) ),
inference(cnf_transformation,[],[f2416]) ).
fof(f5205,plain,
~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac)),
inference(cnf_transformation,[],[f1317]) ).
fof(f5565,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f5567,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ac))
| spl29_1 ),
inference(avatar_component_clause,[],[f5565]) ).
fof(f5568,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f5205,f5565]) ).
fof(f5569,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| spl29_1 ),
inference(resolution,[],[f5567,f3050]) ).
fof(f5570,plain,
( scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f5567,f3051]) ).
fof(f5571,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_1 ),
inference(resolution,[],[f5567,f3052]) ).
fof(f5584,definition,
( spl29_2
<=> scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f5586,plain,
( scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f5584]) ).
fof(f5587,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f5570,f5565,f5584]) ).
fof(f5589,definition,
( spl29_3
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac)) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f5591,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ spl29_3 ),
inference(avatar_component_clause,[],[f5589]) ).
fof(f5592,plain,
( spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f5569,f5565,f5589]) ).
fof(f5594,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f5586,f3049]) ).
fof(f5595,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2
| ~ spl29_3 ),
inference(forward_subsumption_resolution,[],[f5594,f5591]) ).
fof(f5597,definition,
( spl29_4
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f5598,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f5597]) ).
fof(f5599,plain,
( spl29_4
| ~ spl29_2
| ~ spl29_3 ),
inference(avatar_split_clause,[],[f5595,f5589,f5584,f5597]) ).
fof(f6565,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_co))
| pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(resolution,[],[f5598,f3889]) ).
fof(f6843,plain,
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f6565,f3059]) ).
fof(f6968,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(f6970,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| spl29_5 ),
inference(avatar_component_clause,[],[f6968]) ).
fof(f6971,plain,
( ~ spl29_5
| spl29_1 ),
inference(avatar_split_clause,[],[f5571,f5565,f6968]) ).
fof(f6972,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_5 ),
inference(resolution,[],[f6970,f3900]) ).
fof(f7011,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc1483262892all_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(f7013,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| spl29_6 ),
inference(avatar_component_clause,[],[f7011]) ).
fof(f7014,plain,
( ~ spl29_6
| spl29_5 ),
inference(avatar_split_clause,[],[f6972,f6968,f7011]) ).
fof(f7016,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,[],[f7013,f3050]) ).
fof(f7017,plain,
( scratc795021421_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,[],[f7013,f3051]) ).
fof(f7018,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,[],[f7013,f3052]) ).
fof(f7031,definition,
( spl29_7
<=> scratc795021421_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(f7033,plain,
( scratc795021421_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,[],[f7031]) ).
fof(f7034,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f7017,f7011,f7031]) ).
fof(f7036,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(f7038,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,[],[f7036]) ).
fof(f7039,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f7018,f7011,f7036]) ).
fof(f7040,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_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,[],[f7038,f4444]) ).
fof(f7086,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc1483262892all_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(f7088,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_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,[],[f7086]) ).
fof(f7089,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f7040,f7036,f7086]) ).
fof(f7091,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,[],[f7088,f3050]) ).
fof(f7092,plain,
( scratc795021421_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,[],[f7088,f3051]) ).
fof(f7093,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,[],[f7088,f3052]) ).
fof(f7106,definition,
( spl29_10
<=> scratc795021421_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(f7108,plain,
( scratc795021421_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,[],[f7106]) ).
fof(f7109,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f7092,f7086,f7106]) ).
fof(f7111,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_10 ),
inference(resolution,[],[f7108,f3049]) ).
fof(f7112,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| spl29_9
| ~ spl29_10 ),
inference(forward_subsumption_resolution,[],[f7111,f7091]) ).
fof(f7114,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f7033,f3049]) ).
fof(f7115,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| spl29_6
| ~ spl29_7 ),
inference(forward_subsumption_resolution,[],[f7114,f7016]) ).
fof(f7117,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(scratc1483262892all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f7118,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f7117]) ).
fof(f7119,plain,
( spl29_11
| spl29_6
| ~ spl29_7 ),
inference(avatar_split_clause,[],[f7115,f7031,f7011,f7117]) ).
fof(f8096,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_di))
| pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(resolution,[],[f7118,f3869]) ).
fof(f8354,plain,
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f8096,f3069]) ).
fof(f8489,definition,
( spl29_12
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))) ),
introduced(definition,[new_symbols(definition,[spl29_12])],[avatar_definition]) ).
fof(f8491,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_12 ),
inference(avatar_component_clause,[],[f8489]) ).
fof(f8492,plain,
( spl29_12
| spl29_6 ),
inference(avatar_split_clause,[],[f7016,f7011,f8489]) ).
fof(f8494,definition,
( spl29_13
<=> ! [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(scratc1483262892all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f8495,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(scratc1483262892all_of(aTP_Lamm_a),X0)) )
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f8494]) ).
fof(f8496,plain,
( spl29_13
| spl29_9
| ~ spl29_10 ),
inference(avatar_split_clause,[],[f7112,f7106,f7086,f8494]) ).
fof(f9647,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_ce))
| pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,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_13 ),
inference(resolution,[],[f8495,f3897]) ).
fof(f9660,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aTP_Lamm_dg))
| pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,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_13 ),
inference(resolution,[],[f8495,f3871]) ).
fof(f9920,plain,
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,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_13 ),
inference(forward_subsumption_resolution,[],[f9660,f3068]) ).
fof(f9933,plain,
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,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_13 ),
inference(forward_subsumption_resolution,[],[f9647,f3055]) ).
fof(f10054,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(f10056,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,[],[f10054]) ).
fof(f10057,plain,
( ~ spl29_16
| spl29_9 ),
inference(avatar_split_clause,[],[f7093,f7086,f10054]) ).
fof(f10058,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,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,[],[f10056,f4568]) ).
fof(f10059,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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,[],[f10056,f4569]) ).
fof(f10060,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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,[],[f10056,f4570]) ).
fof(f10114,definition,
( spl29_18
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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(f10116,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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,[],[f10114]) ).
fof(f10117,plain,
( ~ spl29_18
| spl29_16 ),
inference(avatar_split_clause,[],[f10060,f10054,f10114]) ).
fof(f10120,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,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,aTP_Lamm_ac)))
| spl29_18 ),
inference(resolution,[],[f10116,f4017]) ).
fof(f10262,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,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(f10264,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1313003373moreis,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,[],[f10262]) ).
fof(f10265,plain,
( spl29_20
| spl29_16 ),
inference(avatar_split_clause,[],[f10058,f10054,f10262]) ).
fof(f10270,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,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(resolution,[],[f10264,f4008]) ).
fof(f10415,definition,
( spl29_26
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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_26])],[avatar_definition]) ).
fof(f10417,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2116345507t_more,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_26 ),
inference(avatar_component_clause,[],[f10415]) ).
fof(f10418,plain,
( spl29_26
| spl29_16 ),
inference(avatar_split_clause,[],[f10059,f10054,f10415]) ).
fof(f10420,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,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_26 ),
inference(resolution,[],[f10417,f4014]) ).
fof(f10710,definition,
( spl29_34
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,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_34])],[avatar_definition]) ).
fof(f10712,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_dh,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_34 ),
inference(avatar_component_clause,[],[f10710]) ).
fof(f10714,definition,
( spl29_35
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
fof(f10716,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))
| ~ spl29_35 ),
inference(avatar_component_clause,[],[f10714]) ).
fof(f10717,plain,
( ~ spl29_34
| spl29_35
| ~ spl29_26 ),
inference(avatar_split_clause,[],[f10420,f10415,f10714,f10710]) ).
fof(f10726,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_dh,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))))
| ~ spl29_13
| spl29_34 ),
inference(resolution,[],[f10712,f8495]) ).
fof(f10765,plain,
( $false
| ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(forward_subsumption_resolution,[],[f10726,f8354]) ).
fof(f10766,plain,
( ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(avatar_contradiction_clause,[],[f10765]) ).
fof(f10909,definition,
( spl29_37
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,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,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_37])],[avatar_definition]) ).
fof(f10911,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_df,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,aTP_Lamm_ac)))
| spl29_37 ),
inference(avatar_component_clause,[],[f10909]) ).
fof(f10913,definition,
( spl29_38
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_38])],[avatar_definition]) ).
fof(f10915,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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,aTP_Lamm_ac)))
| spl29_38 ),
inference(avatar_component_clause,[],[f10913]) ).
fof(f10916,plain,
( ~ spl29_37
| ~ spl29_38
| spl29_18 ),
inference(avatar_split_clause,[],[f10120,f10114,f10913,f10909]) ).
fof(f10925,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_df,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_4
| spl29_37 ),
inference(resolution,[],[f10911,f5598]) ).
fof(f10964,plain,
( $false
| ~ spl29_4
| ~ spl29_13
| spl29_37 ),
inference(forward_subsumption_resolution,[],[f10925,f9920]) ).
fof(f10965,plain,
( ~ spl29_4
| ~ spl29_13
| spl29_37 ),
inference(avatar_contradiction_clause,[],[f10964]) ).
fof(f11505,definition,
( spl29_54
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,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_54])],[avatar_definition]) ).
fof(f11507,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cn,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_54 ),
inference(avatar_component_clause,[],[f11505]) ).
fof(f11509,definition,
( spl29_55
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ),
introduced(definition,[new_symbols(definition,[spl29_55])],[avatar_definition]) ).
fof(f11511,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1179019761lessis,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ spl29_55 ),
inference(avatar_component_clause,[],[f11509]) ).
fof(f11512,plain,
( ~ spl29_54
| spl29_55
| ~ spl29_20 ),
inference(avatar_split_clause,[],[f10270,f10262,f11509,f11505]) ).
fof(f11521,plain,
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cn,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ spl29_11
| spl29_54 ),
inference(resolution,[],[f11507,f7118]) ).
fof(f11560,plain,
( $false
| ~ spl29_4
| ~ spl29_11
| spl29_54 ),
inference(forward_subsumption_resolution,[],[f11521,f6843]) ).
fof(f11561,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_54 ),
inference(avatar_contradiction_clause,[],[f11560]) ).
fof(f11567,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_55 ),
inference(resolution,[],[f11511,f4575]) ).
fof(f13243,definition,
( spl29_120
<=> pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,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_120])],[avatar_definition]) ).
fof(f13245,plain,
( pp(aa_fun171081125l_bool(scratc1483262892all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cd,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_120 ),
inference(avatar_component_clause,[],[f13243]) ).
fof(f13246,plain,
( spl29_120
| ~ spl29_13 ),
inference(avatar_split_clause,[],[f9933,f8494,f13243]) ).
fof(f13247,plain,
( pp(aa_TPTP_ind_bool(aTP_Lamm_ce,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_120 ),
inference(resolution,[],[f13245,f3898]) ).
fof(f18223,definition,
( spl29_236
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac))) ) ),
introduced(definition,[new_symbols(definition,[spl29_236])],[avatar_definition]) ).
fof(f18224,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_236 ),
inference(avatar_component_clause,[],[f18223]) ).
fof(f18225,plain,
( spl29_236
| ~ spl29_55 ),
inference(avatar_split_clause,[],[f11567,f11509,f18223]) ).
fof(f20521,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ac))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_236 ),
inference(resolution,[],[f18224,f3049]) ).
fof(f20557,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) )
| ~ spl29_3
| ~ spl29_236 ),
inference(forward_subsumption_resolution,[],[f20521,f5591]) ).
fof(f20560,definition,
( spl29_300
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac)))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_300])],[avatar_definition]) ).
fof(f20561,plain,
( ! [X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cc(X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),X1)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_300 ),
inference(avatar_component_clause,[],[f20560]) ).
fof(f20562,plain,
( spl29_300
| ~ spl29_3
| ~ spl29_236 ),
inference(avatar_split_clause,[],[f20557,f18223,f5589,f20560]) ).
fof(f20563,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ac),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(aTP_Lamm_cd,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_300 ),
inference(resolution,[],[f20561,f4441]) ).
fof(f20581,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(aTP_Lamm_cd,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) )
| ~ spl29_2
| ~ spl29_300 ),
inference(forward_subsumption_resolution,[],[f20563,f5586]) ).
fof(f20583,definition,
( spl29_301
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(aTP_Lamm_cd,X0),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_301])],[avatar_definition]) ).
fof(f20584,plain,
( ! [X0] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cd,X0),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(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac))) )
| ~ spl29_301 ),
inference(avatar_component_clause,[],[f20583]) ).
fof(f20585,plain,
( spl29_301
| ~ spl29_2
| ~ spl29_300 ),
inference(avatar_split_clause,[],[f20581,f20560,f5584,f20583]) ).
fof(f20597,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))))
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) )
| ~ spl29_301 ),
inference(resolution,[],[f20584,f3049]) ).
fof(f20632,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) )
| ~ spl29_12
| ~ spl29_301 ),
inference(forward_subsumption_resolution,[],[f20597,f8491]) ).
fof(f20634,definition,
( spl29_302
<=> ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) ) ),
introduced(definition,[new_symbols(definition,[spl29_302])],[avatar_definition]) ).
fof(f20635,plain,
( ! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,X0),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(scratc1253208871t_less,X0),sK12(aTP_Lamm_a,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X1)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X1),aa_TPT43085870d_bool(aTP_Lamm_cd,X0))) )
| ~ spl29_302 ),
inference(avatar_component_clause,[],[f20634]) ).
fof(f20636,plain,
( spl29_302
| ~ spl29_12
| ~ spl29_301 ),
inference(avatar_split_clause,[],[f20632,f20583,f8489,f20634]) ).
fof(f20637,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1253208871t_less,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,aTP_Lamm_ac)))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cd,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_35
| ~ spl29_302 ),
inference(resolution,[],[f20635,f10716]) ).
fof(f20696,plain,
( ! [X0] :
( ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cd,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_35
| spl29_38
| ~ spl29_302 ),
inference(forward_subsumption_resolution,[],[f20637,f10915]) ).
fof(f20698,definition,
( spl29_303
<=> ! [X0] :
( ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0)
| ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cd,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_303])],[avatar_definition]) ).
fof(f20699,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1483262892all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_cd,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))))))))
| ~ scratc795021421_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab,sK12(aTP_Lamm_a,aTP_Lamm_ac))),X0) )
| ~ spl29_303 ),
inference(avatar_component_clause,[],[f20698]) ).
fof(f20700,plain,
( spl29_303
| ~ spl29_35
| spl29_38
| ~ spl29_302 ),
inference(avatar_split_clause,[],[f20696,f20634,f10913,f10714,f20698]) ).
fof(f20702,plain,
( ~ scratc795021421_is_of(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(aTP_Lamm_ce,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_303 ),
inference(resolution,[],[f20699,f3897]) ).
fof(f20721,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ce,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_7
| ~ spl29_303 ),
inference(forward_subsumption_resolution,[],[f20702,f7033]) ).
fof(f20724,plain,
( $false
| ~ spl29_7
| ~ spl29_120
| ~ spl29_303 ),
inference(forward_subsumption_resolution,[],[f20721,f13247]) ).
fof(f20725,plain,
( ~ spl29_7
| ~ spl29_120
| ~ spl29_303 ),
inference(avatar_contradiction_clause,[],[f20724]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f5568]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f5587]) ).
cnf(s3,plain,
( spl29_1
| spl29_3 ),
inference(sat_conversion,[],[f5592]) ).
cnf(s4,plain,
( ~ spl29_2
| ~ spl29_3
| spl29_4 ),
inference(sat_conversion,[],[f5599]) ).
cnf(s5,plain,
( spl29_1
| ~ spl29_5 ),
inference(sat_conversion,[],[f6971]) ).
cnf(s6,plain,
( spl29_5
| ~ spl29_6 ),
inference(sat_conversion,[],[f7014]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f7034]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f7039]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f7089]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f7109]) ).
cnf(s11,plain,
( spl29_6
| ~ spl29_7
| spl29_11 ),
inference(sat_conversion,[],[f7119]) ).
cnf(s12,plain,
( spl29_6
| spl29_12 ),
inference(sat_conversion,[],[f8492]) ).
cnf(s13,plain,
( spl29_9
| ~ spl29_10
| spl29_13 ),
inference(sat_conversion,[],[f8496]) ).
cnf(s16,plain,
( spl29_9
| ~ spl29_16 ),
inference(sat_conversion,[],[f10057]) ).
cnf(s18,plain,
( spl29_16
| ~ spl29_18 ),
inference(sat_conversion,[],[f10117]) ).
cnf(s20,plain,
( spl29_16
| spl29_20 ),
inference(sat_conversion,[],[f10265]) ).
cnf(s26,plain,
( spl29_16
| spl29_26 ),
inference(sat_conversion,[],[f10418]) ).
cnf(s34,plain,
( ~ spl29_26
| ~ spl29_34
| spl29_35 ),
inference(sat_conversion,[],[f10717]) ).
cnf(s35,plain,
( ~ spl29_11
| ~ spl29_13
| spl29_34 ),
inference(sat_conversion,[],[f10766]) ).
cnf(s37,plain,
( spl29_18
| ~ spl29_37
| ~ spl29_38 ),
inference(sat_conversion,[],[f10916]) ).
cnf(s38,plain,
( ~ spl29_4
| ~ spl29_13
| spl29_37 ),
inference(sat_conversion,[],[f10965]) ).
cnf(s55,plain,
( ~ spl29_20
| ~ spl29_54
| spl29_55 ),
inference(sat_conversion,[],[f11512]) ).
cnf(s56,plain,
( ~ spl29_4
| ~ spl29_11
| spl29_54 ),
inference(sat_conversion,[],[f11561]) ).
cnf(s126,plain,
( ~ spl29_13
| spl29_120 ),
inference(sat_conversion,[],[f13246]) ).
cnf(s259,plain,
( ~ spl29_55
| spl29_236 ),
inference(sat_conversion,[],[f18225]) ).
cnf(s328,plain,
( ~ spl29_3
| ~ spl29_236
| spl29_300 ),
inference(sat_conversion,[],[f20562]) ).
cnf(s329,plain,
( ~ spl29_2
| ~ spl29_300
| spl29_301 ),
inference(sat_conversion,[],[f20585]) ).
cnf(s330,plain,
( ~ spl29_12
| ~ spl29_301
| spl29_302 ),
inference(sat_conversion,[],[f20636]) ).
cnf(s331,plain,
( ~ spl29_35
| spl29_38
| ~ spl29_302
| spl29_303 ),
inference(sat_conversion,[],[f20700]) ).
cnf(s333,plain,
( ~ spl29_7
| ~ spl29_120
| ~ spl29_303 ),
inference(sat_conversion,[],[f20725]) ).
cnf(s334,plain,
~ spl29_5,
inference(rat,[],[s5,s1]) ).
cnf(s335,plain,
spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s336,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s342,plain,
~ spl29_6,
inference(rat,[],[s6,s334]) ).
cnf(s347,plain,
spl29_4,
inference(rat,[],[s4,s335,s336]) ).
cnf(s350,plain,
spl29_12,
inference(rat,[],[s12,s342]) ).
cnf(s351,plain,
~ spl29_8,
inference(rat,[],[s8,s342]) ).
cnf(s352,plain,
spl29_7,
inference(rat,[],[s7,s342]) ).
cnf(s383,plain,
~ spl29_9,
inference(rat,[],[s9,s351]) ).
cnf(s384,plain,
spl29_11,
inference(rat,[],[s11,s342,s352]) ).
cnf(s392,plain,
~ spl29_16,
inference(rat,[],[s16,s383]) ).
cnf(s394,plain,
spl29_10,
inference(rat,[],[s10,s383]) ).
cnf(s419,plain,
spl29_54,
inference(rat,[],[s56,s347,s384]) ).
cnf(s425,plain,
spl29_26,
inference(rat,[],[s26,s392]) ).
cnf(s426,plain,
spl29_20,
inference(rat,[],[s20,s392]) ).
cnf(s427,plain,
~ spl29_18,
inference(rat,[],[s18,s392]) ).
cnf(s430,plain,
spl29_13,
inference(rat,[],[s13,s383,s394]) ).
cnf(s462,plain,
spl29_55,
inference(rat,[],[s55,s419,s426]) ).
cnf(s489,plain,
spl29_120,
inference(rat,[],[s126,s430]) ).
cnf(s494,plain,
spl29_37,
inference(rat,[],[s38,s347,s430]) ).
cnf(s495,plain,
spl29_34,
inference(rat,[],[s35,s384,s430]) ).
cnf(s501,plain,
spl29_236,
inference(rat,[],[s259,s462]) ).
cnf(s528,plain,
~ spl29_303,
inference(rat,[],[s333,s352,s489]) ).
cnf(s529,plain,
~ spl29_38,
inference(rat,[],[s37,s427,s494]) ).
cnf(s530,plain,
spl29_35,
inference(rat,[],[s34,s425,s495]) ).
cnf(s534,plain,
spl29_300,
inference(rat,[],[s328,s335,s501]) ).
cnf(s546,plain,
~ spl29_302,
inference(rat,[],[s331,s528,s529,s530]) ).
cnf(s552,plain,
spl29_301,
inference(rat,[],[s329,s336,s534]) ).
cnf(s564,plain,
$false,
inference(rat,[],[s330,s350,s546,s552]) ).
fof(f20726,plain,
$false,
inference(avatar_sat_refutation,[],[s564]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM792+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.36 % Computer : n006.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 21:25:26 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.50/2.53 % (3330839)Detected formulas, will run a generic FOF schedule.
% 11.50/2.53 % (3330850)dis-21_1_sil=8000:lcm=predicate:random_seed=2467168508: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.50/2.53 % (3330844)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=2321556337:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.50/2.53 % (3330847)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3952632675:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.50/2.53 % (3330849)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2253157380:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.50/2.53 % (3330848)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2106987027:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.50/2.53 % (3330846)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=3686067088:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.50/2.53 % (3330845)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=415004065:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.50/2.53 % (3330850)Instruction limit reached!
% 11.50/2.53 % (3330850)------------------------------
% 11.50/2.53 % (3330850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.53 % (3330850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.53 % (3330850)CaDiCaL version: 2.1.3
% 11.50/2.53 % (3330850)Termination reason: Instruction limit
% 11.50/2.53 % (3330850)Termination phase: Saturation
% 11.50/2.53 % (3330850)Time elapsed: 0.031 s
% 11.50/2.53 % (3330850)Peak memory usage: 90 MB
% 11.50/2.53 % (3330850)Instructions burned: 130 (million)
% 11.50/2.53 % (3330847)Refutation not found, incomplete strategy
% 11.50/2.53 % (3330847)------------------------------
% 11.50/2.53 % (3330847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.53 % (3330847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.53 % (3330847)CaDiCaL version: 2.1.3
% 11.50/2.53 % (3330847)Termination reason: Refutation not found, incomplete strategy
% 11.50/2.53 % (3330847)Time elapsed: 0.005 s
% 11.50/2.53 % (3330847)Peak memory usage: 89 MB
% 11.50/2.53 % (3330847)Instructions burned: 6 (million)
% 11.50/2.53 % (3330848)Refutation not found, incomplete strategy
% 11.50/2.53 % (3330848)------------------------------
% 11.50/2.53 % (3330848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.53 % (3330848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.53 % (3330848)CaDiCaL version: 2.1.3
% 11.50/2.53 % (3330848)Termination reason: Refutation not found, incomplete strategy
% 11.50/2.53 % (3330848)Time elapsed: 0.006 s
% 11.50/2.53 % (3330848)Peak memory usage: 89 MB
% 11.50/2.53 % (3330848)Instructions burned: 8 (million)
% 11.50/2.53 % (3330849)Instruction limit reached!
% 11.50/2.53 % (3330849)------------------------------
% 11.50/2.53 % (3330849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.53 % (3330849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.53 % (3330849)CaDiCaL version: 2.1.3
% 11.50/2.53 % (3330849)Termination reason: Instruction limit
% 11.50/2.53 % (3330849)Termination phase: Saturation
% 11.50/2.53 % (3330849)Time elapsed: 0.062 s
% 11.50/2.53 % (3330849)Peak memory usage: 90 MB
% 11.50/2.53 % (3330849)Instructions burned: 139 (million)
% 11.50/2.53 % (3330858)lrs+10_1_sil=8000:sp=occurrence:random_seed=2791537708:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.50/2.53 % (3330858)Refutation not found, incomplete strategy
% 11.50/2.53 % (3330858)------------------------------
% 11.50/2.53 % (3330858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.50/2.53 % (3330858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.50/2.53 % (3330858)CaDiCaL version: 2.1.3
% 11.50/2.53 % (3330858)Termination reason: Refutation not found, incomplete strategy
% 11.50/2.53 % (3330858)Time elapsed: 0.003 s
% 11.50/2.53 % (3330858)Peak memory usage: 89 MB
% 11.50/2.53 % (3330858)Instructions burned: 6 (million)
% 11.50/2.53 % (3330859)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2772297952:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.50/3.68 % (3330859)Refutation not found, incomplete strategy
% 19.50/3.68 % (3330859)------------------------------
% 19.50/3.68 % (3330859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.68 % (3330859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.68 % (3330859)CaDiCaL version: 2.1.3
% 19.50/3.68 % (3330859)Termination reason: Refutation not found, incomplete strategy
% 19.50/3.68 % (3330859)Time elapsed: 0.010 s
% 19.50/3.68 % (3330859)Peak memory usage: 89 MB
% 19.50/3.68 % (3330859)Instructions burned: 21 (million)
% 19.50/3.68 % (3330858)------------------------------
% 19.50/3.68 % (3330858)------------------------------
% 19.50/3.68 % (3330847)------------------------------
% 19.50/3.68 % (3330847)------------------------------
% 19.50/3.68 % (3330848)------------------------------
% 19.50/3.68 % (3330848)------------------------------
% 19.50/3.68 % (3330863)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=1959121953:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.50/3.68 % (3330862)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1156733664:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 19.50/3.68 % (3330862)Refutation not found, incomplete strategy
% 19.50/3.68 % (3330862)------------------------------
% 19.50/3.68 % (3330862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.68 % (3330862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.68 % (3330862)CaDiCaL version: 2.1.3
% 19.50/3.68 % (3330862)Termination reason: Refutation not found, incomplete strategy
% 19.50/3.68 % (3330862)Time elapsed: 0.007 s
% 19.50/3.68 % (3330862)Peak memory usage: 90 MB
% 19.50/3.68 % (3330862)Instructions burned: 8 (million)
% 19.50/3.68 % (3330864)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=268274990:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.50/3.68 % (3330864)Refutation not found, incomplete strategy
% 19.50/3.68 % (3330864)------------------------------
% 19.50/3.68 % (3330864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.68 % (3330864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.68 % (3330864)CaDiCaL version: 2.1.3
% 19.50/3.68 % (3330864)Termination reason: Refutation not found, incomplete strategy
% 19.50/3.68 % (3330864)Time elapsed: 0.009 s
% 19.50/3.68 % (3330864)Peak memory usage: 89 MB
% 19.50/3.68 % (3330864)Instructions burned: 13 (million)
% 19.50/3.68 % (3330863)Instruction limit reached!
% 19.50/3.68 % (3330863)------------------------------
% 19.50/3.68 % (3330863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.68 % (3330863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.68 % (3330863)CaDiCaL version: 2.1.3
% 19.50/3.68 % (3330863)Termination reason: Instruction limit
% 19.50/3.68 % (3330863)Termination phase: Saturation
% 19.50/3.68 % (3330863)Time elapsed: 0.070 s
% 19.50/3.68 % (3330863)Peak memory usage: 96 MB
% 19.50/3.68 % (3330863)Instructions burned: 250 (million)
% 19.50/3.68 % (3330859)------------------------------
% 19.50/3.68 % (3330859)------------------------------
% 19.50/3.68 % (3330868)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1276606991:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.50/3.68 % (3330869)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3565668923:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 19.50/3.68 % (3330862)------------------------------
% 19.50/3.68 % (3330862)------------------------------
% 19.50/3.68 % (3330869)Instruction limit reached!
% 19.50/3.68 % (3330869)------------------------------
% 19.50/3.68 % (3330869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.68 % (3330869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.68 % (3330869)CaDiCaL version: 2.1.3
% 19.50/3.68 % (3330869)Termination reason: Instruction limit
% 19.50/3.68 % (3330869)Termination phase: Saturation
% 19.50/3.68 % (3330869)Time elapsed: 0.054 s
% 19.50/3.68 % (3330869)Peak memory usage: 90 MB
% 19.50/3.68 % (3330869)Instructions burned: 115 (million)
% 19.50/3.68 % (3330864)------------------------------
% 19.50/3.68 % (3330864)------------------------------
% 19.50/3.68 % (3330873)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=809834961:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 32.84/5.55 % (3330872)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4090307658:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 32.84/5.55 % (3330874)lrs+10_1_sil=8000:sp=occurrence:random_seed=4235274041:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 32.84/5.55 % (3330872)Instruction limit reached!
% 32.84/5.55 % (3330872)------------------------------
% 32.84/5.55 % (3330872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330872)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330872)Termination reason: Instruction limit
% 32.84/5.55 % (3330872)Termination phase: Property scanning
% 32.84/5.55 % (3330872)Time elapsed: 0.056 s
% 32.84/5.55 % (3330872)Peak memory usage: 89 MB
% 32.84/5.55 % (3330872)Instructions burned: 129 (million)
% 32.84/5.55 % (3330873)Instruction limit reached!
% 32.84/5.55 % (3330873)------------------------------
% 32.84/5.55 % (3330873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330873)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330873)Termination reason: Instruction limit
% 32.84/5.55 % (3330873)Termination phase: Saturation
% 32.84/5.55 % (3330873)Time elapsed: 0.057 s
% 32.84/5.55 % (3330873)Peak memory usage: 90 MB
% 32.84/5.55 % (3330873)Instructions burned: 115 (million)
% 32.84/5.55 % (3330878)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=355127927:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 32.84/5.55 % (3330879)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=272302101:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 32.84/5.55 % (3330878)Refutation not found, incomplete strategy
% 32.84/5.55 % (3330878)------------------------------
% 32.84/5.55 % (3330878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330878)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330878)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.55 % (3330878)Time elapsed: 0.094 s
% 32.84/5.55 % (3330878)Peak memory usage: 93 MB
% 32.84/5.55 % (3330878)Instructions burned: 197 (million)
% 32.84/5.55 % (3330878)------------------------------
% 32.84/5.55 % (3330878)------------------------------
% 32.84/5.55 % (3330874)Instruction limit reached!
% 32.84/5.55 % (3330874)------------------------------
% 32.84/5.55 % (3330874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330874)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330874)Termination reason: Instruction limit
% 32.84/5.55 % (3330874)Termination phase: Saturation
% 32.84/5.55 % (3330874)Time elapsed: 0.544 s
% 32.84/5.55 % (3330874)Peak memory usage: 101 MB
% 32.84/5.55 % (3330874)Instructions burned: 908 (million)
% 32.84/5.55 % (3330882)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3696850548:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 32.84/5.55 % (3330883)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3721483952:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 32.84/5.55 % (3330883)Refutation not found, incomplete strategy
% 32.84/5.55 % (3330883)------------------------------
% 32.84/5.55 % (3330883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330883)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330883)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.55 % (3330883)Time elapsed: 0.022 s
% 32.84/5.55 % (3330883)Peak memory usage: 90 MB
% 32.84/5.55 % (3330883)Instructions burned: 42 (million)
% 32.84/5.55 % (3330882)Instruction limit reached!
% 32.84/5.55 % (3330882)------------------------------
% 32.84/5.55 % (3330882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330882)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330882)Termination reason: Instruction limit
% 32.84/5.55 % (3330882)Termination phase: Saturation
% 32.84/5.55 % (3330882)Time elapsed: 0.062 s
% 32.84/5.55 % (3330882)Peak memory usage: 91 MB
% 32.84/5.55 % (3330882)Instructions burned: 136 (million)
% 32.84/5.55 % (3330886)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=187751997:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 32.84/5.55 % (3330883)------------------------------
% 32.84/5.55 % (3330883)------------------------------
% 32.84/5.55 % (3330889)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=3485084593:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 32.84/5.55 % (3330889)Refutation not found, incomplete strategy
% 32.84/5.55 % (3330889)------------------------------
% 32.84/5.55 % (3330889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330889)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330889)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.55 % (3330889)Time elapsed: 0.015 s
% 32.84/5.55 % (3330889)Peak memory usage: 90 MB
% 32.84/5.55 % (3330889)Instructions burned: 30 (million)
% 32.84/5.55 % (3330868)Instruction limit reached!
% 32.84/5.55 % (3330868)------------------------------
% 32.84/5.55 % (3330868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330868)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330868)Termination reason: Instruction limit
% 32.84/5.55 % (3330868)Termination phase: Saturation
% 32.84/5.55 % (3330868)Time elapsed: 1.367 s
% 32.84/5.55 % (3330868)Peak memory usage: 163 MB
% 32.84/5.55 % (3330868)Instructions burned: 2350 (million)
% 32.84/5.55 % (3330891)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=822244196:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 32.84/5.55 % (3330889)------------------------------
% 32.84/5.55 % (3330889)------------------------------
% 32.84/5.55 % (3330891)Instruction limit reached!
% 32.84/5.55 % (3330891)------------------------------
% 32.84/5.55 % (3330891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330891)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330891)Termination reason: Instruction limit
% 32.84/5.55 % (3330891)Termination phase: Twee Goal Transformation
% 32.84/5.55 % (3330891)Time elapsed: 0.062 s
% 32.84/5.55 % (3330891)Peak memory usage: 91 MB
% 32.84/5.55 % (3330891)Instructions burned: 135 (million)
% 32.84/5.55 % (3330893)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=549493788:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 32.84/5.55 % (3330893)Refutation not found, incomplete strategy
% 32.84/5.55 % (3330893)------------------------------
% 32.84/5.55 % (3330893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330893)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330893)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.55 % (3330893)Time elapsed: 0.005 s
% 32.84/5.55 % (3330893)Peak memory usage: 89 MB
% 32.84/5.55 % (3330893)Instructions burned: 6 (million)
% 32.84/5.55 % (3330894)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1052134681:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 32.84/5.55 % (3330894)Refutation not found, incomplete strategy
% 32.84/5.55 % (3330894)------------------------------
% 32.84/5.55 % (3330894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330894)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330894)Termination reason: Refutation not found, incomplete strategy
% 32.84/5.55 % (3330894)Time elapsed: 0.006 s
% 32.84/5.55 % (3330894)Peak memory usage: 90 MB
% 32.84/5.55 % (3330894)Instructions burned: 8 (million)
% 32.84/5.55 % (3330893)------------------------------
% 32.84/5.55 % (3330893)------------------------------
% 32.84/5.55 % (3330894)------------------------------
% 32.84/5.55 % (3330894)------------------------------
% 32.84/5.55 % (3330897)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=1322086903:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 32.84/5.55 % (3330898)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=4166123180:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 32.84/5.55 % (3330898)Instruction limit reached!
% 32.84/5.55 % (3330898)------------------------------
% 32.84/5.55 % (3330898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330898)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330898)Termination reason: Instruction limit
% 32.84/5.55 % (3330898)Termination phase: Saturation
% 32.84/5.55 % (3330898)Time elapsed: 0.066 s
% 32.84/5.55 % (3330898)Peak memory usage: 91 MB
% 32.84/5.55 % (3330898)Instructions burned: 150 (million)
% 32.84/5.55 % (3330901)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2396267489:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 32.84/5.55 % (3330846)First to succeed.
% 32.84/5.55 % (3330846)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3330839"
% 32.84/5.55 % (3330879)Instruction limit reached!
% 32.84/5.55 % (3330879)------------------------------
% 32.84/5.55 % (3330879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.84/5.55 % (3330879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.84/5.55 % (3330879)CaDiCaL version: 2.1.3
% 32.84/5.55 % (3330879)Termination reason: Instruction limit
% 32.84/5.55 % (3330879)Termination phase: Saturation
% 32.84/5.55 % (3330879)Time elapsed: 3.286 s
% 32.84/5.55 % (3330879)Peak memory usage: 162 MB
% 32.84/5.55 % (3330879)Instructions burned: 5202 (million)
% 32.84/5.55 % (3330903)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3845707554:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 32.84/5.55 % (3330846)Refutation found. Thanks to Tanya!
% 32.84/5.55 % SZS status Theorem for theBenchmark
% 32.84/5.55 % SZS output start Proof for theBenchmark
% See solution above
% 33.59/5.76 % (3330846)------------------------------
% 33.59/5.76 % (3330846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.59/5.76 % (3330846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.59/5.76 % (3330846)CaDiCaL version: 2.1.3
% 33.59/5.76 % (3330846)Termination reason: Refutation
% 33.59/5.76 % (3330846)Time elapsed: 4.227 s
% 33.59/5.76 % (3330846)Peak memory usage: 194 MB
% 33.59/5.76 % (3330846)Instructions burned: 7169 (million)
% 33.59/5.76 % (3330846)------------------------------
% 33.59/5.76 % (3330846)------------------------------
% 33.59/5.76 % (3330839)Success in time 4.711 s
% 33.59/5.76 % Vampire exiting
%------------------------------------------------------------------------------