%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM783+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 : n003.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:58 PM UTC 2026
% Result : Theorem 144.00s 31.52s
% Output : Refutation 216.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 25
% Syntax : Number of formulae : 128 ( 26 unt; 9 def)
% Number of atoms : 342 ( 4 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 382 ( 168 ~; 173 |; 18 &)
% ( 21 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 11 con; 0-3 aty)
% Number of variables : 127 ( 0 sgn 125 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f174,axiom,
! [X0,X1,X2] :
( scratc1941720897_orec3(X0,X1,X2)
<=> pp(scratc876302756_d_and(scratc1898430207nd_or3(X0,X1,X2),scratc1814831172nd_ec3(X0,X1,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__orec3) ).
fof(f184,axiom,
! [X0,X1] :
( pp(scratc876302756_d_and(X0,X1))
<=> pp(scratc983767936_d_not(scratc822302649d_l_ec(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__and) ).
fof(f185,axiom,
! [X0,X1] :
( pp(scratc822302649d_l_ec(X0,X1))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),scratc983767936_d_not(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__l__ec) ).
fof(f188,axiom,
! [X0] :
( pp(scratc983767936_d_not(X0))
<=> pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),fFalse)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__d__not) ).
fof(f189,axiom,
scratc1848533243nd_imp = fimplies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__imp) ).
fof(f220,axiom,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
<=> ! [X2] :
( gg_TPTP_ind(X2)
=> ( scratc1888847154_is_of(X2,X0)
=> pp(aa_TPTP_ind_bool(X1,X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__all__of) ).
fof(f221,axiom,
! [X0,X1] :
( scratc1888847154_is_of(X0,X1)
<=> pp(aa_TPTP_ind_bool(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_def__is__of) ).
fof(f222,axiom,
pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_cc)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_satz81) ).
fof(f751,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
<=> pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__233) ).
fof(f752,axiom,
! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
<=> pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__234) ).
fof(f760,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
<=> scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__242) ).
fof(f763,axiom,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
<=> pp(scratc1898430207nd_or3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ATP_Olambda__245) ).
fof(f1248,axiom,
~ pp(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f1249,axiom,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
fof(f1251,axiom,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
fof(f1258,conjecture,
pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1259,negated_conjecture,
~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(negated_conjecture,[status(cth)],[f1258]) ).
fof(f1260,plain,
~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(flattening,[],[f1259]) ).
fof(f1335,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1888847154_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(ennf_transformation,[],[f220]) ).
fof(f1336,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
<=> ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1888847154_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) ) ),
inference(flattening,[],[f1335]) ).
fof(f1378,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ) ),
inference(nnf_transformation,[],[f752]) ).
fof(f1379,plain,
! [X0] :
( ( pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
| ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0))) )
& ( pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) ) ),
inference(nnf_transformation,[],[f751]) ).
fof(f1383,plain,
! [X0] :
( ( pp(scratc983767936_d_not(X0))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),fFalse)) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),fFalse))
| ~ pp(scratc983767936_d_not(X0)) ) ),
inference(nnf_transformation,[],[f188]) ).
fof(f1387,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1))
| ~ pp(scratc1898430207nd_or3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))) )
& ( pp(scratc1898430207nd_or3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1)))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ) ),
inference(nnf_transformation,[],[f763]) ).
fof(f1389,plain,
! [X0,X1,X2] :
( ( scratc1941720897_orec3(X0,X1,X2)
| ~ pp(scratc876302756_d_and(scratc1898430207nd_or3(X0,X1,X2),scratc1814831172nd_ec3(X0,X1,X2))) )
& ( pp(scratc876302756_d_and(scratc1898430207nd_or3(X0,X1,X2),scratc1814831172nd_ec3(X0,X1,X2)))
| ~ scratc1941720897_orec3(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f174]) ).
fof(f1392,plain,
! [X0,X1] :
( ( pp(scratc822302649d_l_ec(X0,X1))
| ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),scratc983767936_d_not(X1))) )
& ( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),scratc983767936_d_not(X1)))
| ~ pp(scratc822302649d_l_ec(X0,X1)) ) ),
inference(nnf_transformation,[],[f185]) ).
fof(f1393,plain,
! [X0,X1] :
( ( pp(scratc876302756_d_and(X0,X1))
| ~ pp(scratc983767936_d_not(scratc822302649d_l_ec(X0,X1))) )
& ( pp(scratc983767936_d_not(scratc822302649d_l_ec(X0,X1)))
| ~ pp(scratc876302756_d_and(X0,X1)) ) ),
inference(nnf_transformation,[],[f184]) ).
fof(f1403,plain,
! [X0,X1] :
( ( pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1))
| ~ scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1)) )
& ( scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ) ),
inference(nnf_transformation,[],[f760]) ).
fof(f1566,plain,
! [X0,X1] :
( ( scratc1888847154_is_of(X0,X1)
| ~ pp(aa_TPTP_ind_bool(X1,X0)) )
& ( pp(aa_TPTP_ind_bool(X1,X0))
| ~ scratc1888847154_is_of(X0,X1) ) ),
inference(nnf_transformation,[],[f221]) ).
fof(f1567,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1888847154_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X2] :
( pp(aa_TPTP_ind_bool(X1,X2))
| ~ scratc1888847154_is_of(X2,X0)
| ~ gg_TPTP_ind(X2) )
| ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1)) ) ),
inference(nnf_transformation,[],[f1336]) ).
fof(f1568,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| ? [X2] :
( ~ pp(aa_TPTP_ind_bool(X1,X2))
& scratc1888847154_is_of(X2,X0)
& gg_TPTP_ind(X2) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1888847154_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1)) ) ),
inference(rectify,[],[f1567]) ).
fof(f1569,plain,
! [X0,X1] :
( ( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| ( ~ pp(aa_TPTP_ind_bool(X1,sK18(X0,X1)))
& scratc1888847154_is_of(sK18(X0,X1),X0)
& gg_TPTP_ind(sK18(X0,X1)) ) )
& ( ! [X3] :
( pp(aa_TPTP_ind_bool(X1,X3))
| ~ scratc1888847154_is_of(X3,X0)
| ~ gg_TPTP_ind(X3) )
| ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0,X1))],[f1568]) ).
fof(f1648,plain,
~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab)),
inference(cnf_transformation,[],[f1260]) ).
fof(f1665,plain,
! [X0] :
( ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(cnf_transformation,[],[f1378]) ).
fof(f1666,plain,
! [X0] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_cb,X0)))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) ),
inference(cnf_transformation,[],[f1379]) ).
fof(f1677,plain,
pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_cc)),
inference(cnf_transformation,[],[f222]) ).
fof(f1678,plain,
~ pp(fFalse),
inference(cnf_transformation,[],[f1248]) ).
fof(f1679,plain,
! [X0] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),fFalse))
| ~ pp(scratc983767936_d_not(X0)) ),
inference(cnf_transformation,[],[f1383]) ).
fof(f1691,plain,
! [X0,X1] :
( ~ pp(scratc1898430207nd_or3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1)))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) ),
inference(cnf_transformation,[],[f1387]) ).
fof(f1694,plain,
! [X2,X0,X1] :
( pp(scratc876302756_d_and(scratc1898430207nd_or3(X0,X1,X2),scratc1814831172nd_ec3(X0,X1,X2)))
| ~ scratc1941720897_orec3(X0,X1,X2) ),
inference(cnf_transformation,[],[f1389]) ).
fof(f1701,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),scratc983767936_d_not(X1)))
| pp(scratc822302649d_l_ec(X0,X1)) ),
inference(cnf_transformation,[],[f1392]) ).
fof(f1702,plain,
! [X0,X1] :
( pp(scratc983767936_d_not(scratc822302649d_l_ec(X0,X1)))
| ~ pp(scratc876302756_d_and(X0,X1)) ),
inference(cnf_transformation,[],[f1393]) ).
fof(f1722,plain,
! [X0,X1] :
( scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ),
inference(cnf_transformation,[],[f1403]) ).
fof(f1745,plain,
scratc1848533243nd_imp = fimplies,
inference(cnf_transformation,[],[f189]) ).
fof(f1935,plain,
! [X0,X1] :
( pp(X0)
| pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f1251]) ).
fof(f1937,plain,
! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(fimplies,X0),X1))
| ~ pp(X0)
| pp(X1) ),
inference(cnf_transformation,[],[f1249]) ).
fof(f2164,plain,
! [X0,X1] :
( pp(aa_TPTP_ind_bool(X1,X0))
| ~ scratc1888847154_is_of(X0,X1) ),
inference(cnf_transformation,[],[f1566]) ).
fof(f2165,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X1,X0))
| scratc1888847154_is_of(X0,X1) ),
inference(cnf_transformation,[],[f1566]) ).
fof(f2166,plain,
! [X3,X0,X1] :
( ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| ~ scratc1888847154_is_of(X3,X0)
| ~ gg_TPTP_ind(X3)
| pp(aa_TPTP_ind_bool(X1,X3)) ),
inference(cnf_transformation,[],[f1569]) ).
fof(f2167,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| gg_TPTP_ind(sK18(X0,X1)) ),
inference(cnf_transformation,[],[f1569]) ).
fof(f2168,plain,
! [X0,X1] :
( scratc1888847154_is_of(sK18(X0,X1),X0)
| pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1569]) ).
fof(f2169,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(X1,sK18(X0,X1)))
| pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1)) ),
inference(cnf_transformation,[],[f1569]) ).
fof(f2809,definition,
( spl34_78
<=> pp(fFalse) ),
introduced(definition,[new_symbols(definition,[spl34_78])],[avatar_definition]) ).
fof(f2812,plain,
~ spl34_78,
inference(avatar_split_clause,[],[f1678,f2809]) ).
fof(f2814,definition,
( spl34_79
<=> pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_cc)) ),
introduced(definition,[new_symbols(definition,[spl34_79])],[avatar_definition]) ).
fof(f2816,plain,
( pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_cc))
| ~ spl34_79 ),
inference(avatar_component_clause,[],[f2814]) ).
fof(f2817,plain,
spl34_79,
inference(avatar_split_clause,[],[f1677,f2814]) ).
fof(f2849,definition,
( spl34_86
<=> pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab)) ),
introduced(definition,[new_symbols(definition,[spl34_86])],[avatar_definition]) ).
fof(f2851,plain,
( ~ pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab))
| spl34_86 ),
inference(avatar_component_clause,[],[f2849]) ).
fof(f2852,plain,
~ spl34_86,
inference(avatar_split_clause,[],[f1648,f2849]) ).
fof(f2854,definition,
( spl34_87
<=> scratc1848533243nd_imp = fimplies ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f2856,plain,
( scratc1848533243nd_imp = fimplies
| ~ spl34_87 ),
inference(avatar_component_clause,[],[f2854]) ).
fof(f2857,plain,
spl34_87,
inference(avatar_split_clause,[],[f1745,f2854]) ).
fof(f2890,plain,
( ! [X0] :
( ~ scratc1888847154_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0)
| pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0)) )
| ~ spl34_79 ),
inference(resolution,[],[f2816,f2166]) ).
fof(f2919,plain,
( gg_TPTP_ind(sK18(aTP_Lamm_a,aTP_Lamm_ab))
| spl34_86 ),
inference(resolution,[],[f2167,f2851]) ).
fof(f2923,definition,
( spl34_91
<=> gg_TPTP_ind(sK18(aTP_Lamm_a,aTP_Lamm_ab)) ),
introduced(definition,[new_symbols(definition,[spl34_91])],[avatar_definition]) ).
fof(f2925,plain,
( gg_TPTP_ind(sK18(aTP_Lamm_a,aTP_Lamm_ab))
| ~ spl34_91 ),
inference(avatar_component_clause,[],[f2923]) ).
fof(f2926,plain,
( spl34_91
| spl34_86 ),
inference(avatar_split_clause,[],[f2919,f2849,f2923]) ).
fof(f2928,plain,
( ! [X0,X1] :
( ~ pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),X1))
| ~ pp(X0)
| pp(X1) )
| ~ spl34_87 ),
inference(forward_demodulation,[],[f1937,f2856]) ).
fof(f2939,plain,
( ! [X0] :
( ~ pp(scratc983767936_d_not(X0))
| ~ pp(X0)
| pp(fFalse) )
| ~ spl34_87 ),
inference(resolution,[],[f1679,f2928]) ).
fof(f2941,definition,
( spl34_93
<=> ! [X0] :
( ~ pp(scratc983767936_d_not(X0))
| ~ pp(X0) ) ),
introduced(definition,[new_symbols(definition,[spl34_93])],[avatar_definition]) ).
fof(f2942,plain,
( ! [X0] :
( ~ pp(scratc983767936_d_not(X0))
| ~ pp(X0) )
| ~ spl34_93 ),
inference(avatar_component_clause,[],[f2941]) ).
fof(f2943,plain,
( spl34_78
| spl34_93
| ~ spl34_87 ),
inference(avatar_split_clause,[],[f2939,f2854,f2941,f2809]) ).
fof(f2944,plain,
( ! [X0,X1] :
( pp(aa_bool_bool(aa_boo1142376798l_bool(scratc1848533243nd_imp,X0),X1))
| pp(X0) )
| ~ spl34_87 ),
inference(forward_demodulation,[],[f1935,f2856]) ).
fof(f3034,plain,
( ! [X0,X1] :
( pp(scratc822302649d_l_ec(X0,X1))
| pp(X0) )
| ~ spl34_87 ),
inference(resolution,[],[f1701,f2944]) ).
fof(f3042,plain,
! [X0,X1] :
( ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
| ~ scratc1888847154_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_cb,X0),X1)) ),
inference(resolution,[],[f1666,f2166]) ).
fof(f3043,plain,
! [X0,X1] :
( scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| ~ pp(aa_TPTP_ind_bool(aTP_Lamm_cc,X0))
| ~ scratc1888847154_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1) ),
inference(forward_literal_rewriting,[],[f3042,f1722]) ).
fof(f3072,plain,
! [X0,X1] :
( pp(aa_fun171081125l_bool(scratc1486391335all_of(X0),X1))
| ~ scratc1888847154_is_of(sK18(X0,X1),X1) ),
inference(resolution,[],[f2164,f2169]) ).
fof(f3082,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_ab)
| spl34_86 ),
inference(resolution,[],[f3072,f2851]) ).
fof(f3083,plain,
! [X0] :
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))
| pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0)) ),
inference(resolution,[],[f3072,f1665]) ).
fof(f3086,definition,
( spl34_97
<=> scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_ab) ),
introduced(definition,[new_symbols(definition,[spl34_97])],[avatar_definition]) ).
fof(f3088,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_ab)
| spl34_97 ),
inference(avatar_component_clause,[],[f3086]) ).
fof(f3089,plain,
( ~ spl34_97
| spl34_86 ),
inference(avatar_split_clause,[],[f3082,f2849,f3086]) ).
fof(f3228,plain,
( ! [X0] :
( scratc1888847154_is_of(X0,aTP_Lamm_cc)
| ~ scratc1888847154_is_of(X0,aTP_Lamm_a)
| ~ gg_TPTP_ind(X0) )
| ~ spl34_79 ),
inference(forward_literal_rewriting,[],[f2890,f2165]) ).
fof(f3240,plain,
! [X0] :
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))
| scratc1888847154_is_of(X0,aTP_Lamm_ab) ),
inference(forward_literal_rewriting,[],[f3083,f2165]) ).
fof(f3488,plain,
( ! [X0,X1] :
( ~ pp(scratc822302649d_l_ec(X0,X1))
| ~ pp(scratc876302756_d_and(X0,X1)) )
| ~ spl34_93 ),
inference(forward_literal_rewriting,[],[f1702,f2942]) ).
fof(f3553,plain,
! [X0,X1] :
( scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc)
| ~ scratc1888847154_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1) ),
inference(forward_literal_rewriting,[],[f3043,f2164]) ).
fof(f3584,plain,
( ! [X0,X1] :
( ~ pp(scratc876302756_d_and(X0,X1))
| pp(X0) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3488,f3034]) ).
fof(f3598,plain,
( ! [X2,X0,X1] :
( pp(scratc1898430207nd_or3(X0,X1,X2))
| ~ scratc1941720897_orec3(X0,X1,X2) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3584,f1694]) ).
fof(f3602,plain,
( ! [X0,X1] :
( ~ scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| pp(aa_TPTP_ind_bool(aa_TPT43085870d_bool(aTP_Lamm_aa,X0),X1)) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3598,f1691]) ).
fof(f3605,plain,
( ! [X0,X1] :
( ~ scratc1941720897_orec3(aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc2081115645_rt_is,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc1180647656t_more,X0),X1),aa_TPTP_ind_bool(aa_TPT43085870d_bool(scratc317511020t_less,X0),X1))
| scratc1888847154_is_of(X1,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)) )
| ~ spl34_87
| ~ spl34_93 ),
inference(forward_literal_rewriting,[],[f3602,f2165]) ).
fof(f3684,plain,
( ! [X0,X1] :
( scratc1888847154_is_of(X1,aa_TPT43085870d_bool(aTP_Lamm_aa,X0))
| ~ scratc1888847154_is_of(X1,aTP_Lamm_a)
| ~ gg_TPTP_ind(X1)
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3553,f3605]) ).
fof(f3687,plain,
( ! [X0] :
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)),aTP_Lamm_a)
| ~ gg_TPTP_ind(sK18(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc)
| scratc1888847154_is_of(X0,aTP_Lamm_ab) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3684,f3240]) ).
fof(f3688,plain,
( ! [X0] :
( ~ gg_TPTP_ind(sK18(aTP_Lamm_a,aa_TPT43085870d_bool(aTP_Lamm_aa,X0)))
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc)
| scratc1888847154_is_of(X0,aTP_Lamm_ab)
| pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
| ~ spl34_87
| ~ spl34_93 ),
inference(resolution,[],[f3687,f2168]) ).
fof(f3694,plain,
( ! [X0] :
( ~ scratc1888847154_is_of(X0,aTP_Lamm_cc)
| scratc1888847154_is_of(X0,aTP_Lamm_ab)
| pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aa_TPT43085870d_bool(aTP_Lamm_aa,X0))) )
| ~ spl34_87
| ~ spl34_93 ),
inference(forward_subsumption_resolution,[],[f3688,f2167]) ).
fof(f3695,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc)
| scratc1888847154_is_of(X0,aTP_Lamm_ab) )
| ~ spl34_87
| ~ spl34_93 ),
inference(forward_literal_rewriting,[],[f3694,f1665]) ).
fof(f3696,plain,
( ! [X0] :
( pp(aa_TPTP_ind_bool(aTP_Lamm_ab,X0))
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc) )
| ~ spl34_87
| ~ spl34_93 ),
inference(forward_subsumption_resolution,[],[f3695,f2164]) ).
fof(f3697,plain,
( ! [X0] :
( scratc1888847154_is_of(X0,aTP_Lamm_ab)
| ~ scratc1888847154_is_of(X0,aTP_Lamm_cc) )
| ~ spl34_87
| ~ spl34_93 ),
inference(forward_literal_rewriting,[],[f3696,f2165]) ).
fof(f3698,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_cc)
| ~ spl34_87
| ~ spl34_93
| spl34_97 ),
inference(resolution,[],[f3697,f3088]) ).
fof(f3700,definition,
( spl34_103
<=> scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_cc) ),
introduced(definition,[new_symbols(definition,[spl34_103])],[avatar_definition]) ).
fof(f3702,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_cc)
| spl34_103 ),
inference(avatar_component_clause,[],[f3700]) ).
fof(f3703,plain,
( ~ spl34_103
| ~ spl34_87
| ~ spl34_93
| spl34_97 ),
inference(avatar_split_clause,[],[f3698,f3086,f2941,f2854,f3700]) ).
fof(f3704,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ gg_TPTP_ind(sK18(aTP_Lamm_a,aTP_Lamm_ab))
| ~ spl34_79
| spl34_103 ),
inference(resolution,[],[f3702,f3228]) ).
fof(f3711,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| ~ spl34_79
| ~ spl34_91
| spl34_103 ),
inference(forward_subsumption_resolution,[],[f3704,f2925]) ).
fof(f3713,definition,
( spl34_105
<=> scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a) ),
introduced(definition,[new_symbols(definition,[spl34_105])],[avatar_definition]) ).
fof(f3715,plain,
( ~ scratc1888847154_is_of(sK18(aTP_Lamm_a,aTP_Lamm_ab),aTP_Lamm_a)
| spl34_105 ),
inference(avatar_component_clause,[],[f3713]) ).
fof(f3716,plain,
( ~ spl34_105
| ~ spl34_79
| ~ spl34_91
| spl34_103 ),
inference(avatar_split_clause,[],[f3711,f3700,f2923,f2814,f3713]) ).
fof(f3717,plain,
( pp(aa_fun171081125l_bool(scratc1486391335all_of(aTP_Lamm_a),aTP_Lamm_ab))
| spl34_105 ),
inference(resolution,[],[f3715,f2168]) ).
fof(f3720,plain,
( $false
| spl34_86
| spl34_105 ),
inference(forward_subsumption_resolution,[],[f3717,f2851]) ).
fof(f3721,plain,
( spl34_86
| spl34_105 ),
inference(avatar_contradiction_clause,[],[f3720]) ).
cnf(s78,plain,
~ spl34_78,
inference(sat_conversion,[],[f2812]) ).
cnf(s79,plain,
spl34_79,
inference(sat_conversion,[],[f2817]) ).
cnf(s86,plain,
~ spl34_86,
inference(sat_conversion,[],[f2852]) ).
cnf(s87,plain,
spl34_87,
inference(sat_conversion,[],[f2857]) ).
cnf(s91,plain,
( spl34_86
| spl34_91 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s93,plain,
( spl34_78
| ~ spl34_87
| spl34_93 ),
inference(sat_conversion,[],[f2943]) ).
cnf(s96,plain,
( spl34_86
| ~ spl34_97 ),
inference(sat_conversion,[],[f3089]) ).
cnf(s100,plain,
( ~ spl34_87
| ~ spl34_93
| spl34_97
| ~ spl34_103 ),
inference(sat_conversion,[],[f3703]) ).
cnf(s102,plain,
( ~ spl34_79
| ~ spl34_91
| spl34_103
| ~ spl34_105 ),
inference(sat_conversion,[],[f3716]) ).
cnf(s104,plain,
( spl34_86
| spl34_105 ),
inference(sat_conversion,[],[f3721]) ).
cnf(s105,plain,
spl34_105,
inference(rat,[],[s104,s86]) ).
cnf(s106,plain,
~ spl34_97,
inference(rat,[],[s96,s86]) ).
cnf(s108,plain,
spl34_91,
inference(rat,[],[s91,s86]) ).
cnf(s112,plain,
spl34_103,
inference(rat,[],[s102,s105,s108,s79]) ).
cnf(s113,plain,
~ spl34_93,
inference(rat,[],[s100,s106,s87,s112]) ).
cnf(s114,plain,
spl34_78,
inference(rat,[],[s93,s87,s113]) ).
cnf(s116,plain,
$false,
inference(rat,[],[s78,s114]) ).
fof(f3722,plain,
$false,
inference(avatar_sat_refutation,[],[s116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM783+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.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 21:24:57 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/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
% 12.44/2.69 % (927869)Detected formulas, will run a generic FOF schedule.
% 12.44/2.69 % (927876)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=1030804497:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.44/2.69 % (927880)dis-21_1_sil=8000:lcm=predicate:random_seed=546173254: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)
% 12.44/2.69 % (927874)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=3755529467:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.44/2.69 % (927877)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1960621529:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.44/2.69 % (927875)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=31197301:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.44/2.69 % (927878)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1148101621:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.44/2.69 % (927877)Refutation not found, incomplete strategy
% 12.44/2.69 % (927877)------------------------------
% 12.44/2.69 % (927877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.44/2.69 % (927877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.44/2.69 % (927877)CaDiCaL version: 2.1.3
% 12.44/2.69 % (927877)Termination reason: Refutation not found, incomplete strategy
% 12.44/2.69 % (927877)Time elapsed: 0.004 s
% 12.44/2.69 % (927877)Peak memory usage: 89 MB
% 12.44/2.69 % (927877)Instructions burned: 6 (million)
% 12.44/2.69 % (927879)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3169326882:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.44/2.69 % (927878)Refutation not found, incomplete strategy
% 12.44/2.69 % (927878)------------------------------
% 12.44/2.69 % (927878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.44/2.69 % (927878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.44/2.69 % (927878)CaDiCaL version: 2.1.3
% 12.44/2.69 % (927878)Termination reason: Refutation not found, incomplete strategy
% 12.44/2.69 % (927878)Time elapsed: 0.007 s
% 12.44/2.69 % (927878)Peak memory usage: 89 MB
% 12.44/2.69 % (927878)Instructions burned: 9 (million)
% 12.44/2.69 % (927880)Instruction limit reached!
% 12.44/2.69 % (927880)------------------------------
% 12.44/2.69 % (927880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.44/2.69 % (927880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.44/2.69 % (927880)CaDiCaL version: 2.1.3
% 12.44/2.69 % (927880)Termination reason: Instruction limit
% 12.44/2.69 % (927880)Termination phase: Saturation
% 12.44/2.69 % (927880)Time elapsed: 0.055 s
% 12.44/2.69 % (927880)Peak memory usage: 90 MB
% 12.44/2.69 % (927880)Instructions burned: 130 (million)
% 12.44/2.69 % (927879)Instruction limit reached!
% 12.44/2.69 % (927879)------------------------------
% 12.44/2.69 % (927879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.44/2.69 % (927879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.44/2.69 % (927879)CaDiCaL version: 2.1.3
% 12.44/2.69 % (927879)Termination reason: Instruction limit
% 12.44/2.69 % (927879)Termination phase: Saturation
% 12.44/2.69 % (927879)Time elapsed: 0.063 s
% 12.44/2.69 % (927879)Peak memory usage: 91 MB
% 12.44/2.69 % (927879)Instructions burned: 140 (million)
% 12.44/2.69 % (927888)lrs+10_1_sil=8000:sp=occurrence:random_seed=2328611639:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.44/2.69 % (927888)Refutation not found, incomplete strategy
% 12.44/2.69 % (927888)------------------------------
% 12.44/2.69 % (927888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.44/2.69 % (927888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.44/2.69 % (927888)CaDiCaL version: 2.1.3
% 12.44/2.69 % (927888)Termination reason: Refutation not found, incomplete strategy
% 12.44/2.69 % (927888)Time elapsed: 0.007 s
% 12.44/2.69 % (927888)Peak memory usage: 89 MB
% 12.44/2.69 % (927888)Instructions burned: 9 (million)
% 12.44/2.69 % (927889)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2206226516:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 19.98/3.72 % (927889)Refutation not found, incomplete strategy
% 19.98/3.72 % (927889)------------------------------
% 19.98/3.72 % (927889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.72 % (927889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.72 % (927889)CaDiCaL version: 2.1.3
% 19.98/3.72 % (927889)Termination reason: Refutation not found, incomplete strategy
% 19.98/3.72 % (927889)Time elapsed: 0.010 s
% 19.98/3.72 % (927889)Peak memory usage: 89 MB
% 19.98/3.72 % (927889)Instructions burned: 20 (million)
% 19.98/3.72 % (927878)------------------------------
% 19.98/3.72 % (927878)------------------------------
% 19.98/3.72 % (927877)------------------------------
% 19.98/3.72 % (927877)------------------------------
% 19.98/3.72 % (927892)lrs+1011_1_sil=32000:sp=occurrence:random_seed=112670071:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 19.98/3.72 % (927893)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=2081332781:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 19.98/3.72 % (927892)Refutation not found, incomplete strategy
% 19.98/3.72 % (927892)------------------------------
% 19.98/3.72 % (927892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.72 % (927892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.72 % (927892)CaDiCaL version: 2.1.3
% 19.98/3.72 % (927892)Termination reason: Refutation not found, incomplete strategy
% 19.98/3.72 % (927892)Time elapsed: 0.008 s
% 19.98/3.72 % (927892)Peak memory usage: 90 MB
% 19.98/3.72 % (927892)Instructions burned: 10 (million)
% 19.98/3.72 % (927888)------------------------------
% 19.98/3.72 % (927888)------------------------------
% 19.98/3.72 % (927889)------------------------------
% 19.98/3.72 % (927889)------------------------------
% 19.98/3.72 % (927893)Instruction limit reached!
% 19.98/3.72 % (927893)------------------------------
% 19.98/3.72 % (927893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.72 % (927893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.72 % (927893)CaDiCaL version: 2.1.3
% 19.98/3.72 % (927893)Termination reason: Instruction limit
% 19.98/3.72 % (927893)Termination phase: Saturation
% 19.98/3.72 % (927893)Time elapsed: 0.131 s
% 19.98/3.72 % (927893)Peak memory usage: 93 MB
% 19.98/3.72 % (927893)Instructions burned: 248 (million)
% 19.98/3.72 % (927896)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=99748173:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.98/3.72 % (927896)Refutation not found, incomplete strategy
% 19.98/3.72 % (927896)------------------------------
% 19.98/3.72 % (927896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.72 % (927896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.72 % (927896)CaDiCaL version: 2.1.3
% 19.98/3.72 % (927896)Termination reason: Refutation not found, incomplete strategy
% 19.98/3.72 % (927896)Time elapsed: 0.010 s
% 19.98/3.72 % (927896)Peak memory usage: 90 MB
% 19.98/3.72 % (927896)Instructions burned: 14 (million)
% 19.98/3.72 % (927897)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=411322139:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.98/3.72 % (927892)------------------------------
% 19.98/3.72 % (927892)------------------------------
% 19.98/3.72 % (927898)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1080252153:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 19.98/3.72 % (927898)Instruction limit reached!
% 19.98/3.72 % (927898)------------------------------
% 19.98/3.72 % (927898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.98/3.72 % (927898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.98/3.72 % (927898)CaDiCaL version: 2.1.3
% 19.98/3.72 % (927898)Termination reason: Instruction limit
% 19.98/3.72 % (927898)Termination phase: Saturation
% 19.98/3.72 % (927898)Time elapsed: 0.053 s
% 19.98/3.72 % (927898)Peak memory usage: 90 MB
% 19.98/3.72 % (927898)Instructions burned: 113 (million)
% 19.98/3.72 % (927902)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=650185489:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 19.98/3.72 % (927903)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3525813863:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 47.91/7.64 % (927902)Instruction limit reached!
% 47.91/7.64 % (927902)------------------------------
% 47.91/7.64 % (927902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927902)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927902)Termination reason: Instruction limit
% 47.91/7.64 % (927902)Termination phase: Property scanning
% 47.91/7.64 % (927902)Time elapsed: 0.057 s
% 47.91/7.64 % (927902)Peak memory usage: 89 MB
% 47.91/7.64 % (927902)Instructions burned: 130 (million)
% 47.91/7.64 % (927896)------------------------------
% 47.91/7.64 % (927896)------------------------------
% 47.91/7.64 % (927903)Instruction limit reached!
% 47.91/7.64 % (927903)------------------------------
% 47.91/7.64 % (927903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927903)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927903)Termination reason: Instruction limit
% 47.91/7.64 % (927903)Termination phase: Saturation
% 47.91/7.64 % (927903)Time elapsed: 0.058 s
% 47.91/7.64 % (927903)Peak memory usage: 90 MB
% 47.91/7.64 % (927903)Instructions burned: 116 (million)
% 47.91/7.64 % (927906)lrs+10_1_sil=8000:sp=occurrence:random_seed=2492755999:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 47.91/7.64 % (927907)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2238825927:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 47.91/7.64 % (927908)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2308175180:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 47.91/7.64 % (927907)Refutation not found, incomplete strategy
% 47.91/7.64 % (927907)------------------------------
% 47.91/7.64 % (927907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927907)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927907)Termination reason: Refutation not found, incomplete strategy
% 47.91/7.64 % (927907)Time elapsed: 0.091 s
% 47.91/7.64 % (927907)Peak memory usage: 93 MB
% 47.91/7.64 % (927907)Instructions burned: 189 (million)
% 47.91/7.64 % (927907)------------------------------
% 47.91/7.64 % (927907)------------------------------
% 47.91/7.64 % (927912)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3163271947:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 47.91/7.64 % (927906)Instruction limit reached!
% 47.91/7.64 % (927906)------------------------------
% 47.91/7.64 % (927906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927906)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927906)Termination reason: Instruction limit
% 47.91/7.64 % (927906)Termination phase: Saturation
% 47.91/7.64 % (927906)Time elapsed: 0.534 s
% 47.91/7.64 % (927906)Peak memory usage: 102 MB
% 47.91/7.64 % (927906)Instructions burned: 907 (million)
% 47.91/7.64 % (927912)Instruction limit reached!
% 47.91/7.64 % (927912)------------------------------
% 47.91/7.64 % (927912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927912)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927912)Termination reason: Instruction limit
% 47.91/7.64 % (927912)Termination phase: Saturation
% 47.91/7.64 % (927912)Time elapsed: 0.063 s
% 47.91/7.64 % (927912)Peak memory usage: 91 MB
% 47.91/7.64 % (927912)Instructions burned: 136 (million)
% 47.91/7.64 % (927914)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3220039163:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 47.91/7.64 % (927914)Refutation not found, incomplete strategy
% 47.91/7.64 % (927914)------------------------------
% 47.91/7.64 % (927914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.91/7.64 % (927914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.91/7.64 % (927914)CaDiCaL version: 2.1.3
% 47.91/7.64 % (927914)Termination reason: Refutation not found, incomplete strategy
% 47.91/7.64 % (927914)Time elapsed: 0.021 s
% 47.91/7.64 % (927914)Peak memory usage: 90 MB
% 47.91/7.64 % (927914)Instructions burned: 38 (million)
% 47.91/7.64 % (927915)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3212575337:st=3:i=13193:sd=3:ss=axioms_2982 on theBenchmark for (2982ds/13193Mi)
% 78.74/12.05 % (927914)------------------------------
% 78.74/12.05 % (927914)------------------------------
% 78.74/12.05 % (927897)Instruction limit reached!
% 78.74/12.05 % (927897)------------------------------
% 78.74/12.05 % (927897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.74/12.05 % (927897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.74/12.05 % (927897)CaDiCaL version: 2.1.3
% 78.74/12.05 % (927897)Termination reason: Instruction limit
% 78.74/12.05 % (927897)Termination phase: Saturation
% 78.74/12.05 % (927897)Time elapsed: 1.377 s
% 78.74/12.05 % (927897)Peak memory usage: 159 MB
% 78.74/12.05 % (927897)Instructions burned: 2350 (million)
% 78.74/12.05 % (927918)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=3994134960:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 78.74/12.05 % (927918)Instruction limit reached!
% 78.74/12.05 % (927918)------------------------------
% 78.74/12.05 % (927918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.74/12.05 % (927918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.74/12.05 % (927918)CaDiCaL version: 2.1.3
% 78.74/12.05 % (927918)Termination reason: Instruction limit
% 78.74/12.05 % (927918)Termination phase: Saturation
% 78.74/12.05 % (927918)Time elapsed: 0.068 s
% 78.74/12.05 % (927918)Peak memory usage: 91 MB
% 78.74/12.05 % (927918)Instructions burned: 127 (million)
% 78.74/12.05 % (927920)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=847622574:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 78.74/12.05 % (927920)Instruction limit reached!
% 78.74/12.05 % (927920)------------------------------
% 78.74/12.05 % (927920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.74/12.05 % (927920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.74/12.05 % (927920)CaDiCaL version: 2.1.3
% 78.74/12.05 % (927920)Termination reason: Instruction limit
% 78.74/12.05 % (927920)Termination phase: Twee Goal Transformation
% 78.74/12.05 % (927920)Time elapsed: 0.064 s
% 78.74/12.05 % (927920)Peak memory usage: 91 MB
% 78.74/12.05 % (927920)Instructions burned: 135 (million)
% 78.74/12.05 % (927921)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2062014345:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 78.74/12.05 % (927921)Refutation not found, incomplete strategy
% 78.74/12.05 % (927921)------------------------------
% 78.74/12.05 % (927921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.74/12.05 % (927921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.74/12.05 % (927921)CaDiCaL version: 2.1.3
% 78.74/12.05 % (927921)Termination reason: Refutation not found, incomplete strategy
% 78.74/12.05 % (927921)Time elapsed: 0.004 s
% 78.74/12.05 % (927921)Peak memory usage: 89 MB
% 78.74/12.05 % (927921)Instructions burned: 6 (million)
% 78.74/12.05 % (927924)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4176384569:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 78.74/12.05 % (927924)Refutation not found, incomplete strategy
% 78.74/12.05 % (927924)------------------------------
% 78.74/12.05 % (927924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.74/12.05 % (927924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.74/12.05 % (927924)CaDiCaL version: 2.1.3
% 78.74/12.05 % (927924)Termination reason: Refutation not found, incomplete strategy
% 78.74/12.05 % (927924)Time elapsed: 0.005 s
% 78.74/12.05 % (927924)Peak memory usage: 90 MB
% 78.74/12.05 % (927924)Instructions burned: 6 (million)
% 78.74/12.05 % (927921)------------------------------
% 78.74/12.05 % (927921)------------------------------
% 78.74/12.05 % (927924)------------------------------
% 78.74/12.05 % (927924)------------------------------
% 78.74/12.05 % (927926)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=514731444:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 78.74/12.05 % (927928)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1900518284:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 107.09/16.09 % (927928)Instruction limit reached!
% 107.09/16.09 % (927928)------------------------------
% 107.09/16.09 % (927928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927928)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927928)Termination reason: Instruction limit
% 107.09/16.09 % (927928)Termination phase: Saturation
% 107.09/16.09 % (927928)Time elapsed: 0.066 s
% 107.09/16.09 % (927928)Peak memory usage: 91 MB
% 107.09/16.09 % (927928)Instructions burned: 150 (million)
% 107.09/16.09 % (927930)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=496080846:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 107.09/16.09 % (927908)Instruction limit reached!
% 107.09/16.09 % (927908)------------------------------
% 107.09/16.09 % (927908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927908)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927908)Termination reason: Instruction limit
% 107.09/16.09 % (927908)Termination phase: Saturation
% 107.09/16.09 % (927908)Time elapsed: 3.386 s
% 107.09/16.09 % (927908)Peak memory usage: 160 MB
% 107.09/16.09 % (927908)Instructions burned: 5203 (million)
% 107.09/16.09 % (927932)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1344432082:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 107.09/16.09 % (927932)Instruction limit reached!
% 107.09/16.09 % (927932)------------------------------
% 107.09/16.09 % (927932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927932)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927932)Termination reason: Instruction limit
% 107.09/16.09 % (927932)Termination phase: Saturation
% 107.09/16.09 % (927932)Time elapsed: 0.312 s
% 107.09/16.09 % (927932)Peak memory usage: 100 MB
% 107.09/16.09 % (927932)Instructions burned: 667 (million)
% 107.09/16.09 % (927934)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3340805487:s2a=on:i=185:s2at=1.8:fdi=4_2949 on theBenchmark for (2949ds/185Mi)
% 107.09/16.09 % (927934)Instruction limit reached!
% 107.09/16.09 % (927934)------------------------------
% 107.09/16.09 % (927934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927934)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927934)Termination reason: Instruction limit
% 107.09/16.09 % (927934)Termination phase: Saturation
% 107.09/16.09 % (927934)Time elapsed: 0.080 s
% 107.09/16.09 % (927934)Peak memory usage: 91 MB
% 107.09/16.09 % (927934)Instructions burned: 187 (million)
% 107.09/16.09 % (927936)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3886992929:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2947 on theBenchmark for (2947ds/193Mi)
% 107.09/16.09 % (927936)Refutation not found, incomplete strategy
% 107.09/16.09 % (927936)------------------------------
% 107.09/16.09 % (927936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927936)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927936)Termination reason: Refutation not found, incomplete strategy
% 107.09/16.09 % (927936)Time elapsed: 0.010 s
% 107.09/16.09 % (927936)Peak memory usage: 90 MB
% 107.09/16.09 % (927936)Instructions burned: 15 (million)
% 107.09/16.09 % (927936)------------------------------
% 107.09/16.09 % (927936)------------------------------
% 107.09/16.09 % (927938)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1565555633:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2942 on theBenchmark for (2942ds/4850Mi)
% 107.09/16.09 % (927926)Instruction limit reached!
% 107.09/16.09 % (927926)------------------------------
% 107.09/16.09 % (927926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.09/16.09 % (927926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.09/16.09 % (927926)CaDiCaL version: 2.1.3
% 107.09/16.09 % (927926)Termination reason: Instruction limit
% 107.09/16.09 % (927926)Termination phase: Saturation
% 107.09/16.09 % (927926)Time elapsed: 4.043 s
% 131.25/19.54 % (927926)Peak memory usage: 173 MB
% 131.25/19.54 % (927926)Instructions burned: 6061 (million)
% 131.25/19.54 % (927940)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2742180491:i=12111:sd=1:ss=included_2931 on theBenchmark for (2931ds/12111Mi)
% 131.25/19.54 % (927938)Instruction limit reached!
% 131.25/19.54 % (927938)------------------------------
% 131.25/19.54 % (927938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927938)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927938)Termination reason: Instruction limit
% 131.25/19.54 % (927938)Termination phase: Saturation
% 131.25/19.54 % (927938)Time elapsed: 3.059 s
% 131.25/19.54 % (927938)Peak memory usage: 139 MB
% 131.25/19.54 % (927938)Instructions burned: 4851 (million)
% 131.25/19.54 % (927942)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=845343943:i=319:kws=precedence:fsr=off_2911 on theBenchmark for (2911ds/319Mi)
% 131.25/19.54 % (927942)Instruction limit reached!
% 131.25/19.54 % (927942)------------------------------
% 131.25/19.54 % (927942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927942)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927942)Termination reason: Instruction limit
% 131.25/19.54 % (927942)Termination phase: Saturation
% 131.25/19.54 % (927942)Time elapsed: 0.156 s
% 131.25/19.54 % (927942)Peak memory usage: 95 MB
% 131.25/19.54 % (927942)Instructions burned: 321 (million)
% 131.25/19.54 % (927944)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1155779044:i=2064:ep=RST_2908 on theBenchmark for (2908ds/2064Mi)
% 131.25/19.54 % (927944)Refutation not found, incomplete strategy
% 131.25/19.54 % (927944)------------------------------
% 131.25/19.54 % (927944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927944)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927944)Termination reason: Refutation not found, incomplete strategy
% 131.25/19.54 % (927944)Time elapsed: 0.072 s
% 131.25/19.54 % (927944)Peak memory usage: 92 MB
% 131.25/19.54 % (927944)Instructions burned: 163 (million)
% 131.25/19.54 % (927944)------------------------------
% 131.25/19.54 % (927944)------------------------------
% 131.25/19.54 % (927915)Instruction limit reached!
% 131.25/19.54 % (927915)------------------------------
% 131.25/19.54 % (927915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927915)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927915)Termination reason: Instruction limit
% 131.25/19.54 % (927915)Termination phase: Saturation
% 131.25/19.54 % (927915)Time elapsed: 7.812 s
% 131.25/19.54 % (927915)Peak memory usage: 232 MB
% 131.25/19.54 % (927915)Instructions burned: 13194 (million)
% 131.25/19.54 % (927946)dis-1011_128_sil=32000:random_seed=1873003930:i=3706:ep=RST:av=off_2903 on theBenchmark for (2903ds/3706Mi)
% 131.25/19.54 % (927947)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1277162420:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2903 on theBenchmark for (2903ds/757Mi)
% 131.25/19.54 % (927947)Refutation not found, incomplete strategy
% 131.25/19.54 % (927947)------------------------------
% 131.25/19.54 % (927947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927947)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927947)Termination reason: Refutation not found, incomplete strategy
% 131.25/19.54 % (927947)Time elapsed: 0.011 s
% 131.25/19.54 % (927947)Peak memory usage: 90 MB
% 131.25/19.54 % (927947)Instructions burned: 17 (million)
% 131.25/19.54 % (927947)------------------------------
% 131.25/19.54 % (927947)------------------------------
% 131.25/19.54 % (927950)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2422884228:i=13913:ss=axioms:sgt=8_2899 on theBenchmark for (2899ds/13913Mi)
% 131.25/19.54 % (927930)Instruction limit reached!
% 131.25/19.54 % (927930)------------------------------
% 131.25/19.54 % (927930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 131.25/19.54 % (927930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.25/19.54 % (927930)CaDiCaL version: 2.1.3
% 131.25/19.54 % (927930)Termination reason: Instruction limit
% 146.63/21.76 % (927930)Termination phase: Saturation
% 146.63/21.76 % (927930)Time elapsed: 8.136 s
% 146.63/21.76 % (927930)Peak memory usage: 212 MB
% 146.63/21.76 % (927930)Instructions burned: 14157 (million)
% 146.63/21.76 % (927952)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3893108881:i=9925:aac=none_2887 on theBenchmark for (2887ds/9925Mi)
% 146.63/21.76 % (927946)Instruction limit reached!
% 146.63/21.76 % (927946)------------------------------
% 146.63/21.76 % (927946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.63/21.76 % (927946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.63/21.76 % (927946)CaDiCaL version: 2.1.3
% 146.63/21.76 % (927946)Termination reason: Instruction limit
% 146.63/21.76 % (927946)Termination phase: Saturation
% 146.63/21.76 % (927946)Time elapsed: 2.068 s
% 146.63/21.76 % (927946)Peak memory usage: 109 MB
% 146.63/21.76 % (927946)Instructions burned: 3707 (million)
% 146.63/21.76 % (927954)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3073731869:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2881 on theBenchmark for (2881ds/2479Mi)
% 146.63/21.76 % (927954)Refutation not found, incomplete strategy
% 146.63/21.76 % (927954)------------------------------
% 146.63/21.76 % (927954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.63/21.76 % (927954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.63/21.76 % (927954)CaDiCaL version: 2.1.3
% 146.63/21.76 % (927954)Termination reason: Refutation not found, incomplete strategy
% 146.63/21.76 % (927954)Time elapsed: 0.007 s
% 146.63/21.76 % (927954)Peak memory usage: 89 MB
% 146.63/21.76 % (927954)Instructions burned: 11 (million)
% 146.63/21.76 % (927954)------------------------------
% 146.63/21.76 % (927954)------------------------------
% 146.63/21.76 % (927956)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3889657787:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2877 on theBenchmark for (2877ds/440Mi)
% 146.63/21.76 % (927956)Instruction limit reached!
% 146.63/21.76 % (927956)------------------------------
% 146.63/21.76 % (927956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.63/21.76 % (927956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.63/21.76 % (927956)CaDiCaL version: 2.1.3
% 146.63/21.76 % (927956)Termination reason: Instruction limit
% 146.63/21.76 % (927956)Termination phase: Saturation
% 146.63/21.76 % (927956)Time elapsed: 0.166 s
% 146.63/21.76 % (927956)Peak memory usage: 91 MB
% 146.63/21.76 % (927956)Instructions burned: 443 (million)
% 146.63/21.76 % (927958)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2903336823:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2874 on theBenchmark for (2874ds/11145Mi)
% 146.63/21.76 % (927958)Refutation not found, incomplete strategy
% 146.63/21.76 % (927958)------------------------------
% 146.63/21.76 % (927958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.63/21.76 % (927958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.63/21.76 % (927958)CaDiCaL version: 2.1.3
% 146.63/21.76 % (927958)Termination reason: Refutation not found, incomplete strategy
% 146.63/21.76 % (927958)Time elapsed: 0.628 s
% 146.63/21.76 % (927958)Peak memory usage: 133 MB
% 146.63/21.76 % (927958)Instructions burned: 947 (million)
% 146.63/21.76 % (927958)------------------------------
% 146.63/21.76 % (927958)------------------------------
% 146.63/21.76 % (927960)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=297807273:cts=off:i=3034:av=off:er=known:fsd=on_2864 on theBenchmark for (2864ds/3034Mi)
% 146.63/21.76 % (927940)Instruction limit reached!
% 146.63/21.76 % (927940)------------------------------
% 146.63/21.76 % (927940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.63/21.76 % (927940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.63/21.76 % (927940)CaDiCaL version: 2.1.3
% 146.63/21.76 % (927940)Termination reason: Instruction limit
% 146.63/21.76 % (927940)Termination phase: Saturation
% 146.63/21.76 % (927940)Time elapsed: 7.226 s
% 146.63/21.76 % (927940)Peak memory usage: 229 MB
% 146.63/21.76 % (927940)Instructions burned: 12111 (million)
% 146.63/21.76 % (927962)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1319107304:st=2:s2a=on:i=524:s2at=2:ss=axioms_2851 on theBenchmark for (2851ds/524Mi)
% 146.63/21.76 % (927962)Instruction limit reached!
% 146.63/21.76 % (927962)------------------------------
% 172.52/25.31 % (927962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927962)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927962)Termination reason: Instruction limit
% 172.52/25.31 % (927962)Termination phase: Saturation
% 172.52/25.31 % (927962)Time elapsed: 0.281 s
% 172.52/25.31 % (927962)Peak memory usage: 93 MB
% 172.52/25.31 % (927962)Instructions burned: 526 (million)
% 172.52/25.31 % (927960)Instruction limit reached!
% 172.52/25.31 % (927960)------------------------------
% 172.52/25.31 % (927960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927960)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927960)Termination reason: Instruction limit
% 172.52/25.31 % (927960)Termination phase: Saturation
% 172.52/25.31 % (927960)Time elapsed: 1.702 s
% 172.52/25.31 % (927960)Peak memory usage: 161 MB
% 172.52/25.31 % (927960)Instructions burned: 3035 (million)
% 172.52/25.31 % (927964)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=4176961744:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2847 on theBenchmark for (2847ds/1016Mi)
% 172.52/25.31 % (927964)Refutation not found, incomplete strategy
% 172.52/25.31 % (927964)------------------------------
% 172.52/25.31 % (927964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927964)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927964)Termination reason: Refutation not found, incomplete strategy
% 172.52/25.31 % (927964)Time elapsed: 0.005 s
% 172.52/25.31 % (927964)Peak memory usage: 90 MB
% 172.52/25.31 % (927964)Instructions burned: 6 (million)
% 172.52/25.31 % (927966)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2220167227:i=14123:bd=preordered:ins=4_2846 on theBenchmark for (2846ds/14123Mi)
% 172.52/25.31 % (927964)------------------------------
% 172.52/25.31 % (927964)------------------------------
% 172.52/25.31 % (927968)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=838125274:i=5781:kws=precedence:bd=all:rawr=on_2843 on theBenchmark for (2843ds/5781Mi)
% 172.52/25.31 % (927952)Instruction limit reached!
% 172.52/25.31 % (927952)------------------------------
% 172.52/25.31 % (927952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927952)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927952)Termination reason: Instruction limit
% 172.52/25.31 % (927952)Termination phase: Saturation
% 172.52/25.31 % (927952)Time elapsed: 5.349 s
% 172.52/25.31 % (927952)Peak memory usage: 220 MB
% 172.52/25.31 % (927952)Instructions burned: 9926 (million)
% 172.52/25.31 % (927970)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3656400155:i=2448:gtgl=5:bd=preordered:gtg=all_2832 on theBenchmark for (2832ds/2448Mi)
% 172.52/25.31 % (927970)Instruction limit reached!
% 172.52/25.31 % (927970)------------------------------
% 172.52/25.31 % (927970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927970)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927970)Termination reason: Instruction limit
% 172.52/25.31 % (927970)Termination phase: Saturation
% 172.52/25.31 % (927970)Time elapsed: 1.376 s
% 172.52/25.31 % (927970)Peak memory usage: 164 MB
% 172.52/25.31 % (927970)Instructions burned: 2449 (million)
% 172.52/25.31 % (927972)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2965736487:i=3223:kws=precedence:fgj=on:av=off_2817 on theBenchmark for (2817ds/3223Mi)
% 172.52/25.31 % (927968)Instruction limit reached!
% 172.52/25.31 % (927968)------------------------------
% 172.52/25.31 % (927968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.52/25.31 % (927968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.52/25.31 % (927968)CaDiCaL version: 2.1.3
% 172.52/25.31 % (927968)Termination reason: Instruction limit
% 172.52/25.31 % (927968)Termination phase: Saturation
% 172.52/25.31 % (927968)Time elapsed: 2.804 s
% 172.52/25.31 % (927968)Peak memory usage: 118 MB
% 172.52/25.31 % (927968)Instructions burned: 5782 (million)
% 172.52/25.31 % (927974)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3650040597:st=5.6:i=2033:sd=3:ss=axioms_2814 on theBenchmark for (2814ds/2033Mi)
% 206.46/30.05 % (927950)Instruction limit reached!
% 206.46/30.05 % (927950)------------------------------
% 206.46/30.05 % (927950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.46/30.05 % (927950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.46/30.05 % (927950)CaDiCaL version: 2.1.3
% 206.46/30.05 % (927950)Termination reason: Instruction limit
% 206.46/30.05 % (927950)Termination phase: Saturation
% 206.46/30.05 % (927950)Time elapsed: 8.531 s
% 206.46/30.05 % (927950)Peak memory usage: 178 MB
% 206.46/30.05 % (927950)Instructions burned: 13914 (million)
% 206.46/30.05 % (927976)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2835298052:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2812 on theBenchmark for (2812ds/2055Mi)
% 206.46/30.05 % (927974)Refutation not found, incomplete strategy
% 206.46/30.05 % (927974)------------------------------
% 206.46/30.05 % (927974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.46/30.05 % (927974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.46/30.05 % (927974)CaDiCaL version: 2.1.3
% 206.46/30.05 % (927974)Termination reason: Refutation not found, incomplete strategy
% 206.46/30.05 % (927974)Time elapsed: 0.646 s
% 206.46/30.05 % (927974)Peak memory usage: 135 MB
% 206.46/30.05 % (927974)Instructions burned: 982 (million)
% 206.46/30.05 % (927976)Refutation not found, incomplete strategy
% 206.46/30.05 % (927976)------------------------------
% 206.46/30.05 % (927976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.46/30.05 % (927976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.46/30.05 % (927976)CaDiCaL version: 2.1.3
% 206.46/30.05 % (927976)Termination reason: Refutation not found, incomplete strategy
% 206.46/30.05 % (927976)Time elapsed: 0.601 s
% 206.46/30.05 % (927976)Peak memory usage: 132 MB
% 206.46/30.05 % (927976)Instructions burned: 920 (million)
% 206.46/30.05 % (927974)------------------------------
% 206.46/30.05 % (927974)------------------------------
% 206.46/30.05 % (927976)------------------------------
% 206.46/30.05 % (927976)------------------------------
% 206.46/30.05 % (927978)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3612191571:i=21611:sd=3:ss=axioms_2804 on theBenchmark for (2804ds/21611Mi)
% 206.46/30.05 % (927979)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=754405785:i=4835:sd=13:ss=axioms:sgt=23_2802 on theBenchmark for (2802ds/4835Mi)
% 206.46/30.05 % (927978)Refutation not found, incomplete strategy
% 206.46/30.05 % (927978)------------------------------
% 206.46/30.05 % (927978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.46/30.05 % (927978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.46/30.05 % (927978)CaDiCaL version: 2.1.3
% 206.46/30.05 % (927978)Termination reason: Refutation not found, incomplete strategy
% 206.46/30.05 % (927978)Time elapsed: 0.613 s
% 206.46/30.05 % (927978)Peak memory usage: 132 MB
% 206.46/30.05 % (927978)Instructions burned: 928 (million)
% 206.46/30.05 % (927972)Instruction limit reached!
% 206.46/30.05 % (927972)------------------------------
% 206.46/30.05 % (927972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 206.46/30.05 % (927972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 206.46/30.05 % (927972)CaDiCaL version: 2.1.3
% 206.46/30.05 % (927972)Termination reason: Instruction limit
% 206.46/30.05 % (927972)Termination phase: Saturation
% 206.46/30.05 % (927972)Time elapsed: 2.032 s
% 206.46/30.05 % (927972)Peak memory usage: 166 MB
% 206.46/30.05 % (927972)Instructions burned: 3223 (million)
% 206.46/30.05 % (927982)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3969746397:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2795 on theBenchmark for (2795ds/797Mi)
% 206.46/30.05 % (927978)------------------------------
% 206.46/30.05 % (927978)------------------------------
% 206.46/30.05 % (927984)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3136496230:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2793 on theBenchmark for (2793ds/2326Mi)
% 206.46/30.05 % (927982)Instruction limit reached!
% 206.46/30.05 % (927982)------------------------------
% 206.46/30.05 % (927982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927982)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927982)Termination reason: Instruction limit
% 144.00/31.52 % (927982)Termination phase: Saturation
% 144.00/31.52 % (927982)Time elapsed: 0.360 s
% 144.00/31.52 % (927982)Peak memory usage: 94 MB
% 144.00/31.52 % (927982)Instructions burned: 798 (million)
% 144.00/31.52 % (927986)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2168955123:i=6038:nm=6_2790 on theBenchmark for (2790ds/6038Mi)
% 144.00/31.52 % (927984)Instruction limit reached!
% 144.00/31.52 % (927984)------------------------------
% 144.00/31.52 % (927984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927984)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927984)Termination reason: Instruction limit
% 144.00/31.52 % (927984)Termination phase: Saturation
% 144.00/31.52 % (927984)Time elapsed: 1.415 s
% 144.00/31.52 % (927984)Peak memory usage: 105 MB
% 144.00/31.52 % (927984)Instructions burned: 2326 (million)
% 144.00/31.52 % (927988)lrs+10_1_sil=32000:sp=occurrence:random_seed=1585284313:st=2:i=33334:sd=3:ss=included:sgt=32_2778 on theBenchmark for (2778ds/33334Mi)
% 144.00/31.52 % (927979)Instruction limit reached!
% 144.00/31.52 % (927979)------------------------------
% 144.00/31.52 % (927979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927979)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927979)Termination reason: Instruction limit
% 144.00/31.52 % (927979)Termination phase: Saturation
% 144.00/31.52 % (927979)Time elapsed: 2.801 s
% 144.00/31.52 % (927979)Peak memory usage: 137 MB
% 144.00/31.52 % (927979)Instructions burned: 4835 (million)
% 144.00/31.52 % (927990)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1650190997:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2773 on theBenchmark for (2773ds/1008Mi)
% 144.00/31.52 % (927990)Refutation not found, incomplete strategy
% 144.00/31.52 % (927990)------------------------------
% 144.00/31.52 % (927990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927990)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927990)Termination reason: Refutation not found, incomplete strategy
% 144.00/31.52 % (927990)Time elapsed: 0.082 s
% 144.00/31.52 % (927990)Peak memory usage: 91 MB
% 144.00/31.52 % (927990)Instructions burned: 139 (million)
% 144.00/31.52 % (927990)------------------------------
% 144.00/31.52 % (927990)------------------------------
% 144.00/31.52 % (927992)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=3580598241:i=8327:s2at=5:bd=preordered_2768 on theBenchmark for (2768ds/8327Mi)
% 144.00/31.52 % (927986)Instruction limit reached!
% 144.00/31.52 % (927986)------------------------------
% 144.00/31.52 % (927986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927986)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927986)Termination reason: Instruction limit
% 144.00/31.52 % (927986)Termination phase: Saturation
% 144.00/31.52 % (927986)Time elapsed: 3.153 s
% 144.00/31.52 % (927986)Peak memory usage: 217 MB
% 144.00/31.52 % (927986)Instructions burned: 6039 (million)
% 144.00/31.52 % (927966)Instruction limit reached!
% 144.00/31.52 % (927966)------------------------------
% 144.00/31.52 % (927966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927966)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927966)Termination reason: Instruction limit
% 144.00/31.52 % (927966)Termination phase: Saturation
% 144.00/31.52 % (927966)Time elapsed: 8.799 s
% 144.00/31.52 % (927966)Peak memory usage: 234 MB
% 144.00/31.52 % (927966)Instructions burned: 14123 (million)
% 144.00/31.52 % (927994)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3791371981:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2757 on theBenchmark for (2757ds/1083Mi)
% 144.00/31.52 % (927996)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2396806943:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2756 on theBenchmark for (2756ds/1084Mi)
% 144.00/31.52 % (927994)Instruction limit reached!
% 144.00/31.52 % (927994)------------------------------
% 144.00/31.52 % (927994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927994)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927994)Termination reason: Instruction limit
% 144.00/31.52 % (927994)Termination phase: Saturation
% 144.00/31.52 % (927994)Time elapsed: 0.378 s
% 144.00/31.52 % (927994)Peak memory usage: 92 MB
% 144.00/31.52 % (927994)Instructions burned: 1085 (million)
% 144.00/31.52 % (927998)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2529064712:i=6995:s2at=5:gtg=all_2752 on theBenchmark for (2752ds/6995Mi)
% 144.00/31.52 % (927996)Instruction limit reached!
% 144.00/31.52 % (927996)------------------------------
% 144.00/31.52 % (927996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927996)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927996)Termination reason: Instruction limit
% 144.00/31.52 % (927996)Termination phase: Saturation
% 144.00/31.52 % (927996)Time elapsed: 0.499 s
% 144.00/31.52 % (927996)Peak memory usage: 92 MB
% 144.00/31.52 % (927996)Instructions burned: 1084 (million)
% 144.00/31.52 % (928000)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=309606284:st=2:i=6225:sd=15:ss=axioms_2750 on theBenchmark for (2750ds/6225Mi)
% 144.00/31.52 % (928000)Instruction limit reached!
% 144.00/31.52 % (928000)------------------------------
% 144.00/31.52 % (928000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (928000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (928000)CaDiCaL version: 2.1.3
% 144.00/31.52 % (928000)Termination reason: Instruction limit
% 144.00/31.52 % (928000)Termination phase: Saturation
% 144.00/31.52 % (928000)Time elapsed: 2.987 s
% 144.00/31.52 % (928000)Peak memory usage: 170 MB
% 144.00/31.52 % (928000)Instructions burned: 6226 (million)
% 144.00/31.52 % (928002)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=525687609:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2719 on theBenchmark for (2719ds/3372Mi)
% 144.00/31.52 % (927992)Instruction limit reached!
% 144.00/31.52 % (927992)------------------------------
% 144.00/31.52 % (927992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927992)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927992)Termination reason: Instruction limit
% 144.00/31.52 % (927992)Termination phase: Saturation
% 144.00/31.52 % (927992)Time elapsed: 5.151 s
% 144.00/31.52 % (927992)Peak memory usage: 205 MB
% 144.00/31.52 % (927992)Instructions burned: 8327 (million)
% 144.00/31.52 % (928004)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=249712077:st=2.3:i=26457:sd=10:ss=included:sgt=8_2715 on theBenchmark for (2715ds/26457Mi)
% 144.00/31.52 % (928002)Refutation not found, incomplete strategy
% 144.00/31.52 % (928002)------------------------------
% 144.00/31.52 % (928002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (928002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (928002)CaDiCaL version: 2.1.3
% 144.00/31.52 % (928002)Termination reason: Refutation not found, incomplete strategy
% 144.00/31.52 % (928002)Time elapsed: 0.596 s
% 144.00/31.52 % (928002)Peak memory usage: 132 MB
% 144.00/31.52 % (928002)Instructions burned: 898 (million)
% 144.00/31.52 % (928002)------------------------------
% 144.00/31.52 % (928002)------------------------------
% 144.00/31.52 % (927998)Instruction limit reached!
% 144.00/31.52 % (927998)------------------------------
% 144.00/31.52 % (927998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.00/31.52 % (927998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.00/31.52 % (927998)CaDiCaL version: 2.1.3
% 144.00/31.52 % (927998)Termination reason: Instruction limit
% 144.00/31.52 % (927998)Termination phase: Saturation
% 144.00/31.52 % (927998)Time elapsed: 4.256 s
% 144.00/31.52 % (927998)Peak memory usage: 195 MB
% 144.00/31.52 % (927998)Instructions burned: 6996 (million)
% 144.00/31.52 % (928006)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=2865766968:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2709 on theBenchmark for (2709ds/13494Mi)
% 144.00/31.52 % (928007)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=2880676856:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2708 on theBenchmark for (2708ds/2503Mi)
% 144.00/31.52 % (928007)First to succeed.
% 144.00/31.52 % (928007)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-927869"
% 144.00/31.52 % (928007)Refutation found. Thanks to Tanya!
% 144.00/31.52 % SZS status Theorem for theBenchmark
% 144.00/31.52 % SZS output start Proof for theBenchmark
% See solution above
% 216.99/31.72 % (928007)------------------------------
% 216.99/31.72 % (928007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.99/31.72 % (928007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.99/31.72 % (928007)CaDiCaL version: 2.1.3
% 216.99/31.72 % (928007)Termination reason: Refutation
% 216.99/31.72 % (928007)Time elapsed: 1.074 s
% 216.99/31.72 % (928007)Peak memory usage: 139 MB
% 216.99/31.72 % (928007)Instructions burned: 1662 (million)
% 216.99/31.72 % (928007)------------------------------
% 216.99/31.72 % (928007)------------------------------
% 216.99/31.72 % (927869)Success in time 30.679 s
% 216.99/31.72 % Vampire exiting
%------------------------------------------------------------------------------