%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX052+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 01:45:46 PM UTC 2026
% Result : Theorem 11.72s 2.85s
% Output : Refutation 15.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 24
% Syntax : Number of formulae : 171 ( 23 unt; 13 def)
% Number of atoms : 589 ( 186 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 667 ( 249 ~; 339 |; 54 &)
% ( 11 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 11 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 10 con; 0-2 aty)
% Number of variables : 225 ( 0 sgn 187 !; 38 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : '0' != s(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id2) ).
fof(f73,axiom,
! [X0] :
( list_succeeds(X0)
<=> ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2) )
| X0 = nil ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id73) ).
fof(f257,axiom,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
& list_succeeds(X2) )
=> list_succeeds(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom-(delete:types:2)') ).
fof(f274,axiom,
! [X0,X1] :
( permutation_succeeds(X0,X1)
=> ( list_succeeds(X0)
& list_succeeds(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(permutation:types)') ).
fof(f286,axiom,
! [X0] : occ(X0,nil) = '0',
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:nil)') ).
fof(f287,axiom,
! [X0,X1,X2] :
( ( list_succeeds(X2)
& X0 != X1 )
=> occ(X0,cons(X1,X2)) = occ(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:cons:diff)') ).
fof(f288,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> occ(X0,cons(X0,X1)) = s(occ(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:cons:eq)') ).
fof(f291,axiom,
! [X0,X1,X2,X3] :
( ( list_succeeds(X2)
& delete_succeeds(X0,X2,X3)
& X0 != X1 )
=> occ(X1,X2) = occ(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(delete:occ:diff)') ).
fof(f292,axiom,
! [X0,X1,X2] :
( ( list_succeeds(X1)
& delete_succeeds(X0,X1,X2) )
=> occ(X0,X1) = s(occ(X0,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(delete:occ:eq)') ).
fof(f293,axiom,
( ! [X0,X1] :
( ( ? [X2,X3,X4] :
( X1 = cons(X2,X3)
& delete_succeeds(X2,X0,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( X0 = nil
& X1 = nil ) )
=> ! [X5] : occ(X5,X0) = occ(X5,X1) )
=> ! [X0,X1] :
( permutation_succeeds(X0,X1)
=> ! [X5] : occ(X5,X0) = occ(X5,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',induction) ).
fof(f294,conjecture,
! [X0,X1] :
( permutation_succeeds(X0,X1)
=> ! [X2] : occ(X2,X0) = occ(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','theorem-(permutation:occ)') ).
fof(f295,negated_conjecture,
~ ! [X0,X1] :
( permutation_succeeds(X0,X1)
=> ! [X2] : occ(X2,X0) = occ(X2,X1) ),
inference(negated_conjecture,[status(cth)],[f294]) ).
fof(f320,plain,
( ! [X0,X1] :
( ( ? [X2,X3,X4] :
( X1 = cons(X2,X3)
& delete_succeeds(X2,X0,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( X0 = nil
& X1 = nil ) )
=> ! [X6] : occ(X6,X0) = occ(X6,X1) )
=> ! [X7,X8] :
( permutation_succeeds(X7,X8)
=> ! [X9] : occ(X9,X7) = occ(X9,X8) ) ),
inference(rectify,[],[f293]) ).
fof(f618,plain,
! [X0,X1,X2] :
( list_succeeds(X1)
| ~ delete_succeeds(X0,X1,X2)
| ~ list_succeeds(X2) ),
inference(ennf_transformation,[],[f257]) ).
fof(f619,plain,
! [X0,X1,X2] :
( list_succeeds(X1)
| ~ delete_succeeds(X0,X1,X2)
| ~ list_succeeds(X2) ),
inference(flattening,[],[f618]) ).
fof(f643,plain,
! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1) )
| ~ permutation_succeeds(X0,X1) ),
inference(ennf_transformation,[],[f274]) ).
fof(f662,plain,
! [X0,X1,X2] :
( occ(X0,cons(X1,X2)) = occ(X0,X2)
| ~ list_succeeds(X2)
| X0 = X1 ),
inference(ennf_transformation,[],[f287]) ).
fof(f663,plain,
! [X0,X1,X2] :
( occ(X0,cons(X1,X2)) = occ(X0,X2)
| ~ list_succeeds(X2)
| X0 = X1 ),
inference(flattening,[],[f662]) ).
fof(f664,plain,
! [X0,X1] :
( occ(X0,cons(X0,X1)) = s(occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f288]) ).
fof(f668,plain,
! [X0,X1,X2,X3] :
( occ(X1,X2) = occ(X1,X3)
| ~ list_succeeds(X2)
| ~ delete_succeeds(X0,X2,X3)
| X0 = X1 ),
inference(ennf_transformation,[],[f291]) ).
fof(f669,plain,
! [X0,X1,X2,X3] :
( occ(X1,X2) = occ(X1,X3)
| ~ list_succeeds(X2)
| ~ delete_succeeds(X0,X2,X3)
| X0 = X1 ),
inference(flattening,[],[f668]) ).
fof(f670,plain,
! [X0,X1,X2] :
( occ(X0,X1) = s(occ(X0,X2))
| ~ list_succeeds(X1)
| ~ delete_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f292]) ).
fof(f671,plain,
! [X0,X1,X2] :
( occ(X0,X1) = s(occ(X0,X2))
| ~ list_succeeds(X1)
| ~ delete_succeeds(X0,X1,X2) ),
inference(flattening,[],[f670]) ).
fof(f672,plain,
( ! [X7,X8] :
( ! [X9] : occ(X9,X7) = occ(X9,X8)
| ~ permutation_succeeds(X7,X8) )
| ? [X0,X1] :
( ? [X6] : occ(X6,X0) != occ(X6,X1)
& ( ? [X2,X3,X4] :
( X1 = cons(X2,X3)
& delete_succeeds(X2,X0,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( X0 = nil
& X1 = nil ) ) ) ),
inference(ennf_transformation,[],[f320]) ).
fof(f673,plain,
? [X0,X1] :
( ? [X2] : occ(X2,X0) != occ(X2,X1)
& permutation_succeeds(X0,X1) ),
inference(ennf_transformation,[],[f295]) ).
fof(f684,definition,
! [X1,X0] :
( ? [X2,X3,X4] :
( X1 = cons(X2,X3)
& delete_succeeds(X2,X0,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( X0 = nil
& X1 = nil )
| ~ sP6(X1,X0) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f685,plain,
( ! [X7,X8] :
( ! [X9] : occ(X9,X7) = occ(X9,X8)
| ~ permutation_succeeds(X7,X8) )
| ? [X0,X1] :
( ? [X6] : occ(X6,X0) != occ(X6,X1)
& sP6(X1,X0) ) ),
inference(definition_folding,[],[f672,f684]) ).
fof(f787,plain,
! [X0] :
( ( list_succeeds(X0)
| ( ! [X1,X2] :
( cons(X1,X2) != X0
| ~ list_succeeds(X2) )
& nil != X0 ) )
& ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2) )
| X0 = nil
| ~ list_succeeds(X0) ) ),
inference(nnf_transformation,[],[f73]) ).
fof(f788,plain,
! [X0] :
( ( list_succeeds(X0)
| ( ! [X1,X2] :
( cons(X1,X2) != X0
| ~ list_succeeds(X2) )
& nil != X0 ) )
& ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2) )
| X0 = nil
| ~ list_succeeds(X0) ) ),
inference(flattening,[],[f787]) ).
fof(f789,plain,
! [X0] :
( ( list_succeeds(X0)
| ( ! [X1,X2] :
( cons(X1,X2) != X0
| ~ list_succeeds(X2) )
& nil != X0 ) )
& ( ? [X3,X4] :
( cons(X3,X4) = X0
& list_succeeds(X4) )
| X0 = nil
| ~ list_succeeds(X0) ) ),
inference(rectify,[],[f788]) ).
fof(f790,plain,
! [X0] :
( ( list_succeeds(X0)
| ( ! [X1,X2] :
( cons(X1,X2) != X0
| ~ list_succeeds(X2) )
& nil != X0 ) )
& ( ( cons(sK72(X0),sK73(X0)) = X0
& list_succeeds(sK73(X0)) )
| X0 = nil
| ~ list_succeeds(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK72,sK73]),skolemize(X3,sK72(X0)),skolemize(X4,sK73(X0))],[f789]) ).
fof(f887,plain,
! [X1,X0] :
( ? [X2,X3,X4] :
( X1 = cons(X2,X3)
& delete_succeeds(X2,X0,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( X0 = nil
& X1 = nil )
| ~ sP6(X1,X0) ),
inference(nnf_transformation,[],[f684]) ).
fof(f888,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( cons(X2,X3) = X0
& delete_succeeds(X2,X1,X4)
& permutation_succeeds(X4,X3)
& ! [X5] : occ(X5,X4) = occ(X5,X3) )
| ( nil = X1
& nil = X0 )
| ~ sP6(X0,X1) ),
inference(rectify,[],[f887]) ).
fof(f889,plain,
! [X0,X1] :
( ( cons(sK131(X0,X1),sK132(X0,X1)) = X0
& delete_succeeds(sK131(X0,X1),X1,sK133(X0,X1))
& permutation_succeeds(sK133(X0,X1),sK132(X0,X1))
& ! [X5] : occ(X5,sK133(X0,X1)) = occ(X5,sK132(X0,X1)) )
| ( nil = X1
& nil = X0 )
| ~ sP6(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK131,sK132,sK133]),skolemize(X2,sK131(X0,X1)),skolemize(X3,sK132(X0,X1)),skolemize(X4,sK133(X0,X1))],[f888]) ).
fof(f890,plain,
( ! [X0,X1] :
( ! [X2] : occ(X2,X0) = occ(X2,X1)
| ~ permutation_succeeds(X0,X1) )
| ? [X3,X4] :
( ? [X5] : occ(X5,X4) != occ(X5,X3)
& sP6(X4,X3) ) ),
inference(rectify,[],[f685]) ).
fof(f891,plain,
( ! [X0,X1] :
( ! [X2] : occ(X2,X0) = occ(X2,X1)
| ~ permutation_succeeds(X0,X1) )
| ( occ(sK136,sK135) != occ(sK136,sK134)
& sP6(sK135,sK134) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK134,sK135,sK136]),skolemize(X3,sK134),skolemize(X4,sK135),skolemize(X5,sK136)],[f890]) ).
fof(f892,plain,
( occ(sK139,sK137) != occ(sK139,sK138)
& permutation_succeeds(sK137,sK138) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK137,sK138,sK139]),skolemize(X0,sK137),skolemize(X1,sK138),skolemize(X2,sK139)],[f673]) ).
fof(f894,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[],[f2]) ).
fof(f1108,plain,
! [X0] :
( list_succeeds(X0)
| nil != X0 ),
inference(cnf_transformation,[],[f790]) ).
fof(f1385,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| list_succeeds(X1)
| ~ list_succeeds(X2) ),
inference(cnf_transformation,[],[f619]) ).
fof(f1413,plain,
! [X0,X1] :
( ~ permutation_succeeds(X0,X1)
| list_succeeds(X1) ),
inference(cnf_transformation,[],[f643]) ).
fof(f1414,plain,
! [X0,X1] :
( ~ permutation_succeeds(X0,X1)
| list_succeeds(X0) ),
inference(cnf_transformation,[],[f643]) ).
fof(f1427,plain,
! [X0] : '0' = occ(X0,nil),
inference(cnf_transformation,[],[f286]) ).
fof(f1428,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X2)
| occ(X0,cons(X1,X2)) = occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f663]) ).
fof(f1429,plain,
! [X0,X1] :
( ~ list_succeeds(X1)
| occ(X0,cons(X0,X1)) = s(occ(X0,X1)) ),
inference(cnf_transformation,[],[f664]) ).
fof(f1432,plain,
! [X2,X3,X0,X1] :
( ~ delete_succeeds(X0,X2,X3)
| ~ list_succeeds(X2)
| occ(X1,X2) = occ(X1,X3)
| X0 = X1 ),
inference(cnf_transformation,[],[f669]) ).
fof(f1433,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| ~ list_succeeds(X1)
| occ(X0,X1) = s(occ(X0,X2)) ),
inference(cnf_transformation,[],[f671]) ).
fof(f1434,plain,
! [X0,X1,X5] :
( ~ sP6(X0,X1)
| nil = X0
| occ(X5,sK133(X0,X1)) = occ(X5,sK132(X0,X1)) ),
inference(cnf_transformation,[],[f889]) ).
fof(f1435,plain,
! [X0,X1,X5] :
( ~ sP6(X0,X1)
| nil = X1
| occ(X5,sK133(X0,X1)) = occ(X5,sK132(X0,X1)) ),
inference(cnf_transformation,[],[f889]) ).
fof(f1437,plain,
! [X0,X1] :
( permutation_succeeds(sK133(X0,X1),sK132(X0,X1))
| nil = X1
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f889]) ).
fof(f1438,plain,
! [X0,X1] :
( delete_succeeds(sK131(X0,X1),X1,sK133(X0,X1))
| nil = X0
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f889]) ).
fof(f1439,plain,
! [X0,X1] :
( delete_succeeds(sK131(X0,X1),X1,sK133(X0,X1))
| nil = X1
| ~ sP6(X0,X1) ),
inference(cnf_transformation,[],[f889]) ).
fof(f1441,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| nil = X1
| cons(sK131(X0,X1),sK132(X0,X1)) = X0 ),
inference(cnf_transformation,[],[f889]) ).
fof(f1442,plain,
! [X2,X0,X1] :
( occ(X2,X0) = occ(X2,X1)
| ~ permutation_succeeds(X0,X1)
| sP6(sK135,sK134) ),
inference(cnf_transformation,[],[f891]) ).
fof(f1443,plain,
! [X2,X0,X1] :
( occ(X2,X0) = occ(X2,X1)
| ~ permutation_succeeds(X0,X1)
| occ(sK136,sK135) != occ(sK136,sK134) ),
inference(cnf_transformation,[],[f891]) ).
fof(f1444,plain,
permutation_succeeds(sK137,sK138),
inference(cnf_transformation,[],[f892]) ).
fof(f1445,plain,
occ(sK139,sK137) != occ(sK139,sK138),
inference(cnf_transformation,[],[f892]) ).
fof(f1503,plain,
list_succeeds(nil),
inference(equality_resolution,[],[f1108]) ).
fof(f1561,definition,
sF140 = occ(sK139,sK137),
introduced(definition,[new_symbols(definition,[sF140])],[function_definition]) ).
fof(f1562,plain,
occ(sK139,sK137) = sF140,
inference(reorient_equations,[],[f1561]) ).
fof(f1563,definition,
sF141 = occ(sK139,sK138),
introduced(definition,[new_symbols(definition,[sF141])],[function_definition]) ).
fof(f1564,plain,
occ(sK139,sK138) = sF141,
inference(reorient_equations,[],[f1563]) ).
fof(f1565,plain,
sF140 != sF141,
inference(definition_folding,[],[f1445,f1564,f1562]) ).
fof(f1567,definition,
( spl142_1
<=> sP6(sK135,sK134) ),
introduced(definition,[new_symbols(definition,[spl142_1])],[avatar_definition]) ).
fof(f1569,plain,
( sP6(sK135,sK134)
| ~ spl142_1 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1571,definition,
( spl142_2
<=> ! [X2,X0,X1] :
( occ(X2,X0) = occ(X2,X1)
| ~ permutation_succeeds(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl142_2])],[avatar_definition]) ).
fof(f1572,plain,
( ! [X2,X0,X1] :
( ~ permutation_succeeds(X0,X1)
| occ(X2,X0) = occ(X2,X1) )
| ~ spl142_2 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1573,plain,
( spl142_1
| spl142_2 ),
inference(avatar_split_clause,[],[f1442,f1571,f1567]) ).
fof(f1575,definition,
( spl142_3
<=> occ(sK136,sK135) = occ(sK136,sK134) ),
introduced(definition,[new_symbols(definition,[spl142_3])],[avatar_definition]) ).
fof(f1577,plain,
( occ(sK136,sK135) != occ(sK136,sK134)
| spl142_3 ),
inference(avatar_component_clause,[],[f1575]) ).
fof(f1578,plain,
( ~ spl142_3
| spl142_2 ),
inference(avatar_split_clause,[],[f1443,f1571,f1575]) ).
fof(f1580,plain,
( ! [X0] : occ(X0,sK137) = occ(X0,sK138)
| ~ spl142_2 ),
inference(resolution,[],[f1572,f1444]) ).
fof(f1581,plain,
( occ(sK139,sK137) = sF141
| ~ spl142_2 ),
inference(superposition,[],[f1580,f1564]) ).
fof(f1584,plain,
( sF140 = sF141
| ~ spl142_2 ),
inference(forward_demodulation,[],[f1581,f1562]) ).
fof(f1587,plain,
( $false
| ~ spl142_2 ),
inference(forward_subsumption_resolution,[],[f1584,f1565]) ).
fof(f1588,plain,
~ spl142_2,
inference(avatar_contradiction_clause,[],[f1587]) ).
fof(f1592,plain,
( ! [X0] :
( nil = sK134
| occ(X0,sK133(sK135,sK134)) = occ(X0,sK132(sK135,sK134)) )
| ~ spl142_1 ),
inference(resolution,[],[f1435,f1569]) ).
fof(f1594,definition,
( spl142_4
<=> ! [X0] : occ(X0,sK133(sK135,sK134)) = occ(X0,sK132(sK135,sK134)) ),
introduced(definition,[new_symbols(definition,[spl142_4])],[avatar_definition]) ).
fof(f1595,plain,
( ! [X0] : occ(X0,sK133(sK135,sK134)) = occ(X0,sK132(sK135,sK134))
| ~ spl142_4 ),
inference(avatar_component_clause,[],[f1594]) ).
fof(f1597,definition,
( spl142_5
<=> nil = sK134 ),
introduced(definition,[new_symbols(definition,[spl142_5])],[avatar_definition]) ).
fof(f1598,plain,
( nil != sK134
| spl142_5 ),
inference(avatar_component_clause,[],[f1597]) ).
fof(f1599,plain,
( nil = sK134
| ~ spl142_5 ),
inference(avatar_component_clause,[],[f1597]) ).
fof(f1600,plain,
( spl142_4
| spl142_5
| ~ spl142_1 ),
inference(avatar_split_clause,[],[f1592,f1567,f1597,f1594]) ).
fof(f1601,plain,
( sP6(sK135,nil)
| ~ spl142_1
| ~ spl142_5 ),
inference(superposition,[],[f1569,f1599]) ).
fof(f1603,plain,
( ! [X0] :
( nil = sK135
| occ(X0,sK133(sK135,sK134)) = occ(X0,sK132(sK135,sK134)) )
| ~ spl142_1 ),
inference(resolution,[],[f1434,f1569]) ).
fof(f1606,definition,
( spl142_6
<=> ! [X0] : occ(X0,sK133(sK135,nil)) = occ(X0,sK132(sK135,nil)) ),
introduced(definition,[new_symbols(definition,[spl142_6])],[avatar_definition]) ).
fof(f1607,plain,
( ! [X0] : occ(X0,sK133(sK135,nil)) = occ(X0,sK132(sK135,nil))
| ~ spl142_6 ),
inference(avatar_component_clause,[],[f1606]) ).
fof(f1609,definition,
( spl142_7
<=> nil = sK135 ),
introduced(definition,[new_symbols(definition,[spl142_7])],[avatar_definition]) ).
fof(f1610,plain,
( nil != sK135
| spl142_7 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1611,plain,
( nil = sK135
| ~ spl142_7 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1613,plain,
( ! [X0] :
( occ(X0,sK133(sK135,nil)) = occ(X0,sK132(sK135,nil))
| nil = sK135 )
| ~ spl142_1
| ~ spl142_5 ),
inference(forward_demodulation,[],[f1603,f1599]) ).
fof(f1614,plain,
( spl142_7
| spl142_6
| ~ spl142_1
| ~ spl142_5 ),
inference(avatar_split_clause,[],[f1613,f1597,f1567,f1606,f1609]) ).
fof(f1633,plain,
( nil = sK134
| sK135 = cons(sK131(sK135,sK134),sK132(sK135,sK134))
| ~ spl142_1 ),
inference(resolution,[],[f1441,f1569]) ).
fof(f1647,plain,
( occ(sK136,sK134) != occ(sK136,nil)
| spl142_3
| ~ spl142_7 ),
inference(superposition,[],[f1577,f1611]) ).
fof(f1648,plain,
( '0' != occ(sK136,sK134)
| spl142_3
| ~ spl142_7 ),
inference(forward_demodulation,[],[f1647,f1427]) ).
fof(f1650,plain,
( '0' != occ(sK136,nil)
| spl142_3
| ~ spl142_5
| ~ spl142_7 ),
inference(forward_demodulation,[],[f1648,f1599]) ).
fof(f1651,plain,
( $false
| spl142_3
| ~ spl142_5
| ~ spl142_7 ),
inference(forward_subsumption_resolution,[],[f1650,f1427]) ).
fof(f1652,plain,
( spl142_3
| ~ spl142_5
| ~ spl142_7 ),
inference(avatar_contradiction_clause,[],[f1651]) ).
fof(f1654,plain,
( sK135 = cons(sK131(sK135,sK134),sK132(sK135,sK134))
| ~ spl142_1
| spl142_5 ),
inference(forward_subsumption_resolution,[],[f1633,f1598]) ).
fof(f1686,plain,
! [X0,X1] :
( list_succeeds(sK133(X1,X0))
| ~ sP6(X1,X0)
| nil = X0 ),
inference(resolution,[],[f1437,f1414]) ).
fof(f1687,plain,
! [X0,X1] :
( list_succeeds(sK132(X1,X0))
| ~ sP6(X1,X0)
| nil = X0 ),
inference(resolution,[],[f1437,f1413]) ).
fof(f1751,plain,
! [X2,X0,X1] :
( ~ sP6(X1,X0)
| nil = X0
| ~ list_succeeds(X0)
| occ(X2,X0) = occ(X2,sK133(X1,X0))
| sK131(X1,X0) = X2 ),
inference(resolution,[],[f1439,f1432]) ).
fof(f1752,plain,
( ! [X0] :
( nil = sK134
| ~ list_succeeds(sK134)
| occ(X0,sK133(sK135,sK134)) = occ(X0,sK134)
| sK131(sK135,sK134) = X0 )
| ~ spl142_1 ),
inference(resolution,[],[f1751,f1569]) ).
fof(f1753,plain,
( ! [X0] :
( ~ list_succeeds(sK134)
| occ(X0,sK133(sK135,sK134)) = occ(X0,sK134)
| sK131(sK135,sK134) = X0 )
| ~ spl142_1
| spl142_5 ),
inference(forward_subsumption_resolution,[],[f1752,f1598]) ).
fof(f1754,plain,
( ! [X0] :
( occ(X0,sK132(sK135,sK134)) = occ(X0,sK134)
| ~ list_succeeds(sK134)
| sK131(sK135,sK134) = X0 )
| ~ spl142_1
| ~ spl142_4
| spl142_5 ),
inference(forward_demodulation,[],[f1753,f1595]) ).
fof(f1756,definition,
( spl142_15
<=> list_succeeds(sK134) ),
introduced(definition,[new_symbols(definition,[spl142_15])],[avatar_definition]) ).
fof(f1757,plain,
( list_succeeds(sK134)
| ~ spl142_15 ),
inference(avatar_component_clause,[],[f1756]) ).
fof(f1758,plain,
( ~ list_succeeds(sK134)
| spl142_15 ),
inference(avatar_component_clause,[],[f1756]) ).
fof(f1760,definition,
( spl142_16
<=> ! [X0] :
( occ(X0,sK132(sK135,sK134)) = occ(X0,sK134)
| sK131(sK135,sK134) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl142_16])],[avatar_definition]) ).
fof(f1761,plain,
( ! [X0] :
( occ(X0,sK132(sK135,sK134)) = occ(X0,sK134)
| sK131(sK135,sK134) = X0 )
| ~ spl142_16 ),
inference(avatar_component_clause,[],[f1760]) ).
fof(f1762,plain,
( ~ spl142_15
| spl142_16
| ~ spl142_1
| ~ spl142_4
| spl142_5 ),
inference(avatar_split_clause,[],[f1754,f1597,f1594,f1567,f1760,f1756]) ).
fof(f1803,plain,
! [X0,X1] :
( ~ sP6(X0,X1)
| nil = X0
| ~ list_succeeds(X1)
| occ(sK131(X0,X1),X1) = s(occ(sK131(X0,X1),sK133(X0,X1))) ),
inference(resolution,[],[f1438,f1433]) ).
fof(f1822,definition,
( spl142_20
<=> list_succeeds(sK132(sK135,sK134)) ),
introduced(definition,[new_symbols(definition,[spl142_20])],[avatar_definition]) ).
fof(f1823,plain,
( ~ list_succeeds(sK132(sK135,sK134))
| spl142_20 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1824,plain,
( list_succeeds(sK132(sK135,sK134))
| ~ spl142_20 ),
inference(avatar_component_clause,[],[f1822]) ).
fof(f1886,plain,
! [X0,X1] :
( list_succeeds(X0)
| ~ list_succeeds(sK133(X1,X0))
| nil = X0
| ~ sP6(X1,X0) ),
inference(resolution,[],[f1385,f1439]) ).
fof(f1887,plain,
! [X0,X1] :
( ~ sP6(X1,X0)
| nil = X0
| list_succeeds(X0) ),
inference(forward_subsumption_resolution,[],[f1886,f1686]) ).
fof(f1889,plain,
( nil = sK134
| list_succeeds(sK134)
| ~ spl142_1 ),
inference(resolution,[],[f1887,f1569]) ).
fof(f1890,plain,
( list_succeeds(sK134)
| ~ spl142_1
| spl142_5 ),
inference(forward_subsumption_resolution,[],[f1889,f1598]) ).
fof(f1891,plain,
( $false
| ~ spl142_1
| spl142_5
| spl142_15 ),
inference(forward_subsumption_resolution,[],[f1890,f1758]) ).
fof(f1892,plain,
( ~ spl142_1
| spl142_5
| spl142_15 ),
inference(avatar_contradiction_clause,[],[f1891]) ).
fof(f1916,plain,
( ~ sP6(sK135,sK134)
| nil = sK134
| spl142_20 ),
inference(resolution,[],[f1823,f1687]) ).
fof(f1917,plain,
( nil = sK134
| ~ spl142_1
| spl142_20 ),
inference(forward_subsumption_resolution,[],[f1916,f1569]) ).
fof(f1919,plain,
( $false
| ~ spl142_1
| spl142_5
| spl142_20 ),
inference(forward_subsumption_resolution,[],[f1917,f1598]) ).
fof(f1920,plain,
( ~ spl142_1
| spl142_5
| spl142_20 ),
inference(avatar_contradiction_clause,[],[f1919]) ).
fof(f1928,plain,
( ! [X0,X1] :
( occ(X0,sK132(sK135,sK134)) = occ(X0,cons(X1,sK132(sK135,sK134)))
| X0 = X1 )
| ~ spl142_20 ),
inference(resolution,[],[f1824,f1428]) ).
fof(f1929,plain,
( ! [X0] : s(occ(X0,sK132(sK135,sK134))) = occ(X0,cons(X0,sK132(sK135,sK134)))
| ~ spl142_20 ),
inference(resolution,[],[f1824,f1429]) ).
fof(f1934,plain,
( ! [X0] :
( occ(X0,sK132(sK135,sK134)) = occ(X0,sK135)
| sK131(sK135,sK134) = X0 )
| ~ spl142_1
| spl142_5
| ~ spl142_20 ),
inference(superposition,[],[f1928,f1654]) ).
fof(f1938,plain,
( ! [X0] :
( occ(X0,sK134) = occ(X0,sK135)
| sK131(sK135,sK134) = X0
| sK131(sK135,sK134) = X0 )
| ~ spl142_1
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(superposition,[],[f1761,f1934]) ).
fof(f1942,plain,
( ! [X0] :
( occ(X0,sK134) = occ(X0,sK135)
| sK131(sK135,sK134) = X0 )
| ~ spl142_1
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(duplicate_literal_removal,[],[f1938]) ).
fof(f1946,plain,
( occ(sK136,sK134) != occ(sK136,sK134)
| sK136 = sK131(sK135,sK134)
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(superposition,[],[f1577,f1942]) ).
fof(f1949,plain,
( sK136 = sK131(sK135,sK134)
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(trivial_inequality_removal,[],[f1946]) ).
fof(f1950,plain,
( sK135 = cons(sK136,sK132(sK135,sK134))
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(superposition,[],[f1654,f1949]) ).
fof(f1952,plain,
( delete_succeeds(sK136,sK134,sK133(sK135,sK134))
| nil = sK134
| ~ sP6(sK135,sK134)
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(superposition,[],[f1439,f1949]) ).
fof(f1953,plain,
( delete_succeeds(sK136,sK134,sK133(sK135,sK134))
| ~ sP6(sK135,sK134)
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_subsumption_resolution,[],[f1952,f1598]) ).
fof(f1955,plain,
( delete_succeeds(sK136,sK134,sK133(sK135,sK134))
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_subsumption_resolution,[],[f1953,f1569]) ).
fof(f1960,plain,
( ~ list_succeeds(sK134)
| occ(sK136,sK134) = s(occ(sK136,sK133(sK135,sK134)))
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(resolution,[],[f1955,f1433]) ).
fof(f1963,plain,
( occ(sK136,sK134) = s(occ(sK136,sK133(sK135,sK134)))
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_subsumption_resolution,[],[f1960,f1757]) ).
fof(f1965,plain,
( occ(sK136,sK134) = s(occ(sK136,sK132(sK135,sK134)))
| ~ spl142_1
| spl142_3
| ~ spl142_4
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_demodulation,[],[f1963,f1595]) ).
fof(f1978,plain,
( occ(sK136,sK135) = s(occ(sK136,sK132(sK135,sK134)))
| ~ spl142_1
| spl142_3
| spl142_5
| ~ spl142_16
| ~ spl142_20 ),
inference(superposition,[],[f1929,f1950]) ).
fof(f1986,plain,
( occ(sK136,sK135) = occ(sK136,sK134)
| ~ spl142_1
| spl142_3
| ~ spl142_4
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_demodulation,[],[f1978,f1965]) ).
fof(f1987,plain,
( $false
| ~ spl142_1
| spl142_3
| ~ spl142_4
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(forward_subsumption_resolution,[],[f1986,f1577]) ).
fof(f1988,plain,
( ~ spl142_1
| spl142_3
| ~ spl142_4
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(avatar_contradiction_clause,[],[f1987]) ).
fof(f2616,plain,
( nil = sK135
| ~ list_succeeds(nil)
| occ(sK131(sK135,nil),nil) = s(occ(sK131(sK135,nil),sK133(sK135,nil)))
| ~ spl142_1
| ~ spl142_5 ),
inference(resolution,[],[f1803,f1601]) ).
fof(f2617,plain,
( ~ list_succeeds(nil)
| occ(sK131(sK135,nil),nil) = s(occ(sK131(sK135,nil),sK133(sK135,nil)))
| ~ spl142_1
| ~ spl142_5
| spl142_7 ),
inference(forward_subsumption_resolution,[],[f2616,f1610]) ).
fof(f2619,plain,
( occ(sK131(sK135,nil),nil) = s(occ(sK131(sK135,nil),sK133(sK135,nil)))
| ~ spl142_1
| ~ spl142_5
| spl142_7 ),
inference(forward_subsumption_resolution,[],[f2617,f1503]) ).
fof(f2621,plain,
( s(occ(sK131(sK135,nil),sK132(sK135,nil))) = occ(sK131(sK135,nil),nil)
| ~ spl142_1
| ~ spl142_5
| ~ spl142_6
| spl142_7 ),
inference(forward_demodulation,[],[f2619,f1607]) ).
fof(f2623,plain,
( '0' = s(occ(sK131(sK135,nil),sK132(sK135,nil)))
| ~ spl142_1
| ~ spl142_5
| ~ spl142_6
| spl142_7 ),
inference(forward_demodulation,[],[f2621,f1427]) ).
fof(f2625,plain,
( $false
| ~ spl142_1
| ~ spl142_5
| ~ spl142_6
| spl142_7 ),
inference(forward_subsumption_resolution,[],[f2623,f894]) ).
fof(f2626,plain,
( ~ spl142_1
| ~ spl142_5
| ~ spl142_6
| spl142_7 ),
inference(avatar_contradiction_clause,[],[f2625]) ).
cnf(s1,plain,
( spl142_1
| spl142_2 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s2,plain,
( spl142_2
| ~ spl142_3 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s4,plain,
~ spl142_2,
inference(sat_conversion,[],[f1588]) ).
cnf(s5,plain,
( ~ spl142_1
| spl142_4
| spl142_5 ),
inference(sat_conversion,[],[f1600]) ).
cnf(s7,plain,
( ~ spl142_1
| ~ spl142_5
| spl142_6
| spl142_7 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s11,plain,
( spl142_3
| ~ spl142_5
| ~ spl142_7 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s17,plain,
( ~ spl142_1
| ~ spl142_4
| spl142_5
| ~ spl142_15
| spl142_16 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s21,plain,
( ~ spl142_1
| spl142_5
| spl142_15 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s24,plain,
( ~ spl142_1
| spl142_5
| spl142_20 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s26,plain,
( ~ spl142_1
| spl142_3
| ~ spl142_4
| spl142_5
| ~ spl142_15
| ~ spl142_16
| ~ spl142_20 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s29,plain,
( ~ spl142_1
| ~ spl142_5
| ~ spl142_6
| spl142_7 ),
inference(sat_conversion,[],[f2626]) ).
cnf(s32,plain,
~ spl142_3,
inference(rat,[],[s2,s4]) ).
cnf(s33,plain,
spl142_1,
inference(rat,[],[s1,s4]) ).
cnf(s34,plain,
( ~ spl142_5
| spl142_7 ),
inference(rat,[],[s29,s7,s33]) ).
cnf(s35,plain,
~ spl142_5,
inference(rat,[],[s34,s11,s32]) ).
cnf(s36,plain,
spl142_20,
inference(rat,[],[s24,s33,s35]) ).
cnf(s37,plain,
spl142_15,
inference(rat,[],[s21,s33,s35]) ).
cnf(s40,plain,
spl142_4,
inference(rat,[],[s5,s33,s35]) ).
cnf(s42,plain,
spl142_16,
inference(rat,[],[s17,s35,s37,s33,s40]) ).
cnf(s43,plain,
$false,
inference(rat,[],[s26,s36,s35,s37,s33,s32,s42,s40]) ).
fof(f2630,plain,
$false,
inference(avatar_sat_refutation,[],[s43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX052+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 % Computer : n014.cluster.edu
% 0.08/0.22 % Model : x86_64 x86_64
% 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.22 % Memory : 8046.5625MB
% 0.08/0.22 % OS : Linux 6.8.0-71-generic
% 0.08/0.22 % CPULimit : 300
% 0.08/0.22 % WCLimit : 300
% 0.08/0.22 % DateTime : Mon Sep 28 14:54:30 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.28 Running first-order theorem proving
% 0.25/0.28 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.72/2.85 % (1830056)Detected formulas, will run a generic FOF schedule.
% 11.72/2.85 % (1830067)dis-21_1_sil=8000:lcm=predicate:random_seed=3195811191: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.72/2.85 % (1830061)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=1417478134:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.72/2.85 % (1830062)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=644378023:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.72/2.85 % (1830064)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2865690879:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.72/2.85 % (1830065)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3311686835:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.72/2.85 % (1830063)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=2779947687:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.72/2.85 % (1830066)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=462164968:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.72/2.85 % (1830067)Instruction limit reached!
% 11.72/2.85 % (1830067)------------------------------
% 11.72/2.85 % (1830067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830067)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830067)Termination reason: Instruction limit
% 11.72/2.85 % (1830067)Termination phase: Saturation
% 11.72/2.85 % (1830067)Time elapsed: 0.066 s
% 11.72/2.85 % (1830067)Peak memory usage: 89 MB
% 11.72/2.85 % (1830067)Instructions burned: 129 (million)
% 11.72/2.85 % (1830064)Instruction limit reached!
% 11.72/2.85 % (1830064)------------------------------
% 11.72/2.85 % (1830064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830064)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830064)Termination reason: Instruction limit
% 11.72/2.85 % (1830064)Termination phase: Saturation
% 11.72/2.85 % (1830064)Time elapsed: 0.112 s
% 11.72/2.85 % (1830064)Peak memory usage: 89 MB
% 11.72/2.85 % (1830064)Instructions burned: 109 (million)
% 11.72/2.85 % (1830065)Instruction limit reached!
% 11.72/2.85 % (1830065)------------------------------
% 11.72/2.85 % (1830065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830065)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830065)Termination reason: Instruction limit
% 11.72/2.85 % (1830065)Termination phase: Saturation
% 11.72/2.85 % (1830065)Time elapsed: 0.119 s
% 11.72/2.85 % (1830065)Peak memory usage: 88 MB
% 11.72/2.85 % (1830065)Instructions burned: 120 (million)
% 11.72/2.85 % (1830066)Instruction limit reached!
% 11.72/2.85 % (1830066)------------------------------
% 11.72/2.85 % (1830066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830066)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830066)Termination reason: Instruction limit
% 11.72/2.85 % (1830066)Termination phase: Saturation
% 11.72/2.85 % (1830066)Time elapsed: 0.150 s
% 11.72/2.85 % (1830066)Peak memory usage: 90 MB
% 11.72/2.85 % (1830066)Instructions burned: 139 (million)
% 11.72/2.85 % (1830075)lrs+10_1_sil=8000:sp=occurrence:random_seed=2633765653:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.72/2.85 % (1830079)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2987615539:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 11.72/2.85 % (1830078)lrs+10_1_sil=32000:urr=on:br=off:random_seed=432013732:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 11.72/2.85 % (1830075)Instruction limit reached!
% 11.72/2.85 % (1830075)------------------------------
% 11.72/2.85 % (1830075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830075)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830075)Termination reason: Instruction limit
% 11.72/2.85 % (1830075)Termination phase: Saturation
% 11.72/2.85 % (1830075)Time elapsed: 0.160 s
% 11.72/2.85 % (1830075)Peak memory usage: 93 MB
% 11.72/2.85 % (1830075)Instructions burned: 286 (million)
% 11.72/2.85 % (1830078)Refutation not found, incomplete strategy
% 11.72/2.85 % (1830078)------------------------------
% 11.72/2.85 % (1830078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830078)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830078)Termination reason: Refutation not found, incomplete strategy
% 11.72/2.85 % (1830078)Time elapsed: 0.012 s
% 11.72/2.85 % (1830078)Peak memory usage: 89 MB
% 11.72/2.85 % (1830078)Instructions burned: 10 (million)
% 11.72/2.85 % (1830080)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=1566476216:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 11.72/2.85 % (1830084)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1441053907:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 11.72/2.85 % (1830079)Instruction limit reached!
% 11.72/2.85 % (1830079)------------------------------
% 11.72/2.85 % (1830079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830079)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830079)Termination reason: Instruction limit
% 11.72/2.85 % (1830079)Termination phase: Saturation
% 11.72/2.85 % (1830079)Time elapsed: 0.333 s
% 11.72/2.85 % (1830079)Peak memory usage: 91 MB
% 11.72/2.85 % (1830079)Instructions burned: 325 (million)
% 11.72/2.85 % (1830080)Instruction limit reached!
% 11.72/2.85 % (1830080)------------------------------
% 11.72/2.85 % (1830080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830080)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830080)Termination reason: Instruction limit
% 11.72/2.85 % (1830080)Termination phase: Saturation
% 11.72/2.85 % (1830080)Time elapsed: 0.239 s
% 11.72/2.85 % (1830080)Peak memory usage: 93 MB
% 11.72/2.85 % (1830080)Instructions burned: 248 (million)
% 11.72/2.85 % (1830084)Instruction limit reached!
% 11.72/2.85 % (1830084)------------------------------
% 11.72/2.85 % (1830084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830084)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830084)Termination reason: Instruction limit
% 11.72/2.85 % (1830084)Termination phase: Saturation
% 11.72/2.85 % (1830084)Time elapsed: 0.133 s
% 11.72/2.85 % (1830084)Peak memory usage: 89 MB
% 11.72/2.85 % (1830084)Instructions burned: 294 (million)
% 11.72/2.85 % (1830078)------------------------------
% 11.72/2.85 % (1830078)------------------------------
% 11.72/2.85 % (1830087)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3585161245:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 11.72/2.85 % (1830088)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1850156014:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 11.72/2.85 % (1830089)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=449236005:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 11.72/2.85 % (1830090)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=512533882:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 11.72/2.85 % (1830088)Instruction limit reached!
% 11.72/2.85 % (1830088)------------------------------
% 11.72/2.85 % (1830088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830088)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830088)Termination reason: Instruction limit
% 11.72/2.85 % (1830088)Termination phase: Saturation
% 11.72/2.85 % (1830088)Time elapsed: 0.118 s
% 11.72/2.85 % (1830088)Peak memory usage: 91 MB
% 11.72/2.85 % (1830088)Instructions burned: 113 (million)
% 11.72/2.85 % (1830090)Instruction limit reached!
% 11.72/2.85 % (1830090)------------------------------
% 11.72/2.85 % (1830090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830090)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830090)Termination reason: Instruction limit
% 11.72/2.85 % (1830090)Termination phase: Saturation
% 11.72/2.85 % (1830090)Time elapsed: 0.052 s
% 11.72/2.85 % (1830090)Peak memory usage: 89 MB
% 11.72/2.85 % (1830090)Instructions burned: 114 (million)
% 11.72/2.85 % (1830089)Instruction limit reached!
% 11.72/2.85 % (1830089)------------------------------
% 11.72/2.85 % (1830089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830089)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830089)Termination reason: Instruction limit
% 11.72/2.85 % (1830089)Termination phase: Saturation
% 11.72/2.85 % (1830089)Time elapsed: 0.113 s
% 11.72/2.85 % (1830089)Peak memory usage: 90 MB
% 11.72/2.85 % (1830089)Instructions burned: 128 (million)
% 11.72/2.85 % (1830098)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1112065134:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 11.72/2.85 % (1830097)lrs+10_1_sil=8000:sp=occurrence:random_seed=2209800914:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2986 on theBenchmark for (2986ds/907Mi)
% 11.72/2.85 % (1830061)First to succeed.
% 11.72/2.85 % (1830061)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1830056"
% 11.72/2.85 % (1830099)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2613366815:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 11.72/2.85 % (1830098)Instruction limit reached!
% 11.72/2.85 % (1830098)------------------------------
% 11.72/2.85 % (1830098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830098)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830098)Termination reason: Instruction limit
% 11.72/2.85 % (1830098)Termination phase: Saturation
% 11.72/2.85 % (1830098)Time elapsed: 0.203 s
% 11.72/2.85 % (1830098)Peak memory usage: 91 MB
% 11.72/2.85 % (1830098)Instructions burned: 437 (million)
% 11.72/2.85 % (1830062)Also succeeded, but the first one will report.
% 11.72/2.85 % (1830063)Also succeeded, but the first one will report.
% 11.72/2.85 % (1830105)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2281740504:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 11.72/2.85 % (1830105)Instruction limit reached!
% 11.72/2.85 % (1830105)------------------------------
% 11.72/2.85 % (1830105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.72/2.85 % (1830105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.72/2.85 % (1830105)CaDiCaL version: 2.1.3
% 11.72/2.85 % (1830105)Termination reason: Instruction limit
% 11.72/2.85 % (1830105)Termination phase: Saturation
% 11.72/2.85 % (1830105)Time elapsed: 0.068 s
% 11.72/2.85 % (1830105)Peak memory usage: 91 MB
% 11.72/2.85 % (1830105)Instructions burned: 134 (million)
% 11.72/2.85 % (1830061)Refutation found. Thanks to Tanya!
% 11.72/2.85 % SZS status Theorem for theBenchmark
% 11.72/2.85 % SZS output start Proof for theBenchmark
% See solution above
% 15.75/3.09 % (1830061)------------------------------
% 15.75/3.09 % (1830061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.75/3.09 % (1830061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/3.09 % (1830061)CaDiCaL version: 2.1.3
% 15.75/3.09 % (1830061)Termination reason: Refutation
% 15.75/3.09 % (1830061)Time elapsed: 1.405 s
% 15.75/3.09 % (1830061)Peak memory usage: 136 MB
% 15.75/3.09 % (1830061)Instructions burned: 1343 (million)
% 15.75/3.09 % (1830061)------------------------------
% 15.75/3.09 % (1830061)------------------------------
% 15.75/3.09 % (1830056)Success in time 2.142 s
% 15.75/3.09 % Vampire exiting
%------------------------------------------------------------------------------