%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM721+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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:16:40 PM UTC 2026
% Result : Theorem 17.22s 3.73s
% Output : Refutation 20.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 47
% Syntax : Number of formulae : 269 ( 43 unt; 30 def)
% Number of atoms : 653 ( 2 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 664 ( 280 ~; 293 |; 34 &)
% ( 50 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 31 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 12 con; 0-2 aty)
% Number of variables : 176 ( 0 sgn 174 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f29,axiom,
! [X0] : scratc1124775109d_n_ts(X0) = aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__n__ts) ).
fof(f42,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X1),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__iii) ).
fof(f43,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__29__ii) ).
fof(f161,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc161856553_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f163,axiom,
pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_by)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz34) ).
fof(f255,axiom,
pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_lc)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz12) ).
fof(f389,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_lc,X0))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__42) ).
fof(f468,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__121) ).
fof(f469,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__122) ).
fof(f507,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__160) ).
fof(f586,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__239) ).
fof(f587,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__240) ).
fof(f673,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__326) ).
fof(f674,axiom,
! [X0,X1,X2] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__327) ).
fof(f688,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__341) ).
fof(f704,axiom,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__357) ).
fof(f736,conjecture,
pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f737,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(negated_conjecture,[status(cth)],[f736]) ).
fof(f738,plain,
~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(flattening,[],[f737]) ).
fof(f755,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc161856553_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f161]) ).
fof(f756,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc161856553_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f755]) ).
fof(f832,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f507]) ).
fof(f895,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ) ),
inference(ennf_transformation,[],[f688]) ).
fof(f896,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ) ),
inference(flattening,[],[f895]) ).
fof(f927,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) ),
inference(ennf_transformation,[],[f704]) ).
fof(f928,plain,
! [X0,X1,X2,X3] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
<=> ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) ),
inference(flattening,[],[f927]) ).
fof(f956,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X1),X0))) )
& ( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f957,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f1020,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc161856553_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc161856553_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f756]) ).
fof(f1021,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc161856553_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc161856553_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1)) ) ),
inference(rectify,[],[f1020]) ).
fof(f1022,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1)))
& scratc161856553_is_of(sK12(X0,X1),X0)
& gg_TPTP_ind(sK12(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc161856553_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f1021]) ).
fof(f1083,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_lc,X0))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,X0))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_lc,X0)) ) ),
inference(nnf_transformation,[],[f389]) ).
fof(f1162,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0)) ) ),
inference(nnf_transformation,[],[f468]) ).
fof(f1163,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0)) ) ),
inference(nnf_transformation,[],[f469]) ).
fof(f1217,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1)) ) ),
inference(nnf_transformation,[],[f832]) ).
fof(f1218,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1)) ) ),
inference(flattening,[],[f1217]) ).
fof(f1302,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1)) ) ),
inference(nnf_transformation,[],[f586]) ).
fof(f1303,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1)) ) ),
inference(nnf_transformation,[],[f587]) ).
fof(f1428,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f673]) ).
fof(f1429,plain,
! [X0,X1,X2] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) )
& ( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2)) ) ),
inference(nnf_transformation,[],[f674]) ).
fof(f1446,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f896]) ).
fof(f1447,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1446]) ).
fof(f1478,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(nnf_transformation,[],[f928]) ).
fof(f1479,plain,
! [X0,X1,X2,X3] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
& pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ) )
& ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3)) ) ),
inference(flattening,[],[f1478]) ).
fof(f1528,plain,
! [X0] : scratc1124775109d_n_ts(X0) = aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X0)),
inference(cnf_transformation,[],[f29]) ).
fof(f1550,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X1),X0)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f956]) ).
fof(f1551,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X1),X0))) ),
inference(cnf_transformation,[],[f956]) ).
fof(f1552,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1)) ),
inference(cnf_transformation,[],[f957]) ).
fof(f1553,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(X0),X1))) ),
inference(cnf_transformation,[],[f957]) ).
fof(f1738,plain,
! [X3,X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc161856553_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1022]) ).
fof(f1739,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| gg_TPTP_ind(sK12(X0,X1)) ),
inference(cnf_transformation,[],[f1022]) ).
fof(f1740,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| scratc161856553_is_of(sK12(X0,X1),X0) ),
inference(cnf_transformation,[],[f1022]) ).
fof(f1741,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(X0),X1))
| ~ pp(aa_TPTP_ind_bool(X1,sK12(X0,X1))) ),
inference(cnf_transformation,[],[f1022]) ).
fof(f1744,plain,
pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_by)),
inference(cnf_transformation,[],[f163]) ).
fof(f1836,plain,
pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_lc)),
inference(cnf_transformation,[],[f255]) ).
fof(f2041,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_lc,X0)) ),
inference(cnf_transformation,[],[f1083]) ).
fof(f2199,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_by,X0)) ),
inference(cnf_transformation,[],[f1162]) ).
fof(f2202,plain,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ad,X0))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,X0))) ),
inference(cnf_transformation,[],[f1163]) ).
fof(f2291,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X1),X0))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,X0),X1)) ),
inference(cnf_transformation,[],[f1218]) ).
fof(f2455,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,X0),X1)) ),
inference(cnf_transformation,[],[f1302]) ).
fof(f2458,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,X0),X1))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1))) ),
inference(cnf_transformation,[],[f1303]) ).
fof(f2674,plain,
! [X2,X0,X1] :
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(X0),X1),X2)) ),
inference(cnf_transformation,[],[f1428]) ).
fof(f2677,plain,
! [X2,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(X0),X1),X2))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2))) ),
inference(cnf_transformation,[],[f1429]) ).
fof(f2710,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3)) ),
inference(cnf_transformation,[],[f1447]) ).
fof(f2775,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X0),X1)) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f2776,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,X2),X3)) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f2777,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X0),X2)),aa_TPTP_ind_TPTP_ind(scratc1124775109d_n_ts(X1),X3))) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f2830,plain,
~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad)),
inference(cnf_transformation,[],[f738]) ).
fof(f3060,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X1)),X3)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(X0),X1),X2),X3)) ),
inference(definition_unfolding,[],[f2710,f1528,f1528]) ).
fof(f3091,plain,
! [X2,X3,X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(X0),X1),X2),X3))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X0)),X2)),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,X1)),X3))) ),
inference(definition_unfolding,[],[f2777,f1528,f1528]) ).
fof(f3126,definition,
( spl29_1
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad)) ),
introduced(definition,[new_symbols(definition,[spl29_1])],[avatar_definition]) ).
fof(f3128,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_ad))
| spl29_1 ),
inference(avatar_component_clause,[],[f3126]) ).
fof(f3129,plain,
~ spl29_1,
inference(avatar_split_clause,[],[f2830,f3126]) ).
fof(f3130,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| spl29_1 ),
inference(resolution,[],[f3128,f1739]) ).
fof(f3131,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| spl29_1 ),
inference(resolution,[],[f3128,f1740]) ).
fof(f3132,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_1 ),
inference(resolution,[],[f3128,f1741]) ).
fof(f3145,definition,
( spl29_2
<=> scratc161856553_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_2])],[avatar_definition]) ).
fof(f3147,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aTP_Lamm_ad),aTP_Lamm_a)
| ~ spl29_2 ),
inference(avatar_component_clause,[],[f3145]) ).
fof(f3148,plain,
( spl29_2
| spl29_1 ),
inference(avatar_split_clause,[],[f3131,f3126,f3145]) ).
fof(f3150,definition,
( spl29_3
<=> pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_3])],[avatar_definition]) ).
fof(f3152,plain,
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ad,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_3 ),
inference(avatar_component_clause,[],[f3150]) ).
fof(f3153,plain,
( ~ spl29_3
| spl29_1 ),
inference(avatar_split_clause,[],[f3132,f3126,f3150]) ).
fof(f3154,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_3 ),
inference(resolution,[],[f3152,f2202]) ).
fof(f3192,definition,
( spl29_4
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad)) ),
introduced(definition,[new_symbols(definition,[spl29_4])],[avatar_definition]) ).
fof(f3194,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ spl29_4 ),
inference(avatar_component_clause,[],[f3192]) ).
fof(f3195,plain,
( spl29_4
| spl29_1 ),
inference(avatar_split_clause,[],[f3130,f3126,f3192]) ).
fof(f3197,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aTP_Lamm_ad))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2 ),
inference(resolution,[],[f3147,f1738]) ).
fof(f3198,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_2
| ~ spl29_4 ),
inference(forward_subsumption_resolution,[],[f3197,f3194]) ).
fof(f3200,definition,
( spl29_5
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_5])],[avatar_definition]) ).
fof(f3201,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_5 ),
inference(avatar_component_clause,[],[f3200]) ).
fof(f3202,plain,
( spl29_5
| ~ spl29_2
| ~ spl29_4 ),
inference(avatar_split_clause,[],[f3198,f3192,f3145,f3200]) ).
fof(f3788,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_lc))
| pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_5 ),
inference(resolution,[],[f3201,f2041]) ).
fof(f3864,plain,
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_5 ),
inference(forward_subsumption_resolution,[],[f3788,f1836]) ).
fof(f4025,definition,
( spl29_6
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_6])],[avatar_definition]) ).
fof(f4027,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_6 ),
inference(avatar_component_clause,[],[f4025]) ).
fof(f4028,plain,
( ~ spl29_6
| spl29_3 ),
inference(avatar_split_clause,[],[f3154,f3150,f4025]) ).
fof(f4030,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_6 ),
inference(resolution,[],[f4027,f1739]) ).
fof(f4031,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
| spl29_6 ),
inference(resolution,[],[f4027,f1740]) ).
fof(f4032,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_6 ),
inference(resolution,[],[f4027,f1741]) ).
fof(f4045,definition,
( spl29_7
<=> scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_7])],[avatar_definition]) ).
fof(f4047,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))),aTP_Lamm_a)
| ~ spl29_7 ),
inference(avatar_component_clause,[],[f4045]) ).
fof(f4048,plain,
( spl29_7
| spl29_6 ),
inference(avatar_split_clause,[],[f4031,f4025,f4045]) ).
fof(f4050,definition,
( spl29_8
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
introduced(definition,[new_symbols(definition,[spl29_8])],[avatar_definition]) ).
fof(f4052,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_8 ),
inference(avatar_component_clause,[],[f4050]) ).
fof(f4053,plain,
( ~ spl29_8
| spl29_6 ),
inference(avatar_split_clause,[],[f4032,f4025,f4050]) ).
fof(f4054,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_8 ),
inference(resolution,[],[f4052,f2458]) ).
fof(f4100,definition,
( spl29_9
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
introduced(definition,[new_symbols(definition,[spl29_9])],[avatar_definition]) ).
fof(f4102,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_9 ),
inference(avatar_component_clause,[],[f4100]) ).
fof(f4103,plain,
( ~ spl29_9
| spl29_8 ),
inference(avatar_split_clause,[],[f4054,f4050,f4100]) ).
fof(f4105,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| spl29_9 ),
inference(resolution,[],[f4102,f1739]) ).
fof(f4106,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| spl29_9 ),
inference(resolution,[],[f4102,f1740]) ).
fof(f4107,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_9 ),
inference(resolution,[],[f4102,f1741]) ).
fof(f4120,definition,
( spl29_10
<=> scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_10])],[avatar_definition]) ).
fof(f4122,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| ~ spl29_10 ),
inference(avatar_component_clause,[],[f4120]) ).
fof(f4123,plain,
( spl29_10
| spl29_9 ),
inference(avatar_split_clause,[],[f4106,f4100,f4120]) ).
fof(f4128,definition,
( spl29_11
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_11])],[avatar_definition]) ).
fof(f4130,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_11 ),
inference(avatar_component_clause,[],[f4128]) ).
fof(f4131,plain,
( spl29_11
| spl29_6 ),
inference(avatar_split_clause,[],[f4030,f4025,f4128]) ).
fof(f4137,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7 ),
inference(resolution,[],[f4047,f1738]) ).
fof(f4138,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_7
| ~ spl29_11 ),
inference(forward_subsumption_resolution,[],[f4137,f4130]) ).
fof(f4140,definition,
( spl29_13
<=> ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl29_13])],[avatar_definition]) ).
fof(f4141,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(X0,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),X0)) )
| ~ spl29_13 ),
inference(avatar_component_clause,[],[f4140]) ).
fof(f4142,plain,
( spl29_13
| ~ spl29_7
| ~ spl29_11 ),
inference(avatar_split_clause,[],[f4138,f4128,f4045,f4140]) ).
fof(f4640,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aTP_Lamm_by))
| pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_13 ),
inference(resolution,[],[f4141,f2199]) ).
fof(f4893,plain,
( pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_13 ),
inference(forward_subsumption_resolution,[],[f4640,f1744]) ).
fof(f5149,definition,
( spl29_15
<=> gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))) ),
introduced(definition,[new_symbols(definition,[spl29_15])],[avatar_definition]) ).
fof(f5151,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_15 ),
inference(avatar_component_clause,[],[f5149]) ).
fof(f5152,plain,
( spl29_15
| spl29_9 ),
inference(avatar_split_clause,[],[f4105,f4100,f5149]) ).
fof(f6061,definition,
( spl29_16
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_16])],[avatar_definition]) ).
fof(f6063,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_16 ),
inference(avatar_component_clause,[],[f6061]) ).
fof(f6064,plain,
( ~ spl29_16
| spl29_9 ),
inference(avatar_split_clause,[],[f4107,f4100,f6061]) ).
fof(f6065,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_16 ),
inference(resolution,[],[f6063,f2677]) ).
fof(f6112,definition,
( spl29_17
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_17])],[avatar_definition]) ).
fof(f6114,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_17 ),
inference(avatar_component_clause,[],[f6112]) ).
fof(f6115,plain,
( ~ spl29_17
| spl29_16 ),
inference(avatar_split_clause,[],[f6065,f6061,f6112]) ).
fof(f6117,plain,
( gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_17 ),
inference(resolution,[],[f6114,f1739]) ).
fof(f6118,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
| spl29_17 ),
inference(resolution,[],[f6114,f1740]) ).
fof(f6119,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_17 ),
inference(resolution,[],[f6114,f1741]) ).
fof(f6139,definition,
( spl29_19
<=> scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl29_19])],[avatar_definition]) ).
fof(f6141,plain,
( scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aTP_Lamm_a)
| ~ spl29_19 ),
inference(avatar_component_clause,[],[f6139]) ).
fof(f6142,plain,
( spl29_19
| spl29_17 ),
inference(avatar_split_clause,[],[f6118,f6112,f6139]) ).
fof(f6147,definition,
( spl29_20
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_20])],[avatar_definition]) ).
fof(f6149,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_20 ),
inference(avatar_component_clause,[],[f6147]) ).
fof(f6150,plain,
( ~ spl29_20
| spl29_17 ),
inference(avatar_split_clause,[],[f6119,f6112,f6147]) ).
fof(f6157,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_20 ),
inference(resolution,[],[f6149,f2775]) ).
fof(f6158,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_20 ),
inference(resolution,[],[f6149,f2776]) ).
fof(f6159,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_20 ),
inference(resolution,[],[f6149,f3091]) ).
fof(f6199,definition,
( spl29_21
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_21])],[avatar_definition]) ).
fof(f6201,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| spl29_21 ),
inference(avatar_component_clause,[],[f6199]) ).
fof(f6202,plain,
( ~ spl29_21
| spl29_20 ),
inference(avatar_split_clause,[],[f6159,f6147,f6199]) ).
fof(f6206,plain,
( ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_21 ),
inference(resolution,[],[f6201,f1551]) ).
fof(f6403,definition,
( spl29_27
<=> pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_27])],[avatar_definition]) ).
fof(f6405,plain,
( ~ pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_27 ),
inference(avatar_component_clause,[],[f6403]) ).
fof(f6406,plain,
( ~ spl29_27
| spl29_21 ),
inference(avatar_split_clause,[],[f6206,f6199,f6403]) ).
fof(f6407,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_27 ),
inference(resolution,[],[f6405,f1552]) ).
fof(f6444,definition,
( spl29_29
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_29])],[avatar_definition]) ).
fof(f6446,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))),aa_TPTP_ind_TPTP_ind(aa_TPT1424761345TP_ind(scratc1235179703bnd_ap,aa_TPTP_ind_TPTP_ind(scratc850324382_times,sK12(aTP_Lamm_a,aTP_Lamm_ad))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| spl29_29 ),
inference(avatar_component_clause,[],[f6444]) ).
fof(f6447,plain,
( ~ spl29_29
| spl29_27 ),
inference(avatar_split_clause,[],[f6407,f6403,f6444]) ).
fof(f6450,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_29 ),
inference(resolution,[],[f6446,f3060]) ).
fof(f6747,definition,
( spl29_33
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_33])],[avatar_definition]) ).
fof(f6749,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_33 ),
inference(avatar_component_clause,[],[f6747]) ).
fof(f6750,plain,
( spl29_33
| spl29_20 ),
inference(avatar_split_clause,[],[f6158,f6147,f6747]) ).
fof(f6751,plain,
( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ spl29_33 ),
inference(resolution,[],[f6749,f1550]) ).
fof(f6815,definition,
( spl29_34
<=> pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))) ),
introduced(definition,[new_symbols(definition,[spl29_34])],[avatar_definition]) ).
fof(f6817,plain,
( pp(aa_fun171081125l_bool(scratc836808378n_some,aa_TPT43085870d_bool(scratc1295930928ffprop(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ spl29_34 ),
inference(avatar_component_clause,[],[f6815]) ).
fof(f6818,plain,
( spl29_34
| ~ spl29_33 ),
inference(avatar_split_clause,[],[f6751,f6747,f6815]) ).
fof(f6819,plain,
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| ~ spl29_34 ),
inference(resolution,[],[f6817,f1553]) ).
fof(f6833,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_29
| ~ spl29_34 ),
inference(backward_subsumption_resolution,[],[f6450,f6819]) ).
fof(f6835,definition,
( spl29_35
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))) ),
introduced(definition,[new_symbols(definition,[spl29_35])],[avatar_definition]) ).
fof(f6837,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))
| spl29_35 ),
inference(avatar_component_clause,[],[f6835]) ).
fof(f6839,definition,
( spl29_36
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_36])],[avatar_definition]) ).
fof(f6841,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc166993219_29_ii,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_36 ),
inference(avatar_component_clause,[],[f6839]) ).
fof(f6842,plain,
( ~ spl29_35
| ~ spl29_36
| spl29_29
| ~ spl29_34 ),
inference(avatar_split_clause,[],[f6833,f6815,f6444,f6839,f6835]) ).
fof(f6856,plain,
( ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| spl29_35 ),
inference(resolution,[],[f6837,f1738]) ).
fof(f6890,plain,
( ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) )
| ~ spl29_15
| spl29_35 ),
inference(forward_subsumption_resolution,[],[f6856,f5151]) ).
fof(f7007,definition,
( spl29_41
<=> ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl29_41])],[avatar_definition]) ).
fof(f7008,plain,
( ! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_bv(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))))
| ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),X0) )
| ~ spl29_41 ),
inference(avatar_component_clause,[],[f7007]) ).
fof(f7009,plain,
( spl29_41
| ~ spl29_15
| spl29_35 ),
inference(avatar_split_clause,[],[f6890,f6835,f5149,f7007]) ).
fof(f7016,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2060931009nd_iii,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_36 ),
inference(resolution,[],[f6841,f2291]) ).
fof(f7085,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_20
| spl29_36 ),
inference(forward_subsumption_resolution,[],[f7016,f6157]) ).
fof(f7087,definition,
( spl29_42
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))) ),
introduced(definition,[new_symbols(definition,[spl29_42])],[avatar_definition]) ).
fof(f7089,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))
| spl29_42 ),
inference(avatar_component_clause,[],[f7087]) ).
fof(f7090,plain,
( ~ spl29_42
| spl29_20
| spl29_36 ),
inference(avatar_split_clause,[],[f7085,f6839,f6147,f7087]) ).
fof(f7099,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_lb,sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_13
| spl29_42 ),
inference(resolution,[],[f7089,f4141]) ).
fof(f7138,plain,
( $false
| ~ spl29_5
| ~ spl29_13
| spl29_42 ),
inference(forward_subsumption_resolution,[],[f7099,f3864]) ).
fof(f7139,plain,
( ~ spl29_5
| ~ spl29_13
| spl29_42 ),
inference(avatar_contradiction_clause,[],[f7138]) ).
fof(f7249,plain,
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))),aTP_Lamm_a)
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_41 ),
inference(resolution,[],[f7008,f2674]) ).
fof(f7265,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| ~ spl29_10
| ~ spl29_41 ),
inference(forward_subsumption_resolution,[],[f7249,f4122]) ).
fof(f7267,definition,
( spl29_43
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))) ),
introduced(definition,[new_symbols(definition,[spl29_43])],[avatar_definition]) ).
fof(f7269,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))))))))
| spl29_43 ),
inference(avatar_component_clause,[],[f7267]) ).
fof(f7270,plain,
( ~ spl29_43
| ~ spl29_10
| ~ spl29_41 ),
inference(avatar_split_clause,[],[f7265,f7007,f4120,f7267]) ).
fof(f7281,plain,
( ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ gg_TPTP_ind(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))))
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| spl29_43 ),
inference(resolution,[],[f7269,f1738]) ).
fof(f7315,plain,
( ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| spl29_17
| spl29_43 ),
inference(forward_subsumption_resolution,[],[f7281,f6117]) ).
fof(f7618,definition,
( spl29_49
<=> ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ) ),
introduced(definition,[new_symbols(definition,[spl29_49])],[avatar_definition]) ).
fof(f7619,plain,
( ! [X0] :
( ~ scratc161856553_is_of(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aa_TPT60673477d_bool(aTP_Lamm_aa(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ab(sK12(aTP_Lamm_a,aTP_Lamm_ad)),sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))),X0)
| ~ pp(aa_fun171081125l_bool(scratc982322928all_of(X0),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) )
| ~ spl29_49 ),
inference(avatar_component_clause,[],[f7618]) ).
fof(f7620,plain,
( spl29_49
| spl29_17
| spl29_43 ),
inference(avatar_split_clause,[],[f7315,f7267,f6112,f7618]) ).
fof(f7910,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| ~ spl29_19
| ~ spl29_49 ),
inference(resolution,[],[f7619,f6141]) ).
fof(f7913,definition,
( spl29_53
<=> pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))) ),
introduced(definition,[new_symbols(definition,[spl29_53])],[avatar_definition]) ).
fof(f7915,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bw(sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))))
| spl29_53 ),
inference(avatar_component_clause,[],[f7913]) ).
fof(f7916,plain,
( ~ spl29_53
| ~ spl29_19
| ~ spl29_49 ),
inference(avatar_split_clause,[],[f7910,f7618,f6139,f7913]) ).
fof(f8533,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_53 ),
inference(resolution,[],[f7915,f2455]) ).
fof(f19219,definition,
( spl29_255
<=> pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad))) ),
introduced(definition,[new_symbols(definition,[spl29_255])],[avatar_definition]) ).
fof(f19221,plain,
( ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad)))),sK12(aTP_Lamm_a,aTP_Lamm_ad)))
| spl29_255 ),
inference(avatar_component_clause,[],[f19219]) ).
fof(f19222,plain,
( ~ spl29_255
| spl29_53 ),
inference(avatar_split_clause,[],[f8533,f7913,f19219]) ).
fof(f19843,plain,
( ~ pp(aa_fun171081125l_bool(scratc982322928all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_bx,sK12(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_ac,sK12(aTP_Lamm_a,aTP_Lamm_ad))))))
| ~ spl29_5
| spl29_255 ),
inference(resolution,[],[f19221,f3201]) ).
fof(f19882,plain,
( $false
| ~ spl29_5
| ~ spl29_13
| spl29_255 ),
inference(forward_subsumption_resolution,[],[f19843,f4893]) ).
fof(f19883,plain,
( ~ spl29_5
| ~ spl29_13
| spl29_255 ),
inference(avatar_contradiction_clause,[],[f19882]) ).
cnf(s1,plain,
~ spl29_1,
inference(sat_conversion,[],[f3129]) ).
cnf(s2,plain,
( spl29_1
| spl29_2 ),
inference(sat_conversion,[],[f3148]) ).
cnf(s3,plain,
( spl29_1
| ~ spl29_3 ),
inference(sat_conversion,[],[f3153]) ).
cnf(s4,plain,
( spl29_1
| spl29_4 ),
inference(sat_conversion,[],[f3195]) ).
cnf(s5,plain,
( ~ spl29_2
| ~ spl29_4
| spl29_5 ),
inference(sat_conversion,[],[f3202]) ).
cnf(s6,plain,
( spl29_3
| ~ spl29_6 ),
inference(sat_conversion,[],[f4028]) ).
cnf(s7,plain,
( spl29_6
| spl29_7 ),
inference(sat_conversion,[],[f4048]) ).
cnf(s8,plain,
( spl29_6
| ~ spl29_8 ),
inference(sat_conversion,[],[f4053]) ).
cnf(s9,plain,
( spl29_8
| ~ spl29_9 ),
inference(sat_conversion,[],[f4103]) ).
cnf(s10,plain,
( spl29_9
| spl29_10 ),
inference(sat_conversion,[],[f4123]) ).
cnf(s11,plain,
( spl29_6
| spl29_11 ),
inference(sat_conversion,[],[f4131]) ).
cnf(s13,plain,
( ~ spl29_7
| ~ spl29_11
| spl29_13 ),
inference(sat_conversion,[],[f4142]) ).
cnf(s15,plain,
( spl29_9
| spl29_15 ),
inference(sat_conversion,[],[f5152]) ).
cnf(s16,plain,
( spl29_9
| ~ spl29_16 ),
inference(sat_conversion,[],[f6064]) ).
cnf(s17,plain,
( spl29_16
| ~ spl29_17 ),
inference(sat_conversion,[],[f6115]) ).
cnf(s19,plain,
( spl29_17
| spl29_19 ),
inference(sat_conversion,[],[f6142]) ).
cnf(s20,plain,
( spl29_17
| ~ spl29_20 ),
inference(sat_conversion,[],[f6150]) ).
cnf(s21,plain,
( spl29_20
| ~ spl29_21 ),
inference(sat_conversion,[],[f6202]) ).
cnf(s25,plain,
( spl29_21
| ~ spl29_27 ),
inference(sat_conversion,[],[f6406]) ).
cnf(s27,plain,
( spl29_27
| ~ spl29_29 ),
inference(sat_conversion,[],[f6447]) ).
cnf(s31,plain,
( spl29_20
| spl29_33 ),
inference(sat_conversion,[],[f6750]) ).
cnf(s32,plain,
( ~ spl29_33
| spl29_34 ),
inference(sat_conversion,[],[f6818]) ).
cnf(s33,plain,
( spl29_29
| ~ spl29_34
| ~ spl29_35
| ~ spl29_36 ),
inference(sat_conversion,[],[f6842]) ).
cnf(s36,plain,
( ~ spl29_15
| spl29_35
| spl29_41 ),
inference(sat_conversion,[],[f7009]) ).
cnf(s38,plain,
( spl29_20
| spl29_36
| ~ spl29_42 ),
inference(sat_conversion,[],[f7090]) ).
cnf(s39,plain,
( ~ spl29_5
| ~ spl29_13
| spl29_42 ),
inference(sat_conversion,[],[f7139]) ).
cnf(s40,plain,
( ~ spl29_10
| ~ spl29_41
| ~ spl29_43 ),
inference(sat_conversion,[],[f7270]) ).
cnf(s46,plain,
( spl29_17
| spl29_43
| spl29_49 ),
inference(sat_conversion,[],[f7620]) ).
cnf(s49,plain,
( ~ spl29_19
| ~ spl29_49
| ~ spl29_53 ),
inference(sat_conversion,[],[f7916]) ).
cnf(s289,plain,
( spl29_53
| ~ spl29_255 ),
inference(sat_conversion,[],[f19222]) ).
cnf(s304,plain,
( ~ spl29_5
| ~ spl29_13
| spl29_255 ),
inference(sat_conversion,[],[f19883]) ).
cnf(s305,plain,
spl29_4,
inference(rat,[],[s4,s1]) ).
cnf(s306,plain,
~ spl29_3,
inference(rat,[],[s3,s1]) ).
cnf(s307,plain,
spl29_2,
inference(rat,[],[s2,s1]) ).
cnf(s312,plain,
~ spl29_6,
inference(rat,[],[s6,s306]) ).
cnf(s313,plain,
spl29_5,
inference(rat,[],[s5,s305,s307]) ).
cnf(s314,plain,
spl29_11,
inference(rat,[],[s11,s312]) ).
cnf(s315,plain,
~ spl29_8,
inference(rat,[],[s8,s312]) ).
cnf(s316,plain,
spl29_7,
inference(rat,[],[s7,s312]) ).
cnf(s321,plain,
~ spl29_9,
inference(rat,[],[s9,s315]) ).
cnf(s322,plain,
spl29_13,
inference(rat,[],[s13,s314,s316]) ).
cnf(s323,plain,
~ spl29_16,
inference(rat,[],[s16,s321]) ).
cnf(s324,plain,
spl29_15,
inference(rat,[],[s15,s321]) ).
cnf(s325,plain,
spl29_10,
inference(rat,[],[s10,s321]) ).
cnf(s326,plain,
spl29_255,
inference(rat,[],[s304,s313,s322]) ).
cnf(s338,plain,
spl29_42,
inference(rat,[],[s39,s313,s322]) ).
cnf(s340,plain,
~ spl29_17,
inference(rat,[],[s17,s323]) ).
cnf(s344,plain,
spl29_53,
inference(rat,[],[s289,s326]) ).
cnf(s348,plain,
~ spl29_20,
inference(rat,[],[s20,s340]) ).
cnf(s349,plain,
spl29_19,
inference(rat,[],[s19,s340]) ).
cnf(s357,plain,
spl29_36,
inference(rat,[],[s38,s338,s348]) ).
cnf(s358,plain,
spl29_33,
inference(rat,[],[s31,s348]) ).
cnf(s359,plain,
~ spl29_21,
inference(rat,[],[s21,s348]) ).
cnf(s361,plain,
~ spl29_49,
inference(rat,[],[s49,s344,s349]) ).
cnf(s373,plain,
spl29_34,
inference(rat,[],[s32,s358]) ).
cnf(s378,plain,
~ spl29_27,
inference(rat,[],[s25,s359]) ).
cnf(s382,plain,
spl29_43,
inference(rat,[],[s46,s340,s361]) ).
cnf(s392,plain,
~ spl29_29,
inference(rat,[],[s27,s378]) ).
cnf(s394,plain,
~ spl29_41,
inference(rat,[],[s40,s325,s382]) ).
cnf(s406,plain,
~ spl29_35,
inference(rat,[],[s33,s357,s373,s392]) ).
cnf(s408,plain,
$false,
inference(rat,[],[s36,s324,s394,s406]) ).
fof(f19884,plain,
$false,
inference(avatar_sat_refutation,[],[s408]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM721+4 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 21:07:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/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.18/2.58 % (2937279)Detected formulas, will run a generic FOF schedule.
% 11.18/2.58 % (2937286)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=3216357935:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.18/2.58 % (2937290)dis-21_1_sil=8000:lcm=predicate:random_seed=2145679681: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.18/2.58 % (2937284)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=4220466907:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.18/2.58 % (2937289)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2899746346:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.18/2.58 % (2937287)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1212114654:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.18/2.58 % (2937285)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=2637847668:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.18/2.58 % (2937288)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2528164377:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.18/2.58 % (2937287)Refutation not found, incomplete strategy
% 11.18/2.58 % (2937287)------------------------------
% 11.18/2.58 % (2937287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.58 % (2937287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.58 % (2937287)CaDiCaL version: 2.1.3
% 11.18/2.58 % (2937287)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.58 % (2937287)Time elapsed: 0.003 s
% 11.18/2.58 % (2937287)Peak memory usage: 88 MB
% 11.18/2.58 % (2937287)Instructions burned: 3 (million)
% 11.18/2.58 % (2937288)Refutation not found, incomplete strategy
% 11.18/2.58 % (2937288)------------------------------
% 11.18/2.58 % (2937288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.58 % (2937288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.58 % (2937288)CaDiCaL version: 2.1.3
% 11.18/2.58 % (2937288)Termination reason: Refutation not found, incomplete strategy
% 11.18/2.58 % (2937288)Time elapsed: 0.003 s
% 11.18/2.58 % (2937288)Peak memory usage: 88 MB
% 11.18/2.58 % (2937288)Instructions burned: 4 (million)
% 11.18/2.58 % (2937290)Instruction limit reached!
% 11.18/2.58 % (2937290)------------------------------
% 11.18/2.58 % (2937290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.58 % (2937290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.58 % (2937290)CaDiCaL version: 2.1.3
% 11.18/2.58 % (2937290)Termination reason: Instruction limit
% 11.18/2.58 % (2937290)Termination phase: Saturation
% 11.18/2.58 % (2937290)Time elapsed: 0.068 s
% 11.18/2.58 % (2937290)Peak memory usage: 90 MB
% 11.18/2.58 % (2937290)Instructions burned: 130 (million)
% 11.18/2.58 % (2937289)Instruction limit reached!
% 11.18/2.58 % (2937289)------------------------------
% 11.18/2.58 % (2937289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.58 % (2937289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.58 % (2937289)CaDiCaL version: 2.1.3
% 11.18/2.58 % (2937289)Termination reason: Instruction limit
% 11.18/2.58 % (2937289)Termination phase: Saturation
% 11.18/2.58 % (2937289)Time elapsed: 0.077 s
% 11.18/2.58 % (2937289)Peak memory usage: 90 MB
% 11.18/2.58 % (2937289)Instructions burned: 139 (million)
% 11.18/2.58 % (2937298)lrs+10_1_sil=8000:sp=occurrence:random_seed=1858944413:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.18/2.58 % (2937299)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2269310619:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.18/2.58 % (2937298)Refutation not found, incomplete strategy
% 11.18/2.58 % (2937298)------------------------------
% 11.18/2.58 % (2937298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.18/2.58 % (2937298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.18/2.58 % (2937298)CaDiCaL version: 2.1.3
% 11.18/2.58 % (2937298)Termination reason: Refutation not found, incomplete strategy
% 19.12/3.64 % (2937298)Time elapsed: 0.003 s
% 19.12/3.64 % (2937298)Peak memory usage: 88 MB
% 19.12/3.64 % (2937298)Instructions burned: 3 (million)
% 19.12/3.64 % (2937299)Refutation not found, incomplete strategy
% 19.12/3.64 % (2937299)------------------------------
% 19.12/3.64 % (2937299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.12/3.64 % (2937299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.12/3.64 % (2937299)CaDiCaL version: 2.1.3
% 19.12/3.64 % (2937299)Termination reason: Refutation not found, incomplete strategy
% 19.12/3.64 % (2937299)Time elapsed: 0.006 s
% 19.12/3.64 % (2937299)Peak memory usage: 88 MB
% 19.12/3.64 % (2937299)Instructions burned: 12 (million)
% 19.12/3.64 % (2937287)------------------------------
% 19.12/3.64 % (2937287)------------------------------
% 19.12/3.64 % (2937288)------------------------------
% 19.12/3.64 % (2937288)------------------------------
% 19.12/3.64 % (2937302)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1246743348:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 19.12/3.64 % (2937303)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=1040647511:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.12/3.64 % (2937302)Refutation not found, incomplete strategy
% 19.12/3.64 % (2937302)------------------------------
% 19.12/3.64 % (2937302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.12/3.64 % (2937302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.12/3.64 % (2937302)CaDiCaL version: 2.1.3
% 19.12/3.64 % (2937302)Termination reason: Refutation not found, incomplete strategy
% 19.12/3.64 % (2937302)Time elapsed: 0.005 s
% 19.12/3.64 % (2937302)Peak memory usage: 89 MB
% 19.12/3.64 % (2937302)Instructions burned: 6 (million)
% 19.12/3.64 % (2937299)------------------------------
% 19.12/3.64 % (2937299)------------------------------
% 19.12/3.64 % (2937298)------------------------------
% 19.12/3.64 % (2937298)------------------------------
% 19.12/3.64 % (2937303)Instruction limit reached!
% 19.12/3.64 % (2937303)------------------------------
% 19.12/3.64 % (2937303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.12/3.64 % (2937303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.12/3.64 % (2937303)CaDiCaL version: 2.1.3
% 19.12/3.64 % (2937303)Termination reason: Instruction limit
% 19.12/3.64 % (2937303)Termination phase: Saturation
% 19.12/3.64 % (2937303)Time elapsed: 0.135 s
% 19.12/3.64 % (2937303)Peak memory usage: 99 MB
% 19.12/3.64 % (2937303)Instructions burned: 250 (million)
% 19.12/3.64 % (2937307)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4038351396:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.12/3.64 % (2937306)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1909964208:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.12/3.64 % (2937306)Refutation not found, incomplete strategy
% 19.12/3.64 % (2937306)------------------------------
% 19.12/3.64 % (2937306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.12/3.64 % (2937306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.12/3.64 % (2937306)CaDiCaL version: 2.1.3
% 19.12/3.64 % (2937306)Termination reason: Refutation not found, incomplete strategy
% 19.12/3.64 % (2937306)Time elapsed: 0.006 s
% 19.12/3.64 % (2937306)Peak memory usage: 88 MB
% 19.12/3.64 % (2937306)Instructions burned: 7 (million)
% 19.12/3.64 % (2937302)------------------------------
% 19.12/3.64 % (2937302)------------------------------
% 19.12/3.64 % (2937308)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1602947730:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 19.12/3.64 % (2937308)Instruction limit reached!
% 19.12/3.64 % (2937308)------------------------------
% 19.12/3.64 % (2937308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.12/3.64 % (2937308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.12/3.64 % (2937308)CaDiCaL version: 2.1.3
% 19.12/3.64 % (2937308)Termination reason: Instruction limit
% 19.12/3.64 % (2937308)Termination phase: Saturation
% 19.12/3.64 % (2937308)Time elapsed: 0.056 s
% 19.12/3.64 % (2937308)Peak memory usage: 90 MB
% 19.12/3.64 % (2937308)Instructions burned: 115 (million)
% 19.12/3.64 % (2937311)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=944765152:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 17.22/3.73 % (2937306)------------------------------
% 17.22/3.73 % (2937306)------------------------------
% 17.22/3.73 % (2937311)Instruction limit reached!
% 17.22/3.73 % (2937311)------------------------------
% 17.22/3.73 % (2937311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937311)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937311)Termination reason: Instruction limit
% 17.22/3.73 % (2937311)Termination phase: Saturation
% 17.22/3.73 % (2937311)Time elapsed: 0.059 s
% 17.22/3.73 % (2937311)Peak memory usage: 90 MB
% 17.22/3.73 % (2937311)Instructions burned: 128 (million)
% 17.22/3.73 % (2937313)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=946256957:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 17.22/3.73 % (2937313)Instruction limit reached!
% 17.22/3.73 % (2937313)------------------------------
% 17.22/3.73 % (2937313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937313)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937313)Termination reason: Instruction limit
% 17.22/3.73 % (2937313)Termination phase: Saturation
% 17.22/3.73 % (2937313)Time elapsed: 0.061 s
% 17.22/3.73 % (2937313)Peak memory usage: 90 MB
% 17.22/3.73 % (2937313)Instructions burned: 115 (million)
% 17.22/3.73 % (2937316)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1863157586:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 17.22/3.73 % (2937315)lrs+10_1_sil=8000:sp=occurrence:random_seed=3867719769:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 17.22/3.73 % (2937315)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937315)------------------------------
% 17.22/3.73 % (2937315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937315)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937315)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937315)Time elapsed: 0.004 s
% 17.22/3.73 % (2937315)Peak memory usage: 88 MB
% 17.22/3.73 % (2937315)Instructions burned: 3 (million)
% 17.22/3.73 % (2937316)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937316)------------------------------
% 17.22/3.73 % (2937316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937316)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937316)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937316)Time elapsed: 0.054 s
% 17.22/3.73 % (2937316)Peak memory usage: 91 MB
% 17.22/3.73 % (2937316)Instructions burned: 106 (million)
% 17.22/3.73 % (2937318)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3485745550:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 17.22/3.73 % (2937315)------------------------------
% 17.22/3.73 % (2937315)------------------------------
% 17.22/3.73 % (2937316)------------------------------
% 17.22/3.73 % (2937316)------------------------------
% 17.22/3.73 % (2937322)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1015875931:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 17.22/3.73 % (2937323)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=472178125:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 17.22/3.73 % (2937323)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937323)------------------------------
% 17.22/3.73 % (2937323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937323)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937323)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937323)Time elapsed: 0.014 s
% 17.22/3.73 % (2937323)Peak memory usage: 89 MB
% 17.22/3.73 % (2937323)Instructions burned: 25 (million)
% 17.22/3.73 % (2937322)Instruction limit reached!
% 17.22/3.73 % (2937322)------------------------------
% 17.22/3.73 % (2937322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937322)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937322)Termination reason: Instruction limit
% 17.22/3.73 % (2937322)Termination phase: Saturation
% 17.22/3.73 % (2937322)Time elapsed: 0.071 s
% 17.22/3.73 % (2937322)Peak memory usage: 93 MB
% 17.22/3.73 % (2937322)Instructions burned: 134 (million)
% 17.22/3.73 % (2937326)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=983448615:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 17.22/3.73 % (2937323)------------------------------
% 17.22/3.73 % (2937323)------------------------------
% 17.22/3.73 % (2937328)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=3532091491:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 17.22/3.73 % (2937328)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937328)------------------------------
% 17.22/3.73 % (2937328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937328)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937328)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937328)Time elapsed: 0.008 s
% 17.22/3.73 % (2937328)Peak memory usage: 89 MB
% 17.22/3.73 % (2937328)Instructions burned: 15 (million)
% 17.22/3.73 % (2937307)Instruction limit reached!
% 17.22/3.73 % (2937307)------------------------------
% 17.22/3.73 % (2937307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937307)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937307)Termination reason: Instruction limit
% 17.22/3.73 % (2937307)Termination phase: Saturation
% 17.22/3.73 % (2937307)Time elapsed: 1.515 s
% 17.22/3.73 % (2937307)Peak memory usage: 149 MB
% 17.22/3.73 % (2937307)Instructions burned: 2350 (million)
% 17.22/3.73 % (2937328)------------------------------
% 17.22/3.73 % (2937328)------------------------------
% 17.22/3.73 % (2937330)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1038291978:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 17.22/3.73 % (2937331)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2701452963:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 17.22/3.73 % (2937331)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937331)------------------------------
% 17.22/3.73 % (2937331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937331)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937331)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937331)Time elapsed: 0.003 s
% 17.22/3.73 % (2937331)Peak memory usage: 88 MB
% 17.22/3.73 % (2937331)Instructions burned: 3 (million)
% 17.22/3.73 % (2937330)Instruction limit reached!
% 17.22/3.73 % (2937330)------------------------------
% 17.22/3.73 % (2937330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937330)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937330)Termination reason: Instruction limit
% 17.22/3.73 % (2937330)Termination phase: Saturation
% 17.22/3.73 % (2937330)Time elapsed: 0.062 s
% 17.22/3.73 % (2937330)Peak memory usage: 92 MB
% 17.22/3.73 % (2937330)Instructions burned: 134 (million)
% 17.22/3.73 % (2937286)First to succeed.
% 17.22/3.73 % (2937286)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2937279"
% 17.22/3.73 % (2937334)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4181816957:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 17.22/3.73 % (2937334)Refutation not found, incomplete strategy
% 17.22/3.73 % (2937334)------------------------------
% 17.22/3.73 % (2937334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.22/3.73 % (2937334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/3.73 % (2937334)CaDiCaL version: 2.1.3
% 17.22/3.73 % (2937334)Termination reason: Refutation not found, incomplete strategy
% 17.22/3.73 % (2937334)Time elapsed: 0.004 s
% 17.22/3.73 % (2937334)Peak memory usage: 89 MB
% 17.22/3.73 % (2937334)Instructions burned: 3 (million)
% 17.22/3.73 % (2937331)------------------------------
% 17.22/3.73 % (2937331)------------------------------
% 17.22/3.73 % (2937286)Refutation found. Thanks to Tanya!
% 17.22/3.73 % SZS status Theorem for theBenchmark
% 17.22/3.73 % SZS output start Proof for theBenchmark
% See solution above
% 20.74/3.94 % (2937286)------------------------------
% 20.74/3.94 % (2937286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.74/3.94 % (2937286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.74/3.94 % (2937286)CaDiCaL version: 2.1.3
% 20.74/3.94 % (2937286)Termination reason: Refutation
% 20.74/3.94 % (2937286)Time elapsed: 2.531 s
% 20.74/3.94 % (2937286)Peak memory usage: 193 MB
% 20.74/3.94 % (2937286)Instructions burned: 7696 (million)
% 20.74/3.94 % (2937286)------------------------------
% 20.74/3.94 % (2937286)------------------------------
% 20.74/3.94 % (2937279)Success in time 2.876 s
% 20.74/3.94 % Vampire exiting
%------------------------------------------------------------------------------