%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX055+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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:45:46 PM UTC 2026
% Result : Theorem 17.91s 4.51s
% Output : Refutation 26.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 29
% Syntax : Number of formulae : 193 ( 35 unt; 14 def)
% Number of atoms : 509 ( 136 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 532 ( 216 ~; 212 |; 75 &)
% ( 19 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 7 con; 0-3 aty)
% Number of variables : 262 ( 0 sgn 226 !; 36 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1] :
( s(X0) = s(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id6) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( cons(X0,X1) = cons(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id8) ).
fof(f18,axiom,
! [X0,X1] :
~ ( not_same_occ_succeeds(X0,X1)
& not_same_occ_fails(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id18) ).
fof(f46,axiom,
! [X0,X1,X2] :
( member2_succeeds(X0,X1,X2)
<=> ( member_succeeds(X0,X2)
| member_succeeds(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id46) ).
fof(f52,axiom,
! [X0,X1] :
( not_same_occ_succeeds(X0,X1)
<=> ? [X2,X3,X4] :
( member2_succeeds(X2,X0,X1)
& occ_succeeds(X2,X0,X3)
& occ_succeeds(X2,X1,X4)
& X3 != X4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id52) ).
fof(f55,axiom,
! [X0,X1] :
( same_occ_succeeds(X0,X1)
<=> not_same_occ_fails(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id55) ).
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(f91,axiom,
! [X0] :
( nat_succeeds(X0)
<=> ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1) )
| X0 = '0' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id91) ).
fof(f187,axiom,
! [X0,X1] :
( list_succeeds(cons(X0,X1))
=> list_succeeds(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom-(list:cons)') ).
fof(f264,axiom,
! [X0,X1,X2] :
( delete_succeeds(X0,X1,X2)
=> member_succeeds(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom-(delete:member:2)') ).
fof(f273,axiom,
! [X0,X1,X2] :
( list_succeeds(X1)
=> ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','occ/2') ).
fof(f283,axiom,
! [X0,X1,X2] :
( occ_succeeds(X0,X1,X2)
=> ( list_succeeds(X1)
& nat_succeeds(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:types)') ).
fof(f289,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> nat_succeeds(occ(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','corollary-(occ:types)') ).
fof(f296,axiom,
! [X0,X1,X2] :
( ( list_succeeds(X1)
& occ(X0,X1) = s(X2) )
=> ? [X3] : delete_succeeds(X0,X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:successor)') ).
fof(f301,conjecture,
! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1)
& same_occ_succeeds(X0,X1) )
=> ! [X2] : occ(X2,X0) = occ(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(same_occ:success)') ).
fof(f302,negated_conjecture,
~ ! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1)
& same_occ_succeeds(X0,X1) )
=> ! [X2] : occ(X2,X0) = occ(X2,X1) ),
inference(negated_conjecture,[status(cth)],[f301]) ).
fof(f328,plain,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f329,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| cons(X0,X1) != cons(X2,X3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f337,plain,
! [X0,X1] :
( ~ not_same_occ_succeeds(X0,X1)
| ~ not_same_occ_fails(X0,X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f521,plain,
! [X0,X1] :
( list_succeeds(X1)
| ~ list_succeeds(cons(X0,X1)) ),
inference(ennf_transformation,[],[f187]) ).
fof(f637,plain,
! [X0,X1,X2] :
( member_succeeds(X0,X1)
| ~ delete_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f264]) ).
fof(f649,plain,
! [X0,X1,X2] :
( ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) )
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f273]) ).
fof(f665,plain,
! [X0,X1,X2] :
( ( list_succeeds(X1)
& nat_succeeds(X2) )
| ~ occ_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f283]) ).
fof(f672,plain,
! [X0,X1] :
( nat_succeeds(occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f289]) ).
fof(f684,plain,
! [X0,X1,X2] :
( ? [X3] : delete_succeeds(X0,X1,X3)
| ~ list_succeeds(X1)
| s(X2) != occ(X0,X1) ),
inference(ennf_transformation,[],[f296]) ).
fof(f685,plain,
! [X0,X1,X2] :
( ? [X3] : delete_succeeds(X0,X1,X3)
| ~ list_succeeds(X1)
| s(X2) != occ(X0,X1) ),
inference(flattening,[],[f684]) ).
fof(f694,plain,
? [X0,X1] :
( ? [X2] : occ(X2,X0) != occ(X2,X1)
& list_succeeds(X0)
& list_succeeds(X1)
& same_occ_succeeds(X0,X1) ),
inference(ennf_transformation,[],[f302]) ).
fof(f695,plain,
? [X0,X1] :
( ? [X2] : occ(X2,X0) != occ(X2,X1)
& list_succeeds(X0)
& list_succeeds(X1)
& same_occ_succeeds(X0,X1) ),
inference(flattening,[],[f694]) ).
fof(f696,definition,
! [X1,X0,X2] :
( sP0(X1,X0,X2)
<=> ? [X5,X6] :
( X1 = cons(X0,X5)
& X2 = s(X6)
& occ_succeeds(X0,X5,X6) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f709,plain,
! [X0,X1,X2] :
( ( member2_succeeds(X0,X1,X2)
| ( ~ member_succeeds(X0,X2)
& ~ member_succeeds(X0,X1) ) )
& ( member_succeeds(X0,X2)
| member_succeeds(X0,X1)
| ~ member2_succeeds(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f46]) ).
fof(f710,plain,
! [X0,X1,X2] :
( ( member2_succeeds(X0,X1,X2)
| ( ~ member_succeeds(X0,X2)
& ~ member_succeeds(X0,X1) ) )
& ( member_succeeds(X0,X2)
| member_succeeds(X0,X1)
| ~ member2_succeeds(X0,X1,X2) ) ),
inference(flattening,[],[f709]) ).
fof(f719,plain,
! [X1,X0,X2] :
( ( sP0(X1,X0,X2)
| ! [X5,X6] :
( cons(X0,X5) != X1
| s(X6) != X2
| ~ occ_succeeds(X0,X5,X6) ) )
& ( ? [X5,X6] :
( X1 = cons(X0,X5)
& X2 = s(X6)
& occ_succeeds(X0,X5,X6) )
| ~ sP0(X1,X0,X2) ) ),
inference(nnf_transformation,[],[f696]) ).
fof(f720,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3,X4] :
( cons(X1,X3) != X0
| s(X4) != X2
| ~ occ_succeeds(X1,X3,X4) ) )
& ( ? [X5,X6] :
( cons(X1,X5) = X0
& X2 = s(X6)
& occ_succeeds(X1,X5,X6) )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f719]) ).
fof(f721,plain,
! [X0,X1,X2] :
( ( sP0(X0,X1,X2)
| ! [X3,X4] :
( cons(X1,X3) != X0
| s(X4) != X2
| ~ occ_succeeds(X1,X3,X4) ) )
& ( ( cons(X1,sK8(X0,X1,X2)) = X0
& s(sK9(X0,X1,X2)) = X2
& occ_succeeds(X1,sK8(X0,X1,X2),sK9(X0,X1,X2)) )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X5,sK8(X0,X1,X2)),skolemize(X6,sK9(X0,X1,X2))],[f720]) ).
fof(f738,plain,
! [X0,X1] :
( ( not_same_occ_succeeds(X0,X1)
| ! [X2,X3,X4] :
( ~ member2_succeeds(X2,X0,X1)
| ~ occ_succeeds(X2,X0,X3)
| ~ occ_succeeds(X2,X1,X4)
| X3 = X4 ) )
& ( ? [X2,X3,X4] :
( member2_succeeds(X2,X0,X1)
& occ_succeeds(X2,X0,X3)
& occ_succeeds(X2,X1,X4)
& X3 != X4 )
| ~ not_same_occ_succeeds(X0,X1) ) ),
inference(nnf_transformation,[],[f52]) ).
fof(f739,plain,
! [X0,X1] :
( ( not_same_occ_succeeds(X0,X1)
| ! [X2,X3,X4] :
( ~ member2_succeeds(X2,X0,X1)
| ~ occ_succeeds(X2,X0,X3)
| ~ occ_succeeds(X2,X1,X4)
| X3 = X4 ) )
& ( ? [X5,X6,X7] :
( member2_succeeds(X5,X0,X1)
& occ_succeeds(X5,X0,X6)
& occ_succeeds(X5,X1,X7)
& X6 != X7 )
| ~ not_same_occ_succeeds(X0,X1) ) ),
inference(rectify,[],[f738]) ).
fof(f740,plain,
! [X0,X1] :
( ( not_same_occ_succeeds(X0,X1)
| ! [X2,X3,X4] :
( ~ member2_succeeds(X2,X0,X1)
| ~ occ_succeeds(X2,X0,X3)
| ~ occ_succeeds(X2,X1,X4)
| X3 = X4 ) )
& ( ( member2_succeeds(sK18(X0,X1),X0,X1)
& occ_succeeds(sK18(X0,X1),X0,sK19(X0,X1))
& occ_succeeds(sK18(X0,X1),X1,sK20(X0,X1))
& sK19(X0,X1) != sK20(X0,X1) )
| ~ not_same_occ_succeeds(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18,sK19,sK20]),skolemize(X5,sK18(X0,X1)),skolemize(X6,sK19(X0,X1)),skolemize(X7,sK20(X0,X1))],[f739]) ).
fof(f748,plain,
! [X0,X1] :
( ( same_occ_succeeds(X0,X1)
| ~ not_same_occ_fails(X0,X1) )
& ( not_same_occ_fails(X0,X1)
| ~ same_occ_succeeds(X0,X1) ) ),
inference(nnf_transformation,[],[f55]) ).
fof(f807,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(f808,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,[],[f807]) ).
fof(f809,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,[],[f808]) ).
fof(f810,plain,
! [X0] :
( ( list_succeeds(X0)
| ( ! [X1,X2] :
( cons(X1,X2) != X0
| ~ list_succeeds(X2) )
& nil != X0 ) )
& ( ( cons(sK71(X0),sK72(X0)) = X0
& list_succeeds(sK72(X0)) )
| X0 = nil
| ~ list_succeeds(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72]),skolemize(X3,sK71(X0)),skolemize(X4,sK72(X0))],[f809]) ).
fof(f873,plain,
! [X0] :
( ( nat_succeeds(X0)
| ( ! [X1] :
( s(X1) != X0
| ~ nat_succeeds(X1) )
& '0' != X0 ) )
& ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1) )
| X0 = '0'
| ~ nat_succeeds(X0) ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f874,plain,
! [X0] :
( ( nat_succeeds(X0)
| ( ! [X1] :
( s(X1) != X0
| ~ nat_succeeds(X1) )
& '0' != X0 ) )
& ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1) )
| X0 = '0'
| ~ nat_succeeds(X0) ) ),
inference(flattening,[],[f873]) ).
fof(f875,plain,
! [X0] :
( ( nat_succeeds(X0)
| ( ! [X1] :
( s(X1) != X0
| ~ nat_succeeds(X1) )
& '0' != X0 ) )
& ( ? [X2] :
( s(X2) = X0
& nat_succeeds(X2) )
| X0 = '0'
| ~ nat_succeeds(X0) ) ),
inference(rectify,[],[f874]) ).
fof(f876,plain,
! [X0] :
( ( nat_succeeds(X0)
| ( ! [X1] :
( s(X1) != X0
| ~ nat_succeeds(X1) )
& '0' != X0 ) )
& ( ( s(sK109(X0)) = X0
& nat_succeeds(sK109(X0)) )
| X0 = '0'
| ~ nat_succeeds(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109]),skolemize(X2,sK109(X0))],[f875]) ).
fof(f905,plain,
! [X0,X1,X2] :
( ( ( occ(X0,X1) = X2
| ~ occ_succeeds(X0,X1,X2) )
& ( occ_succeeds(X0,X1,X2)
| occ(X0,X1) != X2 ) )
| ~ list_succeeds(X1) ),
inference(nnf_transformation,[],[f649]) ).
fof(f908,plain,
! [X0,X1,X2] :
( delete_succeeds(X0,X1,sK131(X0,X1))
| ~ list_succeeds(X1)
| s(X2) != occ(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK131]),skolemize(X3,sK131(X0,X1))],[f685]) ).
fof(f913,plain,
( occ(sK141,sK139) != occ(sK141,sK140)
& list_succeeds(sK139)
& list_succeeds(sK140)
& same_occ_succeeds(sK139,sK140) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK139,sK140,sK141]),skolemize(X0,sK139),skolemize(X1,sK140),skolemize(X2,sK141)],[f695]) ).
fof(f919,plain,
! [X0,X1] :
( s(X0) != s(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f328]) ).
fof(f921,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f329]) ).
fof(f934,plain,
! [X0,X1] :
( ~ not_same_occ_fails(X0,X1)
| ~ not_same_occ_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f337]) ).
fof(f963,plain,
! [X2,X0,X1] :
( member2_succeeds(X0,X1,X2)
| ~ member_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f710]) ).
fof(f964,plain,
! [X2,X0,X1] :
( member2_succeeds(X0,X1,X2)
| ~ member_succeeds(X0,X2) ),
inference(cnf_transformation,[],[f710]) ).
fof(f980,plain,
! [X2,X0,X1] :
( occ_succeeds(X1,sK8(X0,X1,X2),sK9(X0,X1,X2))
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f721]) ).
fof(f981,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| s(sK9(X0,X1,X2)) = X2 ),
inference(cnf_transformation,[],[f721]) ).
fof(f982,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| cons(X1,sK8(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f721]) ).
fof(f983,plain,
! [X2,X3,X0,X1,X4] :
( sP0(X0,X1,X2)
| cons(X1,X3) != X0
| s(X4) != X2
| ~ occ_succeeds(X1,X3,X4) ),
inference(cnf_transformation,[],[f721]) ).
fof(f1016,plain,
! [X2,X3,X0,X1,X4] :
( ~ occ_succeeds(X2,X1,X4)
| ~ member2_succeeds(X2,X0,X1)
| ~ occ_succeeds(X2,X0,X3)
| not_same_occ_succeeds(X0,X1)
| X3 = X4 ),
inference(cnf_transformation,[],[f740]) ).
fof(f1033,plain,
! [X0,X1] :
( ~ same_occ_succeeds(X0,X1)
| not_same_occ_fails(X0,X1) ),
inference(cnf_transformation,[],[f748]) ).
fof(f1130,plain,
! [X2,X0,X1] :
( list_succeeds(X0)
| cons(X1,X2) != X0
| ~ list_succeeds(X2) ),
inference(cnf_transformation,[],[f810]) ).
fof(f1229,plain,
! [X0] :
( ~ nat_succeeds(X0)
| '0' = X0
| s(sK109(X0)) = X0 ),
inference(cnf_transformation,[],[f876]) ).
fof(f1332,plain,
! [X0,X1] :
( ~ list_succeeds(cons(X0,X1))
| list_succeeds(X1) ),
inference(cnf_transformation,[],[f521]) ).
fof(f1417,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| member_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1432,plain,
! [X2,X0,X1] :
( occ_succeeds(X0,X1,X2)
| occ(X0,X1) != X2
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f905]) ).
fof(f1433,plain,
! [X2,X0,X1] :
( occ(X0,X1) = X2
| ~ occ_succeeds(X0,X1,X2)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f905]) ).
fof(f1445,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| list_succeeds(X1) ),
inference(cnf_transformation,[],[f665]) ).
fof(f1451,plain,
! [X0,X1] :
( nat_succeeds(occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f672]) ).
fof(f1458,plain,
! [X2,X0,X1] :
( s(X2) != occ(X0,X1)
| ~ list_succeeds(X1)
| delete_succeeds(X0,X1,sK131(X0,X1)) ),
inference(cnf_transformation,[],[f908]) ).
fof(f1468,plain,
same_occ_succeeds(sK139,sK140),
inference(cnf_transformation,[],[f913]) ).
fof(f1469,plain,
list_succeeds(sK140),
inference(cnf_transformation,[],[f913]) ).
fof(f1470,plain,
list_succeeds(sK139),
inference(cnf_transformation,[],[f913]) ).
fof(f1471,plain,
occ(sK141,sK139) != occ(sK141,sK140),
inference(cnf_transformation,[],[f913]) ).
fof(f1475,plain,
! [X2,X3,X1,X4] :
( sP0(cons(X1,X3),X1,X2)
| s(X4) != X2
| ~ occ_succeeds(X1,X3,X4) ),
inference(equality_resolution,[],[f983]) ).
fof(f1476,plain,
! [X3,X1,X4] :
( sP0(cons(X1,X3),X1,s(X4))
| ~ occ_succeeds(X1,X3,X4) ),
inference(equality_resolution,[],[f1475]) ).
fof(f1528,plain,
! [X2,X1] :
( list_succeeds(cons(X1,X2))
| ~ list_succeeds(X2) ),
inference(equality_resolution,[],[f1130]) ).
fof(f1585,plain,
! [X0,X1] :
( occ_succeeds(X0,X1,occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(equality_resolution,[],[f1432]) ).
fof(f1587,definition,
sF142 = occ(sK141,sK139),
introduced(definition,[new_symbols(definition,[sF142])],[function_definition]) ).
fof(f1588,plain,
occ(sK141,sK139) = sF142,
inference(reorient_equations,[],[f1587]) ).
fof(f1589,definition,
sF143 = occ(sK141,sK140),
introduced(definition,[new_symbols(definition,[sF143])],[function_definition]) ).
fof(f1590,plain,
occ(sK141,sK140) = sF143,
inference(reorient_equations,[],[f1589]) ).
fof(f1591,plain,
sF142 != sF143,
inference(definition_folding,[],[f1471,f1590,f1588]) ).
fof(f1628,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| occ(X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f1433,f1445]) ).
fof(f1652,plain,
( nat_succeeds(sF143)
| ~ list_succeeds(sK140) ),
inference(superposition,[],[f1451,f1590]) ).
fof(f1653,plain,
( nat_succeeds(sF142)
| ~ list_succeeds(sK139) ),
inference(superposition,[],[f1451,f1588]) ).
fof(f1661,plain,
nat_succeeds(sF142),
inference(forward_subsumption_resolution,[],[f1653,f1470]) ).
fof(f1662,plain,
nat_succeeds(sF143),
inference(forward_subsumption_resolution,[],[f1652,f1469]) ).
fof(f1663,plain,
! [X2,X0,X1] :
( ~ sP0(X0,X1,X2)
| sK9(X0,X1,X2) = occ(X1,sK8(X0,X1,X2)) ),
inference(resolution,[],[f980,f1628]) ).
fof(f1668,plain,
( occ_succeeds(sK141,sK140,sF143)
| ~ list_succeeds(sK140) ),
inference(superposition,[],[f1585,f1590]) ).
fof(f1669,plain,
( occ_succeeds(sK141,sK139,sF142)
| ~ list_succeeds(sK139) ),
inference(superposition,[],[f1585,f1588]) ).
fof(f1678,plain,
occ_succeeds(sK141,sK139,sF142),
inference(forward_subsumption_resolution,[],[f1669,f1470]) ).
fof(f1679,plain,
occ_succeeds(sK141,sK140,sF143),
inference(forward_subsumption_resolution,[],[f1668,f1469]) ).
fof(f1735,plain,
! [X0] :
( s(X0) != sF143
| ~ list_succeeds(sK140)
| delete_succeeds(sK141,sK140,sK131(sK141,sK140)) ),
inference(superposition,[],[f1458,f1590]) ).
fof(f1745,plain,
! [X0] :
( s(X0) != sF143
| delete_succeeds(sK141,sK140,sK131(sK141,sK140)) ),
inference(forward_subsumption_resolution,[],[f1735,f1469]) ).
fof(f1747,definition,
( spl144_9
<=> delete_succeeds(sK141,sK139,sK131(sK141,sK139)) ),
introduced(definition,[new_symbols(definition,[spl144_9])],[avatar_definition]) ).
fof(f1748,plain,
( ~ delete_succeeds(sK141,sK139,sK131(sK141,sK139))
| spl144_9 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1749,plain,
( delete_succeeds(sK141,sK139,sK131(sK141,sK139))
| ~ spl144_9 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1751,definition,
( spl144_10
<=> ! [X0] : s(X0) != sF142 ),
introduced(definition,[new_symbols(definition,[spl144_10])],[avatar_definition]) ).
fof(f1752,plain,
( ! [X0] : s(X0) != sF142
| ~ spl144_10 ),
inference(avatar_component_clause,[],[f1751]) ).
fof(f1755,definition,
( spl144_11
<=> delete_succeeds(sK141,sK140,sK131(sK141,sK140)) ),
introduced(definition,[new_symbols(definition,[spl144_11])],[avatar_definition]) ).
fof(f1757,plain,
( delete_succeeds(sK141,sK140,sK131(sK141,sK140))
| ~ spl144_11 ),
inference(avatar_component_clause,[],[f1755]) ).
fof(f1759,definition,
( spl144_12
<=> ! [X0] : s(X0) != sF143 ),
introduced(definition,[new_symbols(definition,[spl144_12])],[avatar_definition]) ).
fof(f1760,plain,
( ! [X0] : s(X0) != sF143
| ~ spl144_12 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1761,plain,
( spl144_11
| spl144_12 ),
inference(avatar_split_clause,[],[f1745,f1759,f1755]) ).
fof(f1780,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| s(X2) = s(sK9(cons(X0,X1),X0,s(X2))) ),
inference(resolution,[],[f1476,f981]) ).
fof(f1783,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| cons(X0,X1) = cons(X0,sK8(cons(X0,X1),X0,s(X2))) ),
inference(resolution,[],[f1476,f982]) ).
fof(f1789,plain,
cons(sK141,sK139) = cons(sK141,sK8(cons(sK141,sK139),sK141,s(sF142))),
inference(resolution,[],[f1783,f1678]) ).
fof(f1794,plain,
s(sF142) = s(sK9(cons(sK141,sK139),sK141,s(sF142))),
inference(resolution,[],[f1780,f1678]) ).
fof(f1799,plain,
! [X0] :
( s(X0) != s(sF142)
| sK9(cons(sK141,sK139),sK141,s(sF142)) = X0 ),
inference(superposition,[],[f919,f1794]) ).
fof(f1802,plain,
sF142 = sK9(cons(sK141,sK139),sK141,s(sF142)),
inference(equality_resolution,[],[f1799]) ).
fof(f1807,definition,
( spl144_13
<=> sP0(cons(sK141,sK139),sK141,s(sF142)) ),
introduced(definition,[new_symbols(definition,[spl144_13])],[avatar_definition]) ).
fof(f1808,plain,
( sP0(cons(sK141,sK139),sK141,s(sF142))
| ~ spl144_13 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1809,plain,
( ~ sP0(cons(sK141,sK139),sK141,s(sF142))
| spl144_13 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1815,plain,
( ~ occ_succeeds(sK141,sK139,sF142)
| spl144_13 ),
inference(resolution,[],[f1809,f1476]) ).
fof(f1816,plain,
( $false
| spl144_13 ),
inference(forward_subsumption_resolution,[],[f1815,f1678]) ).
fof(f1817,plain,
spl144_13,
inference(avatar_contradiction_clause,[],[f1816]) ).
fof(f1819,plain,
( sK9(cons(sK141,sK139),sK141,s(sF142)) = occ(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)))
| ~ spl144_13 ),
inference(resolution,[],[f1808,f1663]) ).
fof(f1822,plain,
( sF142 = occ(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)))
| ~ spl144_13 ),
inference(forward_demodulation,[],[f1819,f1802]) ).
fof(f2010,plain,
( ! [X0] :
( s(X0) != sF142
| ~ list_succeeds(sK8(cons(sK141,sK139),sK141,s(sF142)))
| delete_succeeds(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)),sK131(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)))) )
| ~ spl144_13 ),
inference(superposition,[],[f1458,f1822]) ).
fof(f2014,definition,
( spl144_27
<=> delete_succeeds(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)),sK131(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)))) ),
introduced(definition,[new_symbols(definition,[spl144_27])],[avatar_definition]) ).
fof(f2016,plain,
( delete_succeeds(sK141,sK8(cons(sK141,sK139),sK141,s(sF142)),sK131(sK141,sK8(cons(sK141,sK139),sK141,s(sF142))))
| ~ spl144_27 ),
inference(avatar_component_clause,[],[f2014]) ).
fof(f2018,definition,
( spl144_28
<=> list_succeeds(sK8(cons(sK141,sK139),sK141,s(sF142))) ),
introduced(definition,[new_symbols(definition,[spl144_28])],[avatar_definition]) ).
fof(f2020,plain,
( ~ list_succeeds(sK8(cons(sK141,sK139),sK141,s(sF142)))
| spl144_28 ),
inference(avatar_component_clause,[],[f2018]) ).
fof(f2021,plain,
( spl144_27
| ~ spl144_28
| spl144_10
| ~ spl144_13 ),
inference(avatar_split_clause,[],[f2010,f1807,f1751,f2018,f2014]) ).
fof(f2105,plain,
not_same_occ_fails(sK139,sK140),
inference(resolution,[],[f1033,f1468]) ).
fof(f2189,plain,
! [X0,X1] :
( ~ occ_succeeds(sK141,X0,X1)
| ~ member2_succeeds(sK141,X0,sK140)
| not_same_occ_succeeds(X0,sK140)
| sF143 = X1 ),
inference(resolution,[],[f1016,f1679]) ).
fof(f2366,plain,
! [X0,X1] :
( cons(X0,X1) != cons(sK141,sK139)
| sK8(cons(sK141,sK139),sK141,s(sF142)) = X1 ),
inference(superposition,[],[f921,f1789]) ).
fof(f2369,plain,
( ~ list_succeeds(cons(sK141,sK139))
| list_succeeds(sK8(cons(sK141,sK139),sK141,s(sF142))) ),
inference(superposition,[],[f1332,f1789]) ).
fof(f2378,plain,
( ~ list_succeeds(cons(sK141,sK139))
| spl144_28 ),
inference(forward_subsumption_resolution,[],[f2369,f2020]) ).
fof(f2379,plain,
( ~ list_succeeds(sK139)
| spl144_28 ),
inference(resolution,[],[f2378,f1528]) ).
fof(f2380,plain,
( $false
| spl144_28 ),
inference(forward_subsumption_resolution,[],[f2379,f1470]) ).
fof(f2381,plain,
spl144_28,
inference(avatar_contradiction_clause,[],[f2380]) ).
fof(f2390,plain,
sK139 = sK8(cons(sK141,sK139),sK141,s(sF142)),
inference(equality_resolution,[],[f2366]) ).
fof(f2798,plain,
( ~ member2_succeeds(sK141,sK139,sK140)
| not_same_occ_succeeds(sK139,sK140)
| sF142 = sF143 ),
inference(resolution,[],[f2189,f1678]) ).
fof(f2806,plain,
( ~ member2_succeeds(sK141,sK139,sK140)
| not_same_occ_succeeds(sK139,sK140) ),
inference(forward_subsumption_resolution,[],[f2798,f1591]) ).
fof(f2811,definition,
( spl144_76
<=> not_same_occ_succeeds(sK139,sK140) ),
introduced(definition,[new_symbols(definition,[spl144_76])],[avatar_definition]) ).
fof(f2813,plain,
( not_same_occ_succeeds(sK139,sK140)
| ~ spl144_76 ),
inference(avatar_component_clause,[],[f2811]) ).
fof(f2815,definition,
( spl144_77
<=> member2_succeeds(sK141,sK139,sK140) ),
introduced(definition,[new_symbols(definition,[spl144_77])],[avatar_definition]) ).
fof(f2817,plain,
( ~ member2_succeeds(sK141,sK139,sK140)
| spl144_77 ),
inference(avatar_component_clause,[],[f2815]) ).
fof(f2818,plain,
( spl144_76
| ~ spl144_77 ),
inference(avatar_split_clause,[],[f2806,f2815,f2811]) ).
fof(f3252,definition,
( spl144_85
<=> '0' = sF143 ),
introduced(definition,[new_symbols(definition,[spl144_85])],[avatar_definition]) ).
fof(f3253,plain,
( '0' != sF143
| spl144_85 ),
inference(avatar_component_clause,[],[f3252]) ).
fof(f3254,plain,
( '0' = sF143
| ~ spl144_85 ),
inference(avatar_component_clause,[],[f3252]) ).
fof(f3261,plain,
( '0' != sF142
| ~ spl144_85 ),
inference(superposition,[],[f1591,f3254]) ).
fof(f3289,definition,
( spl144_87
<=> '0' = sF142 ),
introduced(definition,[new_symbols(definition,[spl144_87])],[avatar_definition]) ).
fof(f3290,plain,
( '0' != sF142
| spl144_87 ),
inference(avatar_component_clause,[],[f3289]) ).
fof(f3296,plain,
( ~ spl144_87
| ~ spl144_85 ),
inference(avatar_split_clause,[],[f3261,f3252,f3289]) ).
fof(f8875,plain,
( delete_succeeds(sK141,sK139,sK131(sK141,sK139))
| ~ spl144_27 ),
inference(forward_demodulation,[],[f2016,f2390]) ).
fof(f8910,plain,
( $false
| spl144_9
| ~ spl144_27 ),
inference(forward_subsumption_resolution,[],[f8875,f1748]) ).
fof(f8911,plain,
( spl144_9
| ~ spl144_27 ),
inference(avatar_contradiction_clause,[],[f8910]) ).
fof(f11760,plain,
( '0' = sF142
| sF142 = s(sK109(sF142)) ),
inference(resolution,[],[f1229,f1661]) ).
fof(f11761,plain,
( '0' = sF143
| sF143 = s(sK109(sF143)) ),
inference(resolution,[],[f1229,f1662]) ).
fof(f11762,plain,
( sF143 = s(sK109(sF143))
| spl144_85 ),
inference(forward_subsumption_resolution,[],[f11761,f3253]) ).
fof(f11766,plain,
( $false
| ~ spl144_12
| spl144_85 ),
inference(forward_subsumption_resolution,[],[f11762,f1760]) ).
fof(f11767,plain,
( ~ spl144_12
| spl144_85 ),
inference(avatar_contradiction_clause,[],[f11766]) ).
fof(f12285,plain,
( member_succeeds(sK141,sK140)
| ~ spl144_11 ),
inference(resolution,[],[f1417,f1757]) ).
fof(f13462,plain,
( ~ member_succeeds(sK141,sK140)
| spl144_77 ),
inference(resolution,[],[f964,f2817]) ).
fof(f13483,plain,
( $false
| ~ spl144_11
| spl144_77 ),
inference(forward_subsumption_resolution,[],[f13462,f12285]) ).
fof(f13484,plain,
( ~ spl144_11
| spl144_77 ),
inference(avatar_contradiction_clause,[],[f13483]) ).
fof(f15162,plain,
~ not_same_occ_succeeds(sK139,sK140),
inference(resolution,[],[f934,f2105]) ).
fof(f15372,plain,
( $false
| ~ spl144_76 ),
inference(forward_subsumption_resolution,[],[f15162,f2813]) ).
fof(f15373,plain,
~ spl144_76,
inference(avatar_contradiction_clause,[],[f15372]) ).
fof(f15581,plain,
( sF142 = s(sK109(sF142))
| spl144_87 ),
inference(forward_subsumption_resolution,[],[f11760,f3290]) ).
fof(f16050,plain,
( ~ member_succeeds(sK141,sK139)
| spl144_77 ),
inference(resolution,[],[f2817,f963]) ).
fof(f16061,plain,
( member_succeeds(sK141,sK139)
| ~ spl144_9 ),
inference(resolution,[],[f1749,f1417]) ).
fof(f16067,plain,
( $false
| ~ spl144_9
| spl144_77 ),
inference(forward_subsumption_resolution,[],[f16061,f16050]) ).
fof(f16068,plain,
( ~ spl144_9
| spl144_77 ),
inference(avatar_contradiction_clause,[],[f16067]) ).
fof(f16347,plain,
( sF142 != sF142
| ~ spl144_10
| spl144_87 ),
inference(superposition,[],[f1752,f15581]) ).
fof(f16354,plain,
( $false
| ~ spl144_10
| spl144_87 ),
inference(trivial_inequality_removal,[],[f16347]) ).
fof(f16355,plain,
( ~ spl144_10
| spl144_87 ),
inference(avatar_contradiction_clause,[],[f16354]) ).
cnf(s10,plain,
( spl144_11
| spl144_12 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s12,plain,
spl144_13,
inference(sat_conversion,[],[f1817]) ).
cnf(s22,plain,
( spl144_10
| ~ spl144_13
| spl144_27
| ~ spl144_28 ),
inference(sat_conversion,[],[f2021]) ).
cnf(s43,plain,
spl144_28,
inference(sat_conversion,[],[f2381]) ).
cnf(s55,plain,
( spl144_76
| ~ spl144_77 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s69,plain,
( ~ spl144_85
| ~ spl144_87 ),
inference(sat_conversion,[],[f3296]) ).
cnf(s225,plain,
( spl144_9
| ~ spl144_27 ),
inference(sat_conversion,[],[f8911]) ).
cnf(s270,plain,
( ~ spl144_12
| spl144_85 ),
inference(sat_conversion,[],[f11767]) ).
cnf(s314,plain,
( ~ spl144_11
| spl144_77 ),
inference(sat_conversion,[],[f13484]) ).
cnf(s392,plain,
~ spl144_76,
inference(sat_conversion,[],[f15373]) ).
cnf(s444,plain,
( ~ spl144_9
| spl144_77 ),
inference(sat_conversion,[],[f16068]) ).
cnf(s460,plain,
( ~ spl144_10
| spl144_87 ),
inference(sat_conversion,[],[f16355]) ).
cnf(s471,plain,
~ spl144_77,
inference(rat,[],[s55,s392]) ).
cnf(s472,plain,
~ spl144_9,
inference(rat,[],[s444,s471]) ).
cnf(s473,plain,
~ spl144_11,
inference(rat,[],[s314,s471]) ).
cnf(s474,plain,
~ spl144_27,
inference(rat,[],[s225,s472]) ).
cnf(s490,plain,
( spl144_10
| ~ spl144_13 ),
inference(rat,[],[s22,s43,s474]) ).
cnf(s506,plain,
spl144_10,
inference(rat,[],[s490,s12]) ).
cnf(s511,plain,
spl144_87,
inference(rat,[],[s460,s506]) ).
cnf(s518,plain,
~ spl144_85,
inference(rat,[],[s69,s511]) ).
cnf(s522,plain,
~ spl144_12,
inference(rat,[],[s270,s518]) ).
cnf(s527,plain,
$false,
inference(rat,[],[s10,s522,s473]) ).
fof(f16357,plain,
$false,
inference(avatar_sat_refutation,[],[s527]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX055+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.27 % Computer : n017.cluster.edu
% 0.10/0.27 % Model : x86_64 x86_64
% 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.27 % Memory : 8046.5625MB
% 0.10/0.27 % OS : Linux 6.8.0-71-generic
% 0.10/0.27 % CPULimit : 300
% 0.10/0.27 % WCLimit : 300
% 0.10/0.27 % DateTime : Mon Sep 28 14:53:07 UTC 2026
% 0.27/0.28 % CPUTime :
% 0.27/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.27/0.31 Running first-order theorem proving
% 0.27/0.31 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
% 21.71/3.98 % (3611336)Detected formulas, will run a generic FOF schedule.
% 21.71/3.98 % (3611349)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=1259794702:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 21.71/3.98 % (3611355)dis-21_1_sil=8000:lcm=predicate:random_seed=133199491: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)
% 21.71/3.98 % (3611352)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3015084769:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 21.71/3.98 % (3611354)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1688509781:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 21.71/3.98 % (3611353)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1723526281:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 21.71/3.98 % (3611350)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=799536421:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 21.71/3.98 % (3611351)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=2080938990:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 21.71/3.98 % (3611355)Instruction limit reached!
% 21.71/3.98 % (3611355)------------------------------
% 21.71/3.98 % (3611355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.71/3.98 % (3611355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.71/3.98 % (3611355)CaDiCaL version: 2.1.3
% 21.71/3.98 % (3611355)Termination reason: Instruction limit
% 21.71/3.98 % (3611355)Termination phase: Saturation
% 21.71/3.98 % (3611355)Time elapsed: 0.068 s
% 21.71/3.98 % (3611355)Peak memory usage: 90 MB
% 21.71/3.98 % (3611355)Instructions burned: 130 (million)
% 21.71/3.98 % (3611352)Instruction limit reached!
% 21.71/3.98 % (3611352)------------------------------
% 21.71/3.98 % (3611352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.71/3.98 % (3611352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.71/3.98 % (3611352)CaDiCaL version: 2.1.3
% 21.71/3.98 % (3611352)Termination reason: Instruction limit
% 21.71/3.98 % (3611352)Termination phase: Saturation
% 21.71/3.98 % (3611352)Time elapsed: 0.104 s
% 21.71/3.98 % (3611352)Peak memory usage: 90 MB
% 21.71/3.98 % (3611352)Instructions burned: 109 (million)
% 21.71/3.98 % (3611353)Instruction limit reached!
% 21.71/3.98 % (3611353)------------------------------
% 21.71/3.98 % (3611353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.71/3.98 % (3611353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.71/3.98 % (3611353)CaDiCaL version: 2.1.3
% 21.71/3.98 % (3611353)Termination reason: Instruction limit
% 21.71/3.98 % (3611353)Termination phase: Saturation
% 21.71/3.98 % (3611353)Time elapsed: 0.105 s
% 21.71/3.98 % (3611353)Peak memory usage: 89 MB
% 21.71/3.98 % (3611353)Instructions burned: 119 (million)
% 21.71/3.98 % (3611354)Instruction limit reached!
% 21.71/3.98 % (3611354)------------------------------
% 21.71/3.98 % (3611354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.71/3.98 % (3611354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.71/3.98 % (3611354)CaDiCaL version: 2.1.3
% 21.71/3.98 % (3611354)Termination reason: Instruction limit
% 21.71/3.98 % (3611354)Termination phase: Saturation
% 21.71/3.98 % (3611354)Time elapsed: 0.146 s
% 21.71/3.98 % (3611354)Peak memory usage: 90 MB
% 21.71/3.98 % (3611354)Instructions burned: 139 (million)
% 21.71/3.98 % (3611368)lrs+10_1_sil=8000:sp=occurrence:random_seed=3722614609:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 21.71/3.98 % (3611371)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1607790726:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 21.71/3.98 % (3611371)Refutation not found, incomplete strategy
% 21.71/3.98 % (3611371)------------------------------
% 21.71/3.98 % (3611371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.71/3.98 % (3611371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.71/3.98 % (3611371)CaDiCaL version: 2.1.3
% 21.71/3.98 % (3611371)Termination reason: Refutation not found, incomplete strategy
% 17.91/4.51 % (3611371)Time elapsed: 0.023 s
% 17.91/4.51 % (3611371)Peak memory usage: 89 MB
% 17.91/4.51 % (3611371)Instructions burned: 18 (million)
% 17.91/4.51 % (3611370)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2414916781:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 17.91/4.51 % (3611370)Refutation not found, incomplete strategy
% 17.91/4.51 % (3611370)------------------------------
% 17.91/4.51 % (3611370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611370)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611370)Termination reason: Refutation not found, incomplete strategy
% 17.91/4.51 % (3611370)Time elapsed: 0.021 s
% 17.91/4.51 % (3611370)Peak memory usage: 89 MB
% 17.91/4.51 % (3611370)Instructions burned: 17 (million)
% 17.91/4.51 % (3611368)Instruction limit reached!
% 17.91/4.51 % (3611368)------------------------------
% 17.91/4.51 % (3611368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611368)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611368)Termination reason: Instruction limit
% 17.91/4.51 % (3611368)Termination phase: Saturation
% 17.91/4.51 % (3611368)Time elapsed: 0.167 s
% 17.91/4.51 % (3611368)Peak memory usage: 92 MB
% 17.91/4.51 % (3611368)Instructions burned: 286 (million)
% 17.91/4.51 % (3611372)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=1647737194:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 17.91/4.51 % (3611376)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=262669001:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 17.91/4.51 % (3611372)Instruction limit reached!
% 17.91/4.51 % (3611372)------------------------------
% 17.91/4.51 % (3611372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611372)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611372)Termination reason: Instruction limit
% 17.91/4.51 % (3611372)Termination phase: Saturation
% 17.91/4.51 % (3611372)Time elapsed: 0.229 s
% 17.91/4.51 % (3611372)Peak memory usage: 93 MB
% 17.91/4.51 % (3611372)Instructions burned: 249 (million)
% 17.91/4.51 % (3611376)Instruction limit reached!
% 17.91/4.51 % (3611376)------------------------------
% 17.91/4.51 % (3611376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611376)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611376)Termination reason: Instruction limit
% 17.91/4.51 % (3611376)Termination phase: Saturation
% 17.91/4.51 % (3611376)Time elapsed: 0.139 s
% 17.91/4.51 % (3611376)Peak memory usage: 89 MB
% 17.91/4.51 % (3611376)Instructions burned: 294 (million)
% 17.91/4.51 % (3611371)------------------------------
% 17.91/4.51 % (3611371)------------------------------
% 17.91/4.51 % (3611370)------------------------------
% 17.91/4.51 % (3611370)------------------------------
% 17.91/4.51 % (3611379)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3054445492:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 17.91/4.51 % (3611381)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1368619199:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 17.91/4.51 % (3611383)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1109803329:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 17.91/4.51 % (3611384)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1730022698:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 17.91/4.51 % (3611381)Instruction limit reached!
% 17.91/4.51 % (3611381)------------------------------
% 17.91/4.51 % (3611381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611381)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611381)Termination reason: Instruction limit
% 17.91/4.51 % (3611381)Termination phase: Saturation
% 17.91/4.51 % (3611381)Time elapsed: 0.115 s
% 17.91/4.51 % (3611381)Peak memory usage: 90 MB
% 17.91/4.51 % (3611381)Instructions burned: 113 (million)
% 17.91/4.51 % (3611383)Instruction limit reached!
% 17.91/4.51 % (3611383)------------------------------
% 17.91/4.51 % (3611383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611383)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611383)Termination reason: Instruction limit
% 17.91/4.51 % (3611383)Termination phase: Saturation
% 17.91/4.51 % (3611383)Time elapsed: 0.112 s
% 17.91/4.51 % (3611383)Peak memory usage: 90 MB
% 17.91/4.51 % (3611383)Instructions burned: 127 (million)
% 17.91/4.51 % (3611384)Instruction limit reached!
% 17.91/4.51 % (3611384)------------------------------
% 17.91/4.51 % (3611384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611384)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611384)Termination reason: Instruction limit
% 17.91/4.51 % (3611384)Termination phase: Saturation
% 17.91/4.51 % (3611384)Time elapsed: 0.110 s
% 17.91/4.51 % (3611384)Peak memory usage: 89 MB
% 17.91/4.51 % (3611384)Instructions burned: 114 (million)
% 17.91/4.51 % (3611389)lrs+10_1_sil=8000:sp=occurrence:random_seed=2025411469:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 17.91/4.51 % (3611390)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1530057120:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 17.91/4.51 % (3611391)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3371844868:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 17.91/4.51 % (3611390)Instruction limit reached!
% 17.91/4.51 % (3611390)------------------------------
% 17.91/4.51 % (3611390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611390)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611390)Termination reason: Instruction limit
% 17.91/4.51 % (3611390)Termination phase: Saturation
% 17.91/4.51 % (3611390)Time elapsed: 0.409 s
% 17.91/4.51 % (3611390)Peak memory usage: 91 MB
% 17.91/4.51 % (3611390)Instructions burned: 437 (million)
% 17.91/4.51 % (3611395)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1293350506:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2981 on theBenchmark for (2981ds/134Mi)
% 17.91/4.51 % (3611395)Instruction limit reached!
% 17.91/4.51 % (3611395)------------------------------
% 17.91/4.51 % (3611395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611395)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611395)Termination reason: Instruction limit
% 17.91/4.51 % (3611395)Termination phase: Saturation
% 17.91/4.51 % (3611395)Time elapsed: 0.130 s
% 17.91/4.51 % (3611395)Peak memory usage: 92 MB
% 17.91/4.51 % (3611395)Instructions burned: 135 (million)
% 17.91/4.51 % (3611389)Instruction limit reached!
% 17.91/4.51 % (3611389)------------------------------
% 17.91/4.51 % (3611389)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611389)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611389)Termination reason: Instruction limit
% 17.91/4.51 % (3611389)Termination phase: Saturation
% 17.91/4.51 % (3611389)Time elapsed: 0.932 s
% 17.91/4.51 % (3611389)Peak memory usage: 100 MB
% 17.91/4.51 % (3611389)Instructions burned: 907 (million)
% 17.91/4.51 % (3611400)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1397598911:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 17.91/4.51 % (3611402)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1447677484:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 17.91/4.51 % (3611400)Instruction limit reached!
% 17.91/4.51 % (3611400)------------------------------
% 17.91/4.51 % (3611400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611400)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611400)Termination reason: Instruction limit
% 17.91/4.51 % (3611400)Termination phase: Saturation
% 17.91/4.51 % (3611400)Time elapsed: 0.572 s
% 17.91/4.51 % (3611400)Peak memory usage: 99 MB
% 17.91/4.51 % (3611400)Instructions burned: 592 (million)
% 17.91/4.51 % (3611405)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=4049284577:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 17.91/4.51 % (3611349)First to succeed.
% 17.91/4.51 % (3611349)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3611336"
% 17.91/4.51 % (3611405)Instruction limit reached!
% 17.91/4.51 % (3611405)------------------------------
% 17.91/4.51 % (3611405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611405)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611405)Termination reason: Instruction limit
% 17.91/4.51 % (3611405)Termination phase: Saturation
% 17.91/4.51 % (3611405)Time elapsed: 0.125 s
% 17.91/4.51 % (3611405)Peak memory usage: 91 MB
% 17.91/4.51 % (3611405)Instructions burned: 125 (million)
% 17.91/4.51 % (3611407)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1754781425:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 17.91/4.51 % (3611379)Instruction limit reached!
% 17.91/4.51 % (3611379)------------------------------
% 17.91/4.51 % (3611379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611379)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611379)Termination reason: Instruction limit
% 17.91/4.51 % (3611379)Termination phase: Saturation
% 17.91/4.51 % (3611379)Time elapsed: 2.626 s
% 17.91/4.51 % (3611379)Peak memory usage: 142 MB
% 17.91/4.51 % (3611379)Instructions burned: 2351 (million)
% 17.91/4.51 % (3611407)Instruction limit reached!
% 17.91/4.51 % (3611407)------------------------------
% 17.91/4.51 % (3611407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/4.51 % (3611407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/4.51 % (3611407)CaDiCaL version: 2.1.3
% 17.91/4.51 % (3611407)Termination reason: Instruction limit
% 17.91/4.51 % (3611407)Termination phase: Saturation
% 17.91/4.51 % (3611407)Time elapsed: 0.138 s
% 17.91/4.51 % (3611407)Peak memory usage: 91 MB
% 17.91/4.51 % (3611407)Instructions burned: 135 (million)
% 17.91/4.51 % (3611349)Refutation found. Thanks to Tanya!
% 17.91/4.51 % SZS status Theorem for theBenchmark
% 17.91/4.51 % SZS output start Proof for theBenchmark
% See solution above
% 26.89/4.77 % (3611349)------------------------------
% 26.89/4.77 % (3611349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.89/4.77 % (3611349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.89/4.77 % (3611349)CaDiCaL version: 2.1.3
% 26.89/4.77 % (3611349)Termination reason: Refutation
% 26.89/4.77 % (3611349)Time elapsed: 3.106 s
% 26.89/4.77 % (3611349)Peak memory usage: 147 MB
% 26.89/4.77 % (3611349)Instructions burned: 2800 (million)
% 26.89/4.77 % (3611349)------------------------------
% 26.89/4.77 % (3611349)------------------------------
% 26.89/4.77 % (3611336)Success in time 3.704 s
% 26.89/4.77 % Vampire exiting
%------------------------------------------------------------------------------