%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX029+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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:46:22 PM UTC 2026
% Result : Theorem 36.60s 11.11s
% Output : Refutation 36.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 46
% Syntax : Number of formulae : 284 ( 43 unt; 25 def)
% Number of atoms : 706 ( 136 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 689 ( 267 ~; 347 |; 29 &)
% ( 31 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 26 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 227 ( 0 sgn 212 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : '0' != s(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id1) ).
fof(f7,axiom,
! [X0,X1] : nil != cons(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id7) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( cons(X0,X1) = cons(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id8) ).
fof(f73,axiom,
! [X0,X1,X2] :
( split_succeeds(X0,X1,X2)
<=> ( ? [X3,X4,X5] :
( X0 = cons(X3,X4)
& X1 = cons(X3,X5)
& split_succeeds(X4,X2,X5) )
| ( X0 = nil
& X1 = nil
& X2 = nil ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id73) ).
fof(f97,axiom,
! [X0,X1] :
( length_succeeds(X0,X1)
<=> ( ? [X2,X3,X4] :
( X0 = cons(X2,X3)
& X1 = s(X4)
& length_succeeds(X3,X4) )
| ( X0 = nil
& X1 = '0' ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id97) ).
fof(f121,axiom,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
<=> ( ? [X2,X3] :
( X0 = s(X2)
& X1 = s(X3)
& '@<_succeeds'(X2,X3) )
| ? [X4] :
( X0 = '0'
& X1 = s(X4) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id121) ).
fof(f124,axiom,
! [X0] :
( nat_succeeds(X0)
<=> ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1) )
| X0 = '0' ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id124) ).
fof(f152,axiom,
! [X0] : '@+'('0',X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(plus:zero)') ).
fof(f189,axiom,
! [X0,X1] :
( ( nat_succeeds(X0)
& nat_succeeds(X1) )
=> ( '@<_succeeds'(X0,X1)
| X0 = X1
| '@<_succeeds'(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(less:totality)') ).
fof(f190,axiom,
! [X0] :
( ( nat_succeeds(X0)
& X0 != '0' )
=> '@<_succeeds'('0',X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(less:different:zero)') ).
fof(f203,axiom,
! [X0,X1,X2] :
( ( '@=<_succeeds'(X0,X1)
& '@<_succeeds'(X1,X2) )
=> '@<_succeeds'(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(leq:less:transitive)') ).
fof(f209,axiom,
! [X0,X1,X2] :
( ( nat_succeeds(X0)
& '@<_succeeds'(X1,X2) )
=> '@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(less:plus:second)') ).
fof(f215,axiom,
! [X0,X1] :
( nat_succeeds(X0)
=> '@=<_succeeds'(X0,'@+'(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(leq:plus:first)_011') ).
fof(f218,axiom,
! [X0,X1,X2] :
( ( nat_succeeds(X0)
& nat_succeeds(X1)
& nat_succeeds(X2)
& '@<_succeeds'('@+'(X0,X2),'@+'(X1,X2)) )
=> '@<_succeeds'(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(less:plus:inverse)_013') ).
fof(f228,axiom,
! [X0,X1,X2] :
( ( nat_succeeds(X0)
& nat_succeeds(X1)
& nat_succeeds(X2)
& '@+'(X0,X2) = '@+'(X1,X2) )
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(plus:injective:first)') ).
fof(f263,axiom,
! [X0] :
( list_succeeds(X0)
=> nat_succeeds(lh(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(lh:types)') ).
fof(f264,axiom,
! [X0] :
( ( list_succeeds(X0)
& lh(X0) = '0' )
=> X0 = nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(lh:zero)') ).
fof(f361,axiom,
! [X0,X1] :
( list_succeeds(X0)
=> ( lh(X0) = X1
<=> length_succeeds(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lh/1') ).
fof(f365,axiom,
! [X0,X1,X2] :
( split_succeeds(X0,X1,X2)
=> ( list_succeeds(X0)
& list_succeeds(X1)
& list_succeeds(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(split:types)') ).
fof(f366,axiom,
! [X0,X1,X2] :
( split_succeeds(X0,X1,X2)
=> lh(X0) = '@+'(lh(X1),lh(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(split:length)') ).
fof(f374,conjecture,
! [X0,X1,X2,X3,X4] :
( split_succeeds(cons(X0,cons(X1,X2)),X3,X4)
=> ( '@<_succeeds'(lh(X3),lh(cons(X0,cons(X1,X2))))
& '@<_succeeds'(lh(X4),lh(cons(X0,cons(X1,X2)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(split:length:less)') ).
fof(f375,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( split_succeeds(cons(X0,cons(X1,X2)),X3,X4)
=> ( '@<_succeeds'(lh(X3),lh(cons(X0,cons(X1,X2))))
& '@<_succeeds'(lh(X4),lh(cons(X0,cons(X1,X2)))) ) ),
inference(negated_conjecture,[status(cth)],[f374]) ).
fof(f382,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| cons(X0,X1) != cons(X2,X3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f533,plain,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
| X0 = X1
| '@<_succeeds'(X1,X0)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1) ),
inference(ennf_transformation,[],[f189]) ).
fof(f534,plain,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
| X0 = X1
| '@<_succeeds'(X1,X0)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1) ),
inference(flattening,[],[f533]) ).
fof(f535,plain,
! [X0] :
( '@<_succeeds'('0',X0)
| ~ nat_succeeds(X0)
| '0' = X0 ),
inference(ennf_transformation,[],[f190]) ).
fof(f536,plain,
! [X0] :
( '@<_succeeds'('0',X0)
| ~ nat_succeeds(X0)
| '0' = X0 ),
inference(flattening,[],[f535]) ).
fof(f553,plain,
! [X0,X1,X2] :
( '@<_succeeds'(X0,X2)
| ~ '@=<_succeeds'(X0,X1)
| ~ '@<_succeeds'(X1,X2) ),
inference(ennf_transformation,[],[f203]) ).
fof(f554,plain,
! [X0,X1,X2] :
( '@<_succeeds'(X0,X2)
| ~ '@=<_succeeds'(X0,X1)
| ~ '@<_succeeds'(X1,X2) ),
inference(flattening,[],[f553]) ).
fof(f563,plain,
! [X0,X1,X2] :
( '@<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ nat_succeeds(X0)
| ~ '@<_succeeds'(X1,X2) ),
inference(ennf_transformation,[],[f209]) ).
fof(f564,plain,
! [X0,X1,X2] :
( '@<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| ~ nat_succeeds(X0)
| ~ '@<_succeeds'(X1,X2) ),
inference(flattening,[],[f563]) ).
fof(f574,plain,
! [X0,X1] :
( '@=<_succeeds'(X0,'@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(ennf_transformation,[],[f215]) ).
fof(f579,plain,
! [X0,X1,X2] :
( '@<_succeeds'(X0,X1)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ '@<_succeeds'('@+'(X0,X2),'@+'(X1,X2)) ),
inference(ennf_transformation,[],[f218]) ).
fof(f580,plain,
! [X0,X1,X2] :
( '@<_succeeds'(X0,X1)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| ~ '@<_succeeds'('@+'(X0,X2),'@+'(X1,X2)) ),
inference(flattening,[],[f579]) ).
fof(f599,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| '@+'(X1,X2) != '@+'(X0,X2) ),
inference(ennf_transformation,[],[f228]) ).
fof(f600,plain,
! [X0,X1,X2] :
( X0 = X1
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X2)
| '@+'(X1,X2) != '@+'(X0,X2) ),
inference(flattening,[],[f599]) ).
fof(f645,plain,
! [X0] :
( nat_succeeds(lh(X0))
| ~ list_succeeds(X0) ),
inference(ennf_transformation,[],[f263]) ).
fof(f646,plain,
! [X0] :
( X0 = nil
| ~ list_succeeds(X0)
| '0' != lh(X0) ),
inference(ennf_transformation,[],[f264]) ).
fof(f647,plain,
! [X0] :
( X0 = nil
| ~ list_succeeds(X0)
| '0' != lh(X0) ),
inference(flattening,[],[f646]) ).
fof(f801,plain,
! [X0,X1] :
( ( lh(X0) = X1
<=> length_succeeds(X0,X1) )
| ~ list_succeeds(X0) ),
inference(ennf_transformation,[],[f361]) ).
fof(f805,plain,
! [X0,X1,X2] :
( ( list_succeeds(X0)
& list_succeeds(X1)
& list_succeeds(X2) )
| ~ split_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f365]) ).
fof(f806,plain,
! [X0,X1,X2] :
( lh(X0) = '@+'(lh(X1),lh(X2))
| ~ split_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f366]) ).
fof(f819,plain,
? [X0,X1,X2,X3,X4] :
( ( ~ '@<_succeeds'(lh(X3),lh(cons(X0,cons(X1,X2))))
| ~ '@<_succeeds'(lh(X4),lh(cons(X0,cons(X1,X2)))) )
& split_succeeds(cons(X0,cons(X1,X2)),X3,X4) ),
inference(ennf_transformation,[],[f375]) ).
fof(f820,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f826,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[],[f7]) ).
fof(f827,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f382]) ).
fof(f1037,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| cons(sK61(X0,X1,X2),sK63(X0,X1,X2)) = X1
| nil = X0 ),
inference(cnf_transformation,[],[f73]) ).
fof(f1038,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| cons(sK61(X0,X1,X2),sK62(X0,X1,X2)) = X0
| nil = X0 ),
inference(cnf_transformation,[],[f73]) ).
fof(f1039,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| split_succeeds(sK62(X0,X1,X2),X2,sK63(X0,X1,X2))
| nil = X1 ),
inference(cnf_transformation,[],[f73]) ).
fof(f1285,plain,
! [X0,X1] :
( ~ length_succeeds(X0,X1)
| s(sK139(X0,X1)) = X1
| nil = X0 ),
inference(cnf_transformation,[],[f97]) ).
fof(f1432,plain,
! [X0,X1] :
( s(sK193(X0,X1)) = X1
| s(sK195(X0,X1)) = X1
| ~ '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
fof(f1453,plain,
! [X0] :
( '0' != X0
| nat_succeeds(X0) ),
inference(cnf_transformation,[],[f124]) ).
fof(f1486,plain,
! [X0] : '@+'('0',X0) = X0,
inference(cnf_transformation,[],[f152]) ).
fof(f1523,plain,
! [X0,X1] :
( ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| '@<_succeeds'(X1,X0)
| X0 = X1
| '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f534]) ).
fof(f1524,plain,
! [X0] :
( '0' = X0
| ~ nat_succeeds(X0)
| '@<_succeeds'('0',X0) ),
inference(cnf_transformation,[],[f536]) ).
fof(f1537,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'(X1,X2)
| ~ '@=<_succeeds'(X0,X1)
| '@<_succeeds'(X0,X2) ),
inference(cnf_transformation,[],[f554]) ).
fof(f1543,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'(X1,X2)
| ~ nat_succeeds(X0)
| '@<_succeeds'('@+'(X0,X1),'@+'(X0,X2)) ),
inference(cnf_transformation,[],[f564]) ).
fof(f1549,plain,
! [X0,X1] :
( ~ nat_succeeds(X0)
| '@=<_succeeds'(X0,'@+'(X0,X1)) ),
inference(cnf_transformation,[],[f574]) ).
fof(f1552,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'('@+'(X0,X2),'@+'(X1,X2))
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| '@<_succeeds'(X0,X1) ),
inference(cnf_transformation,[],[f580]) ).
fof(f1562,plain,
! [X2,X0,X1] :
( '@+'(X1,X2) != '@+'(X0,X2)
| ~ nat_succeeds(X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f600]) ).
fof(f1601,plain,
! [X0] :
( ~ list_succeeds(X0)
| nat_succeeds(lh(X0)) ),
inference(cnf_transformation,[],[f645]) ).
fof(f1602,plain,
! [X0] :
( '0' != lh(X0)
| ~ list_succeeds(X0)
| nil = X0 ),
inference(cnf_transformation,[],[f647]) ).
fof(f1709,plain,
! [X0,X1] :
( ~ list_succeeds(X0)
| length_succeeds(X0,X1)
| lh(X0) != X1 ),
inference(cnf_transformation,[],[f801]) ).
fof(f1716,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| list_succeeds(X2) ),
inference(cnf_transformation,[],[f805]) ).
fof(f1717,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| list_succeeds(X1) ),
inference(cnf_transformation,[],[f805]) ).
fof(f1718,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| list_succeeds(X0) ),
inference(cnf_transformation,[],[f805]) ).
fof(f1719,plain,
! [X2,X0,X1] :
( ~ split_succeeds(X0,X1,X2)
| lh(X0) = '@+'(lh(X1),lh(X2)) ),
inference(cnf_transformation,[],[f806]) ).
fof(f1727,plain,
( ~ '@<_succeeds'(lh(sK231),lh(cons(sK227,cons(sK228,sK229))))
| ~ '@<_succeeds'(lh(sK230),lh(cons(sK227,cons(sK228,sK229)))) ),
inference(cnf_transformation,[],[f819]) ).
fof(f1728,plain,
split_succeeds(cons(sK227,cons(sK228,sK229)),sK230,sK231),
inference(cnf_transformation,[],[f819]) ).
fof(f1924,plain,
nat_succeeds('0'),
inference(equality_resolution,[],[f1453]) ).
fof(f1934,plain,
! [X0] :
( ~ list_succeeds(X0)
| length_succeeds(X0,lh(X0)) ),
inference(equality_resolution,[],[f1709]) ).
fof(f2349,plain,
! [X0,X1] :
( '@<_succeeds'(X0,X1)
| s(sK195(X0,X1)) = X1
| s(sK193(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f1432]) ).
fof(f2362,plain,
~ nat_succeeds('0'),
inference(consistent_polarity_flipping,[],[f1924]) ).
fof(f2425,plain,
! [X0,X1] :
( ~ '@<_succeeds'(X0,X1)
| nat_succeeds(X0)
| ~ '@<_succeeds'(X1,X0)
| X0 = X1
| nat_succeeds(X1) ),
inference(consistent_polarity_flipping,[],[f1523]) ).
fof(f2426,plain,
! [X0] :
( ~ '@<_succeeds'('0',X0)
| nat_succeeds(X0)
| '0' = X0 ),
inference(consistent_polarity_flipping,[],[f1524]) ).
fof(f2439,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'(X0,X2)
| '@=<_succeeds'(X0,X1)
| '@<_succeeds'(X1,X2) ),
inference(consistent_polarity_flipping,[],[f1537]) ).
fof(f2445,plain,
! [X2,X0,X1] :
( ~ '@<_succeeds'('@+'(X0,X1),'@+'(X0,X2))
| nat_succeeds(X0)
| '@<_succeeds'(X1,X2) ),
inference(consistent_polarity_flipping,[],[f1543]) ).
fof(f2451,plain,
! [X0,X1] :
( ~ '@=<_succeeds'(X0,'@+'(X0,X1))
| nat_succeeds(X0) ),
inference(consistent_polarity_flipping,[],[f1549]) ).
fof(f2454,plain,
! [X2,X0,X1] :
( '@<_succeeds'('@+'(X0,X2),'@+'(X1,X2))
| nat_succeeds(X2)
| nat_succeeds(X1)
| nat_succeeds(X0)
| ~ '@<_succeeds'(X0,X1) ),
inference(consistent_polarity_flipping,[],[f1552]) ).
fof(f2464,plain,
! [X2,X0,X1] :
( '@+'(X1,X2) != '@+'(X0,X2)
| nat_succeeds(X2)
| nat_succeeds(X1)
| nat_succeeds(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f1562]) ).
fof(f2493,plain,
! [X0] :
( ~ nat_succeeds(lh(X0))
| list_succeeds(X0) ),
inference(consistent_polarity_flipping,[],[f1601]) ).
fof(f2494,plain,
! [X0] :
( '0' != lh(X0)
| list_succeeds(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f1602]) ).
fof(f2582,plain,
! [X0] :
( length_succeeds(X0,lh(X0))
| list_succeeds(X0) ),
inference(consistent_polarity_flipping,[],[f1934]) ).
fof(f2590,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X0)
| ~ split_succeeds(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f1718]) ).
fof(f2591,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X1)
| ~ split_succeeds(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f1717]) ).
fof(f2592,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X2)
| ~ split_succeeds(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f1716]) ).
fof(f2600,plain,
( '@<_succeeds'(lh(sK231),lh(cons(sK227,cons(sK228,sK229))))
| '@<_succeeds'(lh(sK230),lh(cons(sK227,cons(sK228,sK229)))) ),
inference(consistent_polarity_flipping,[],[f1727]) ).
fof(f2602,definition,
( spl232_1
<=> '@<_succeeds'(lh(sK230),lh(cons(sK227,cons(sK228,sK229)))) ),
introduced(definition,[new_symbols(definition,[spl232_1])],[avatar_definition]) ).
fof(f2604,plain,
( '@<_succeeds'(lh(sK230),lh(cons(sK227,cons(sK228,sK229))))
| ~ spl232_1 ),
inference(avatar_component_clause,[],[f2602]) ).
fof(f2606,definition,
( spl232_2
<=> '@<_succeeds'(lh(sK231),lh(cons(sK227,cons(sK228,sK229)))) ),
introduced(definition,[new_symbols(definition,[spl232_2])],[avatar_definition]) ).
fof(f2608,plain,
( '@<_succeeds'(lh(sK231),lh(cons(sK227,cons(sK228,sK229))))
| ~ spl232_2 ),
inference(avatar_component_clause,[],[f2606]) ).
fof(f2609,plain,
( spl232_1
| spl232_2 ),
inference(avatar_split_clause,[],[f2600,f2606,f2602]) ).
fof(f3485,plain,
( ! [X0] :
( '@<_succeeds'(X0,lh(cons(sK227,cons(sK228,sK229))))
| '@=<_succeeds'(lh(sK230),X0) )
| ~ spl232_1 ),
inference(resolution,[],[f2604,f2439]) ).
fof(f3528,definition,
( spl232_87
<=> list_succeeds(cons(sK227,cons(sK228,sK229))) ),
introduced(definition,[new_symbols(definition,[spl232_87])],[avatar_definition]) ).
fof(f3529,plain,
( ~ list_succeeds(cons(sK227,cons(sK228,sK229)))
| spl232_87 ),
inference(avatar_component_clause,[],[f3528]) ).
fof(f3530,plain,
( list_succeeds(cons(sK227,cons(sK228,sK229)))
| ~ spl232_87 ),
inference(avatar_component_clause,[],[f3528]) ).
fof(f3593,definition,
( spl232_92
<=> nat_succeeds(lh(sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_92])],[avatar_definition]) ).
fof(f3594,plain,
( ~ nat_succeeds(lh(sK231))
| spl232_92 ),
inference(avatar_component_clause,[],[f3593]) ).
fof(f3595,plain,
( nat_succeeds(lh(sK231))
| ~ spl232_92 ),
inference(avatar_component_clause,[],[f3593]) ).
fof(f3621,plain,
( list_succeeds(sK231)
| ~ spl232_92 ),
inference(resolution,[],[f3595,f2493]) ).
fof(f3738,definition,
( spl232_101
<=> '0' = lh(sK231) ),
introduced(definition,[new_symbols(definition,[spl232_101])],[avatar_definition]) ).
fof(f3740,plain,
( '0' = lh(sK231)
| ~ spl232_101 ),
inference(avatar_component_clause,[],[f3738]) ).
fof(f3887,plain,
( ! [X0,X1] : ~ split_succeeds(X0,X1,sK231)
| ~ spl232_92 ),
inference(resolution,[],[f3621,f2592]) ).
fof(f4299,plain,
lh(cons(sK227,cons(sK228,sK229))) = '@+'(lh(sK230),lh(sK231)),
inference(resolution,[],[f1719,f1728]) ).
fof(f4330,plain,
( $false
| ~ spl232_92 ),
inference(backward_subsumption_resolution,[],[f1728,f3887]) ).
fof(f4332,plain,
~ spl232_92,
inference(avatar_contradiction_clause,[],[f4330]) ).
fof(f4479,plain,
( '0' != '0'
| list_succeeds(sK231)
| nil = sK231
| ~ spl232_101 ),
inference(superposition,[],[f2494,f3740]) ).
fof(f4699,definition,
( spl232_108
<=> list_succeeds(sK231) ),
introduced(definition,[new_symbols(definition,[spl232_108])],[avatar_definition]) ).
fof(f4700,plain,
( ~ list_succeeds(sK231)
| spl232_108 ),
inference(avatar_component_clause,[],[f4699]) ).
fof(f4701,plain,
( list_succeeds(sK231)
| ~ spl232_108 ),
inference(avatar_component_clause,[],[f4699]) ).
fof(f4708,definition,
( spl232_110
<=> nil = sK231 ),
introduced(definition,[new_symbols(definition,[spl232_110])],[avatar_definition]) ).
fof(f4710,plain,
( nil = sK231
| ~ spl232_110 ),
inference(avatar_component_clause,[],[f4708]) ).
fof(f4846,definition,
( spl232_114
<=> nat_succeeds(lh(sK230)) ),
introduced(definition,[new_symbols(definition,[spl232_114])],[avatar_definition]) ).
fof(f4847,plain,
( ~ nat_succeeds(lh(sK230))
| spl232_114 ),
inference(avatar_component_clause,[],[f4846]) ).
fof(f4848,plain,
( nat_succeeds(lh(sK230))
| ~ spl232_114 ),
inference(avatar_component_clause,[],[f4846]) ).
fof(f4948,plain,
( ! [X0,X1] : ~ split_succeeds(cons(sK227,cons(sK228,sK229)),X0,X1)
| ~ spl232_87 ),
inference(resolution,[],[f3530,f2590]) ).
fof(f5634,plain,
! [X0,X1] :
( '@<_succeeds'('@+'(X1,X0),X0)
| nat_succeeds(X0)
| nat_succeeds('0')
| nat_succeeds(X1)
| ~ '@<_succeeds'(X1,'0') ),
inference(superposition,[],[f2454,f1486]) ).
fof(f5641,plain,
! [X0,X1] :
( '@<_succeeds'('@+'(X1,X0),X0)
| nat_succeeds(X0)
| nat_succeeds(X1)
| ~ '@<_succeeds'(X1,'0') ),
inference(forward_subsumption_resolution,[],[f5634,f2362]) ).
fof(f5655,plain,
! [X0,X1] :
( '@+'(X1,X0) != X0
| nat_succeeds(X0)
| nat_succeeds(X1)
| nat_succeeds('0')
| '0' = X1 ),
inference(superposition,[],[f2464,f1486]) ).
fof(f5658,plain,
! [X0,X1] :
( '@+'(X1,X0) != X0
| nat_succeeds(X0)
| nat_succeeds(X1)
| '0' = X1 ),
inference(forward_subsumption_resolution,[],[f5655,f2362]) ).
fof(f5712,definition,
( spl232_118
<=> nil = sK230 ),
introduced(definition,[new_symbols(definition,[spl232_118])],[avatar_definition]) ).
fof(f5713,plain,
( nil != sK230
| spl232_118 ),
inference(avatar_component_clause,[],[f5712]) ).
fof(f5716,definition,
( spl232_119
<=> split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil)) ),
introduced(definition,[new_symbols(definition,[spl232_119])],[avatar_definition]) ).
fof(f5718,plain,
( split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil))
| ~ spl232_119 ),
inference(avatar_component_clause,[],[f5716]) ).
fof(f5724,definition,
( spl232_120
<=> lh(sK231) = lh(cons(sK227,cons(sK228,sK229))) ),
introduced(definition,[new_symbols(definition,[spl232_120])],[avatar_definition]) ).
fof(f5725,plain,
( lh(sK231) != lh(cons(sK227,cons(sK228,sK229)))
| spl232_120 ),
inference(avatar_component_clause,[],[f5724]) ).
fof(f5726,plain,
( lh(sK231) = lh(cons(sK227,cons(sK228,sK229)))
| ~ spl232_120 ),
inference(avatar_component_clause,[],[f5724]) ).
fof(f5728,definition,
( spl232_121
<=> '@<_succeeds'(lh(cons(sK227,cons(sK228,sK229))),lh(sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_121])],[avatar_definition]) ).
fof(f5729,plain,
( '@<_succeeds'(lh(cons(sK227,cons(sK228,sK229))),lh(sK231))
| ~ spl232_121 ),
inference(avatar_component_clause,[],[f5728]) ).
fof(f5730,plain,
( ~ '@<_succeeds'(lh(cons(sK227,cons(sK228,sK229))),lh(sK231))
| spl232_121 ),
inference(avatar_component_clause,[],[f5728]) ).
fof(f5733,definition,
( spl232_122
<=> split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK231,sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_122])],[avatar_definition]) ).
fof(f5735,plain,
( split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK231,sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231))
| ~ spl232_122 ),
inference(avatar_component_clause,[],[f5733]) ).
fof(f6107,definition,
( spl232_129
<=> cons(sK227,cons(sK228,sK229)) = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,nil),sK62(cons(sK227,cons(sK228,sK229)),sK230,nil)) ),
introduced(definition,[new_symbols(definition,[spl232_129])],[avatar_definition]) ).
fof(f6109,plain,
( cons(sK227,cons(sK228,sK229)) = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,nil),sK62(cons(sK227,cons(sK228,sK229)),sK230,nil))
| ~ spl232_129 ),
inference(avatar_component_clause,[],[f6107]) ).
fof(f6933,plain,
( $false
| ~ spl232_87 ),
inference(backward_subsumption_resolution,[],[f1728,f4948]) ).
fof(f6935,plain,
~ spl232_87,
inference(avatar_contradiction_clause,[],[f6933]) ).
fof(f6940,plain,
( split_succeeds(cons(sK227,cons(sK228,sK229)),sK230,nil)
| ~ spl232_110 ),
inference(forward_demodulation,[],[f1728,f4710]) ).
fof(f6953,plain,
( cons(sK227,cons(sK228,sK229)) = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,nil),sK62(cons(sK227,cons(sK228,sK229)),sK230,nil))
| nil = cons(sK227,cons(sK228,sK229))
| ~ spl232_110 ),
inference(resolution,[],[f6940,f1038]) ).
fof(f6954,plain,
( split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil))
| nil = sK230
| ~ spl232_110 ),
inference(resolution,[],[f6940,f1039]) ).
fof(f6965,plain,
( split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil))
| ~ spl232_110
| spl232_118 ),
inference(forward_subsumption_resolution,[],[f6954,f5713]) ).
fof(f6966,plain,
( cons(sK227,cons(sK228,sK229)) = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,nil),sK62(cons(sK227,cons(sK228,sK229)),sK230,nil))
| ~ spl232_110 ),
inference(forward_subsumption_resolution,[],[f6953,f826]) ).
fof(f6971,plain,
( spl232_119
| ~ spl232_110
| spl232_118 ),
inference(avatar_split_clause,[],[f6965,f5712,f4708,f5716]) ).
fof(f6972,plain,
( spl232_129
| ~ spl232_110 ),
inference(avatar_split_clause,[],[f6966,f4708,f6107]) ).
fof(f7332,plain,
( list_succeeds(sK230)
| ~ spl232_114 ),
inference(resolution,[],[f4848,f2493]) ).
fof(f7537,definition,
( spl232_147
<=> '0' = lh(sK230) ),
introduced(definition,[new_symbols(definition,[spl232_147])],[avatar_definition]) ).
fof(f7539,plain,
( '0' = lh(sK230)
| ~ spl232_147 ),
inference(avatar_component_clause,[],[f7537]) ).
fof(f7749,plain,
( length_succeeds(sK230,'0')
| list_succeeds(sK230)
| ~ spl232_147 ),
inference(superposition,[],[f2582,f7539]) ).
fof(f7753,definition,
( spl232_157
<=> list_succeeds(sK230) ),
introduced(definition,[new_symbols(definition,[spl232_157])],[avatar_definition]) ).
fof(f7754,plain,
( ~ list_succeeds(sK230)
| spl232_157 ),
inference(avatar_component_clause,[],[f7753]) ).
fof(f7755,plain,
( list_succeeds(sK230)
| ~ spl232_157 ),
inference(avatar_component_clause,[],[f7753]) ).
fof(f7757,definition,
( spl232_158
<=> length_succeeds(sK230,'0') ),
introduced(definition,[new_symbols(definition,[spl232_158])],[avatar_definition]) ).
fof(f7759,plain,
( length_succeeds(sK230,'0')
| ~ spl232_158 ),
inference(avatar_component_clause,[],[f7757]) ).
fof(f8441,plain,
( ! [X0,X1] : ~ split_succeeds(X0,sK230,X1)
| ~ spl232_157 ),
inference(resolution,[],[f7755,f2591]) ).
fof(f8761,plain,
( nil = cons(sK61(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil)),sK63(sK62(cons(sK227,cons(sK228,sK229)),sK230,nil),nil,sK63(cons(sK227,cons(sK228,sK229)),sK230,nil)))
| nil = sK62(cons(sK227,cons(sK228,sK229)),sK230,nil)
| ~ spl232_119 ),
inference(resolution,[],[f5718,f1037]) ).
fof(f8787,definition,
( spl232_224
<=> nil = sK62(cons(sK227,cons(sK228,sK229)),sK230,nil) ),
introduced(definition,[new_symbols(definition,[spl232_224])],[avatar_definition]) ).
fof(f8789,plain,
( nil = sK62(cons(sK227,cons(sK228,sK229)),sK230,nil)
| ~ spl232_224 ),
inference(avatar_component_clause,[],[f8787]) ).
fof(f8791,plain,
( nil = sK62(cons(sK227,cons(sK228,sK229)),sK230,nil)
| ~ spl232_119 ),
inference(forward_subsumption_resolution,[],[f8761,f826]) ).
fof(f8794,plain,
( spl232_224
| ~ spl232_119 ),
inference(avatar_split_clause,[],[f8791,f5716,f8787]) ).
fof(f9130,plain,
( ! [X0,X1] :
( cons(X0,X1) != cons(sK227,cons(sK228,sK229))
| sK62(cons(sK227,cons(sK228,sK229)),sK230,nil) = X1 )
| ~ spl232_129 ),
inference(superposition,[],[f827,f6109]) ).
fof(f103863,definition,
( spl232_1887
<=> sK230 = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_1887])],[avatar_definition]) ).
fof(f103865,plain,
( sK230 = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231))
| ~ spl232_1887 ),
inference(avatar_component_clause,[],[f103863]) ).
fof(f106026,plain,
( sK230 = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231))
| nil = cons(sK227,cons(sK228,sK229)) ),
inference(resolution,[],[f1728,f1037]) ).
fof(f106028,plain,
( split_succeeds(sK62(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK231,sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231))
| nil = sK230 ),
inference(resolution,[],[f1728,f1039]) ).
fof(f106124,plain,
sK230 = cons(sK61(cons(sK227,cons(sK228,sK229)),sK230,sK231),sK63(cons(sK227,cons(sK228,sK229)),sK230,sK231)),
inference(forward_subsumption_resolution,[],[f106026,f826]) ).
fof(f106135,plain,
spl232_1887,
inference(avatar_split_clause,[],[f106124,f103863]) ).
fof(f106673,plain,
( ! [X0,X1] : ~ split_succeeds(X0,sK231,X1)
| ~ spl232_108 ),
inference(resolution,[],[f4701,f2591]) ).
fof(f107695,plain,
( nil != sK230
| ~ spl232_1887 ),
inference(superposition,[],[f826,f103865]) ).
fof(f109570,definition,
( spl232_2317
<=> ! [X1] : '@<_succeeds'(X1,lh(sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_2317])],[avatar_definition]) ).
fof(f109571,plain,
( ! [X1] : '@<_succeeds'(X1,lh(sK231))
| ~ spl232_2317 ),
inference(avatar_component_clause,[],[f109570]) ).
fof(f114670,plain,
( nat_succeeds(lh(sK231))
| '0' = lh(sK231)
| ~ spl232_2317 ),
inference(resolution,[],[f109571,f2426]) ).
fof(f114735,plain,
( '0' = lh(sK231)
| spl232_92
| ~ spl232_2317 ),
inference(forward_subsumption_resolution,[],[f114670,f3594]) ).
fof(f114753,plain,
( spl232_101
| spl232_92
| ~ spl232_2317 ),
inference(avatar_split_clause,[],[f114735,f109570,f3593,f3738]) ).
fof(f116856,plain,
( $false
| ~ spl232_157 ),
inference(backward_subsumption_resolution,[],[f1728,f8441]) ).
fof(f116857,plain,
~ spl232_157,
inference(avatar_contradiction_clause,[],[f116856]) ).
fof(f127696,plain,
( $false
| ~ spl232_108
| ~ spl232_122 ),
inference(backward_subsumption_resolution,[],[f5735,f106673]) ).
fof(f127697,plain,
( ~ spl232_108
| ~ spl232_122 ),
inference(avatar_contradiction_clause,[],[f127696]) ).
fof(f127783,plain,
( $false
| ~ spl232_114
| spl232_157 ),
inference(forward_subsumption_resolution,[],[f7332,f7754]) ).
fof(f127784,plain,
( ~ spl232_114
| spl232_157 ),
inference(avatar_contradiction_clause,[],[f127783]) ).
fof(f137592,plain,
( lh(sK231) = '@+'(lh(sK230),lh(sK231))
| ~ spl232_120 ),
inference(forward_demodulation,[],[f4299,f5726]) ).
fof(f137672,plain,
( lh(sK231) != lh(sK231)
| nat_succeeds(lh(sK231))
| nat_succeeds(lh(sK230))
| '0' = lh(sK230)
| ~ spl232_120 ),
inference(superposition,[],[f5658,f137592]) ).
fof(f137673,plain,
( nat_succeeds(lh(sK231))
| nat_succeeds(lh(sK230))
| '0' = lh(sK230)
| ~ spl232_120 ),
inference(trivial_inequality_removal,[],[f137672]) ).
fof(f137674,plain,
( nat_succeeds(lh(sK230))
| '0' = lh(sK230)
| spl232_92
| ~ spl232_120 ),
inference(forward_subsumption_resolution,[],[f137673,f3594]) ).
fof(f137728,plain,
( '0' = lh(sK230)
| spl232_92
| spl232_114
| ~ spl232_120 ),
inference(forward_subsumption_resolution,[],[f137674,f4847]) ).
fof(f138422,plain,
( lh(sK231) != '@+'(lh(sK230),lh(sK231))
| spl232_120 ),
inference(superposition,[],[f5725,f4299]) ).
fof(f138434,plain,
( ~ nat_succeeds('@+'(lh(sK230),lh(sK231)))
| list_succeeds(cons(sK227,cons(sK228,sK229))) ),
inference(superposition,[],[f2493,f4299]) ).
fof(f138521,plain,
( ~ nat_succeeds('@+'(lh(sK230),lh(sK231)))
| spl232_87 ),
inference(forward_subsumption_resolution,[],[f138434,f3529]) ).
fof(f138548,definition,
( spl232_4108
<=> nat_succeeds('@+'(lh(sK230),lh(sK231))) ),
introduced(definition,[new_symbols(definition,[spl232_4108])],[avatar_definition]) ).
fof(f138549,plain,
( ~ nat_succeeds('@+'(lh(sK230),lh(sK231)))
| spl232_4108 ),
inference(avatar_component_clause,[],[f138548]) ).
fof(f139833,definition,
( spl232_4230
<=> lh(sK231) = '@+'(lh(sK230),lh(sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_4230])],[avatar_definition]) ).
fof(f139837,definition,
( spl232_4231
<=> '@<_succeeds'(lh(sK231),'@+'(lh(sK230),lh(sK231))) ),
introduced(definition,[new_symbols(definition,[spl232_4231])],[avatar_definition]) ).
fof(f139878,plain,
( '@<_succeeds'(lh(sK231),'@+'(lh(sK230),lh(sK231)))
| ~ spl232_2 ),
inference(forward_demodulation,[],[f2608,f4299]) ).
fof(f139964,plain,
( ~ '@<_succeeds'('@+'(lh(sK230),lh(sK231)),lh(sK231))
| spl232_121 ),
inference(forward_demodulation,[],[f5730,f4299]) ).
fof(f139972,plain,
( spl232_4231
| ~ spl232_2 ),
inference(avatar_split_clause,[],[f139878,f2606,f139837]) ).
fof(f140101,plain,
( nat_succeeds(lh(sK231))
| nat_succeeds(lh(sK230))
| ~ '@<_succeeds'(lh(sK230),'0')
| spl232_121 ),
inference(resolution,[],[f139964,f5641]) ).
fof(f140394,plain,
( nat_succeeds(lh(sK230))
| ~ '@<_succeeds'(lh(sK230),'0')
| spl232_92
| spl232_121 ),
inference(forward_subsumption_resolution,[],[f140101,f3594]) ).
fof(f140790,plain,
( '@<_succeeds'('@+'(lh(sK230),lh(sK231)),lh(sK231))
| ~ spl232_121 ),
inference(forward_demodulation,[],[f5729,f4299]) ).
fof(f142661,plain,
( ~ spl232_4108
| spl232_87 ),
inference(avatar_split_clause,[],[f138521,f3528,f138548]) ).
fof(f149896,plain,
( ~ spl232_4230
| spl232_120 ),
inference(avatar_split_clause,[],[f138422,f5724,f139833]) ).
fof(f150166,plain,
( ~ '@<_succeeds'(lh(sK230),'0')
| spl232_92
| spl232_114
| spl232_121 ),
inference(forward_subsumption_resolution,[],[f140394,f4847]) ).
fof(f150277,definition,
( spl232_4600
<=> '@<_succeeds'(lh(sK230),'0') ),
introduced(definition,[new_symbols(definition,[spl232_4600])],[avatar_definition]) ).
fof(f150278,plain,
( ~ '@<_succeeds'(lh(sK230),'0')
| spl232_4600 ),
inference(avatar_component_clause,[],[f150277]) ).
fof(f150422,plain,
( ~ spl232_4600
| spl232_92
| spl232_114
| spl232_121 ),
inference(avatar_split_clause,[],[f150166,f5728,f4846,f3593,f150277]) ).
fof(f151128,plain,
( '0' = s(sK195(lh(sK230),'0'))
| '0' = s(sK193(lh(sK230),'0'))
| spl232_4600 ),
inference(resolution,[],[f150278,f2349]) ).
fof(f151363,plain,
( '0' = s(sK195(lh(sK230),'0'))
| spl232_4600 ),
inference(forward_subsumption_resolution,[],[f151128,f820]) ).
fof(f151426,plain,
( $false
| spl232_4600 ),
inference(forward_subsumption_resolution,[],[f151363,f820]) ).
fof(f151427,plain,
spl232_4600,
inference(avatar_contradiction_clause,[],[f151426]) ).
fof(f151580,plain,
( spl232_147
| spl232_92
| spl232_114
| ~ spl232_120 ),
inference(avatar_split_clause,[],[f137728,f5724,f4846,f3593,f7537]) ).
fof(f151689,plain,
( length_succeeds(sK230,'0')
| ~ spl232_147
| spl232_157 ),
inference(forward_subsumption_resolution,[],[f7749,f7754]) ).
fof(f152102,plain,
( ~ spl232_118
| ~ spl232_1887 ),
inference(avatar_split_clause,[],[f107695,f103863,f5712]) ).
fof(f152429,plain,
( spl232_158
| ~ spl232_147
| spl232_157 ),
inference(avatar_split_clause,[],[f151689,f7753,f7537,f7757]) ).
fof(f152635,definition,
( spl232_4648
<=> '@<_succeeds'('@+'(lh(sK230),lh(sK231)),lh(sK231)) ),
introduced(definition,[new_symbols(definition,[spl232_4648])],[avatar_definition]) ).
fof(f152636,plain,
( '@<_succeeds'('@+'(lh(sK230),lh(sK231)),lh(sK231))
| ~ spl232_4648 ),
inference(avatar_component_clause,[],[f152635]) ).
fof(f152825,plain,
( list_succeeds(sK231)
| nil = sK231
| ~ spl232_101 ),
inference(trivial_inequality_removal,[],[f4479]) ).
fof(f152918,plain,
( ! [X0] :
( '@<_succeeds'(X0,'@+'(lh(sK230),lh(sK231)))
| '@=<_succeeds'(lh(sK230),X0) )
| ~ spl232_1 ),
inference(forward_demodulation,[],[f3485,f4299]) ).
fof(f154738,plain,
( nil = sK231
| ~ spl232_101
| spl232_108 ),
inference(forward_subsumption_resolution,[],[f152825,f4700]) ).
fof(f157682,plain,
( spl232_118
| spl232_122 ),
inference(avatar_split_clause,[],[f106028,f5733,f5712]) ).
fof(f158483,plain,
( spl232_110
| ~ spl232_101
| spl232_108 ),
inference(avatar_split_clause,[],[f154738,f4699,f3738,f4708]) ).
fof(f160484,plain,
( '0' = s(sK139(sK230,'0'))
| nil = sK230
| ~ spl232_158 ),
inference(resolution,[],[f7759,f1285]) ).
fof(f160558,plain,
( nil = sK230
| ~ spl232_158 ),
inference(forward_subsumption_resolution,[],[f160484,f820]) ).
fof(f160563,plain,
( $false
| spl232_118
| ~ spl232_158 ),
inference(forward_subsumption_resolution,[],[f160558,f5713]) ).
fof(f160564,plain,
( spl232_118
| ~ spl232_158 ),
inference(avatar_contradiction_clause,[],[f160563]) ).
fof(f160565,plain,
( spl232_4648
| ~ spl232_121 ),
inference(avatar_split_clause,[],[f140790,f5728,f152635]) ).
fof(f160569,plain,
( nat_succeeds('@+'(lh(sK230),lh(sK231)))
| ~ '@<_succeeds'(lh(sK231),'@+'(lh(sK230),lh(sK231)))
| lh(sK231) = '@+'(lh(sK230),lh(sK231))
| nat_succeeds(lh(sK231))
| ~ spl232_4648 ),
inference(resolution,[],[f152636,f2425]) ).
fof(f160628,plain,
( ~ '@<_succeeds'(lh(sK231),'@+'(lh(sK230),lh(sK231)))
| lh(sK231) = '@+'(lh(sK230),lh(sK231))
| nat_succeeds(lh(sK231))
| spl232_4108
| ~ spl232_4648 ),
inference(forward_subsumption_resolution,[],[f160569,f138549]) ).
fof(f160653,plain,
( ~ '@<_succeeds'(lh(sK231),'@+'(lh(sK230),lh(sK231)))
| lh(sK231) = '@+'(lh(sK230),lh(sK231))
| spl232_92
| spl232_4108
| ~ spl232_4648 ),
inference(forward_subsumption_resolution,[],[f160628,f3594]) ).
fof(f160674,plain,
( spl232_4230
| ~ spl232_4231
| spl232_92
| spl232_4108
| ~ spl232_4648 ),
inference(avatar_split_clause,[],[f160653,f152635,f138548,f3593,f139837,f139833]) ).
fof(f161157,plain,
( ! [X0] :
( '@=<_succeeds'(lh(sK230),'@+'(lh(sK230),X0))
| nat_succeeds(lh(sK230))
| '@<_succeeds'(X0,lh(sK231)) )
| ~ spl232_1 ),
inference(resolution,[],[f152918,f2445]) ).
fof(f161245,plain,
( ! [X0] :
( nat_succeeds(lh(sK230))
| '@<_succeeds'(X0,lh(sK231)) )
| ~ spl232_1 ),
inference(forward_subsumption_resolution,[],[f161157,f2451]) ).
fof(f161262,plain,
( ! [X0] : '@<_succeeds'(X0,lh(sK231))
| ~ spl232_1
| spl232_114 ),
inference(forward_subsumption_resolution,[],[f161245,f4847]) ).
fof(f161270,plain,
( spl232_2317
| ~ spl232_1
| spl232_114 ),
inference(avatar_split_clause,[],[f161262,f4846,f2602,f109570]) ).
fof(f308578,plain,
( cons(sK228,sK229) = sK62(cons(sK227,cons(sK228,sK229)),sK230,nil)
| ~ spl232_129 ),
inference(equality_resolution,[],[f9130]) ).
fof(f308581,plain,
( nil = cons(sK228,sK229)
| ~ spl232_129
| ~ spl232_224 ),
inference(forward_demodulation,[],[f308578,f8789]) ).
fof(f308594,plain,
( $false
| ~ spl232_129
| ~ spl232_224 ),
inference(forward_subsumption_resolution,[],[f308581,f826]) ).
fof(f308595,plain,
( ~ spl232_129
| ~ spl232_224 ),
inference(avatar_contradiction_clause,[],[f308594]) ).
cnf(s1,plain,
( spl232_1
| spl232_2 ),
inference(sat_conversion,[],[f2609]) ).
cnf(s110,plain,
~ spl232_92,
inference(sat_conversion,[],[f4332]) ).
cnf(s147,plain,
~ spl232_87,
inference(sat_conversion,[],[f6935]) ).
cnf(s154,plain,
( ~ spl232_110
| spl232_118
| spl232_119 ),
inference(sat_conversion,[],[f6971]) ).
cnf(s155,plain,
( ~ spl232_110
| spl232_129 ),
inference(sat_conversion,[],[f6972]) ).
cnf(s298,plain,
( ~ spl232_119
| spl232_224 ),
inference(sat_conversion,[],[f8794]) ).
cnf(s4151,plain,
spl232_1887,
inference(sat_conversion,[],[f106135]) ).
cnf(s5139,plain,
( spl232_92
| spl232_101
| ~ spl232_2317 ),
inference(sat_conversion,[],[f114753]) ).
cnf(s5288,plain,
~ spl232_157,
inference(sat_conversion,[],[f116857]) ).
cnf(s6424,plain,
( ~ spl232_108
| ~ spl232_122 ),
inference(sat_conversion,[],[f127697]) ).
cnf(s6439,plain,
( ~ spl232_114
| spl232_157 ),
inference(sat_conversion,[],[f127784]) ).
cnf(s9833,plain,
( ~ spl232_2
| spl232_4231 ),
inference(sat_conversion,[],[f139972]) ).
cnf(s10318,plain,
( spl232_87
| ~ spl232_4108 ),
inference(sat_conversion,[],[f142661]) ).
cnf(s11588,plain,
( spl232_120
| ~ spl232_4230 ),
inference(sat_conversion,[],[f149896]) ).
cnf(s11772,plain,
( spl232_92
| spl232_114
| spl232_121
| ~ spl232_4600 ),
inference(sat_conversion,[],[f150422]) ).
cnf(s12072,plain,
spl232_4600,
inference(sat_conversion,[],[f151427]) ).
cnf(s12084,plain,
( spl232_92
| spl232_114
| ~ spl232_120
| spl232_147 ),
inference(sat_conversion,[],[f151580]) ).
cnf(s12348,plain,
( ~ spl232_118
| ~ spl232_1887 ),
inference(sat_conversion,[],[f152102]) ).
cnf(s12496,plain,
( ~ spl232_147
| spl232_157
| spl232_158 ),
inference(sat_conversion,[],[f152429]) ).
cnf(s16147,plain,
( spl232_118
| spl232_122 ),
inference(sat_conversion,[],[f157682]) ).
cnf(s16707,plain,
( ~ spl232_101
| spl232_108
| spl232_110 ),
inference(sat_conversion,[],[f158483]) ).
cnf(s18268,plain,
( spl232_118
| ~ spl232_158 ),
inference(sat_conversion,[],[f160564]) ).
cnf(s18269,plain,
( ~ spl232_121
| spl232_4648 ),
inference(sat_conversion,[],[f160565]) ).
cnf(s18288,plain,
( spl232_92
| spl232_4108
| spl232_4230
| ~ spl232_4231
| ~ spl232_4648 ),
inference(sat_conversion,[],[f160674]) ).
cnf(s18348,plain,
( ~ spl232_1
| spl232_114
| spl232_2317 ),
inference(sat_conversion,[],[f161270]) ).
cnf(s36848,plain,
( ~ spl232_129
| ~ spl232_224 ),
inference(sat_conversion,[],[f308595]) ).
cnf(s36912,plain,
( spl232_92
| spl232_114
| spl232_121 ),
inference(rat,[],[s11772,s12072]) ).
cnf(s36948,plain,
~ spl232_114,
inference(rat,[],[s6439,s5288]) ).
cnf(s37303,plain,
~ spl232_118,
inference(rat,[],[s12348,s4151]) ).
cnf(s37330,plain,
~ spl232_158,
inference(rat,[],[s18268,s37303]) ).
cnf(s37339,plain,
spl232_122,
inference(rat,[],[s16147,s37303]) ).
cnf(s37374,plain,
~ spl232_147,
inference(rat,[],[s12496,s5288,s37330]) ).
cnf(s37375,plain,
~ spl232_108,
inference(rat,[],[s6424,s37339]) ).
cnf(s38551,plain,
( ~ spl232_110
| spl232_119 ),
inference(rat,[],[s154,s37303]) ).
cnf(s38554,plain,
~ spl232_4108,
inference(rat,[],[s10318,s147]) ).
cnf(s38704,plain,
~ spl232_120,
inference(rat,[],[s12084,s37374,s36948,s110]) ).
cnf(s38705,plain,
spl232_121,
inference(rat,[],[s36912,s36948,s110]) ).
cnf(s38708,plain,
~ spl232_4230,
inference(rat,[],[s11588,s38704]) ).
cnf(s38709,plain,
spl232_4648,
inference(rat,[],[s18269,s38705]) ).
cnf(s38744,plain,
~ spl232_4231,
inference(rat,[],[s18288,s38709,s110,s38554,s38708]) ).
cnf(s38746,plain,
~ spl232_2,
inference(rat,[],[s9833,s38744]) ).
cnf(s38868,plain,
spl232_1,
inference(rat,[],[s1,s38746]) ).
cnf(s38871,plain,
spl232_2317,
inference(rat,[],[s18348,s36948,s38868]) ).
cnf(s38906,plain,
spl232_101,
inference(rat,[],[s5139,s110,s38871]) ).
cnf(s38976,plain,
spl232_110,
inference(rat,[],[s16707,s37375,s38906]) ).
cnf(s39630,plain,
spl232_129,
inference(rat,[],[s155,s38976]) ).
cnf(s39631,plain,
spl232_119,
inference(rat,[],[s38551,s38976]) ).
cnf(s39826,plain,
~ spl232_224,
inference(rat,[],[s36848,s39630]) ).
cnf(s39828,plain,
$false,
inference(rat,[],[s298,s39826,s39631]) ).
fof(f308601,plain,
$false,
inference(avatar_sat_refutation,[],[s39828]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX029+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 % Computer : n016.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 14:57:03 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.27 Running first-order model finding
% 0.09/0.27 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.57/4.19 % (3684401)Will run a generic schedule for satisfiability detection.
% 27.57/4.19 % (3684411)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1468023585:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.57/4.19 % (3684407)% WARNING: option uhcvi not known.
% 27.57/4.19 % (3684406)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2700512518_2999 on theBenchmark for (2999ds/0Mi)
% 27.57/4.19 % (3684409)dis+10_1_sil=32000:sp=arity:random_seed=1271702903:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.57/4.19 % (3684407)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3398428019:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.57/4.19 % (3684408)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=627410825:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.57/4.19 % (3684410)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3415328733:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.57/4.19 % (3684412)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=671882528:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.57/4.19 % (3684411)Instruction limit reached!
% 27.57/4.19 % (3684411)------------------------------
% 27.57/4.19 % (3684411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.57/4.19 % (3684411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/4.19 % (3684411)CaDiCaL version: 2.1.3
% 27.57/4.19 % (3684411)Termination reason: Instruction limit
% 27.57/4.19 % (3684411)Termination phase: Saturation
% 27.57/4.19 % (3684411)Time elapsed: 0.078 s
% 27.57/4.19 % (3684411)Peak memory usage: 14 MB
% 27.57/4.19 % (3684411)Instructions burned: 131 (million)
% 27.57/4.19 % TRYING [1]
% 27.57/4.19 % TRYING [2]
% 27.57/4.19 % (3684420)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=617686397:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.57/4.19 % (3684410)Instruction limit reached!
% 27.57/4.19 % (3684410)------------------------------
% 27.57/4.19 % (3684410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.57/4.19 % (3684410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/4.19 % (3684410)CaDiCaL version: 2.1.3
% 27.57/4.19 % (3684410)Termination reason: Instruction limit
% 27.57/4.19 % (3684410)Termination phase: Saturation
% 27.57/4.19 % (3684410)Time elapsed: 0.103 s
% 27.57/4.19 % (3684410)Peak memory usage: 13 MB
% 27.57/4.19 % (3684410)Instructions burned: 116 (million)
% 27.57/4.19 % (3684409)Instruction limit reached!
% 27.57/4.19 % (3684409)------------------------------
% 27.57/4.19 % (3684409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.57/4.19 % (3684409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/4.19 % (3684409)CaDiCaL version: 2.1.3
% 27.57/4.19 % (3684409)Termination reason: Instruction limit
% 27.57/4.19 % (3684409)Termination phase: Saturation
% 27.57/4.19 % (3684409)Time elapsed: 0.108 s
% 27.57/4.19 % (3684409)Peak memory usage: 13 MB
% 27.57/4.19 % (3684409)Instructions burned: 103 (million)
% 27.57/4.19 % (3684422)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1132294662:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.57/4.19 % TRYING [3]
% 27.57/4.19 % (3684423)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1323568870:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.57/4.19 % (3684412)Instruction limit reached!
% 27.57/4.19 % (3684412)------------------------------
% 27.57/4.19 % (3684412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.57/4.19 % (3684412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.57/4.19 % (3684412)CaDiCaL version: 2.1.3
% 27.57/4.19 % (3684412)Termination reason: Instruction limit
% 27.57/4.19 % (3684412)Termination phase: Saturation
% 27.57/4.19 % (3684412)Time elapsed: 0.164 s
% 27.57/4.19 % (3684412)Peak memory usage: 15 MB
% 27.57/4.19 % (3684412)Instructions burned: 159 (million)
% 27.57/4.19 % TRYING [1]
% 27.57/4.19 % TRYING [2]
% 27.57/4.19 % (3684426)ott-21_1_sil=16000:fs=off:random_seed=3494016020:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 27.57/4.19 % TRYING [3]
% 27.57/4.19 % (3684422)Instruction limit reached!
% 27.57/4.19 % (3684422)------------------------------
% 27.57/4.19 % (3684422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.57/4.19 % (3684422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684422)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684422)Termination reason: Instruction limit
% 36.60/11.11 % (3684422)Termination phase: Saturation
% 36.60/11.11 % (3684422)Time elapsed: 0.128 s
% 36.60/11.11 % (3684422)Peak memory usage: 14 MB
% 36.60/11.11 % (3684422)Instructions burned: 131 (million)
% 36.60/11.11 % (3684428)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=325368827:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 36.60/11.11 % (3684426)Instruction limit reached!
% 36.60/11.11 % (3684426)------------------------------
% 36.60/11.11 % (3684426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684426)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684426)Termination reason: Instruction limit
% 36.60/11.11 % (3684426)Termination phase: Saturation
% 36.60/11.11 % (3684426)Time elapsed: 0.165 s
% 36.60/11.11 % (3684426)Peak memory usage: 14 MB
% 36.60/11.11 % (3684426)Instructions burned: 181 (million)
% 36.60/11.11 % (3684430)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4140623420:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 36.60/11.11 % TRYING [4]
% 36.60/11.11 % TRYING [1]
% 36.60/11.11 % TRYING [2]
% 36.60/11.11 % TRYING [3]
% 36.60/11.11 % (3684420)Instruction limit reached!
% 36.60/11.11 % (3684420)------------------------------
% 36.60/11.11 % (3684420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684420)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684420)Termination reason: Instruction limit
% 36.60/11.11 % (3684420)Termination phase: Finite model building constraint generation
% 36.60/11.11 % (3684420)Time elapsed: 0.509 s
% 36.60/11.11 % (3684420)Peak memory usage: 38 MB
% 36.60/11.11 % (3684420)Instructions burned: 714 (million)
% 36.60/11.11 % (3684432)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3075625605:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 36.60/11.11 % (3684428)Instruction limit reached!
% 36.60/11.11 % (3684428)------------------------------
% 36.60/11.11 % (3684428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684428)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684428)Termination reason: Instruction limit
% 36.60/11.11 % (3684428)Termination phase: Saturation
% 36.60/11.11 % (3684428)Time elapsed: 0.527 s
% 36.60/11.11 % (3684428)Peak memory usage: 16 MB
% 36.60/11.11 % (3684428)Instructions burned: 477 (million)
% 36.60/11.11 % (3684434)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1391526781:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 36.60/11.11 % (3684423)Instruction limit reached!
% 36.60/11.11 % (3684423)------------------------------
% 36.60/11.11 % (3684423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684423)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684423)Termination reason: Instruction limit
% 36.60/11.11 % (3684423)Termination phase: Saturation
% 36.60/11.11 % (3684423)Time elapsed: 0.721 s
% 36.60/11.11 % (3684423)Peak memory usage: 20 MB
% 36.60/11.11 % (3684423)Instructions burned: 684 (million)
% 36.60/11.11 % (3684436)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3414418723:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 36.60/11.11 % (3684430)Instruction limit reached!
% 36.60/11.11 % (3684430)------------------------------
% 36.60/11.11 % (3684430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684430)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684430)Termination reason: Instruction limit
% 36.60/11.11 % (3684430)Termination phase: Finite model building SAT solving
% 36.60/11.11 % (3684430)Time elapsed: 0.675 s
% 36.60/11.11 % (3684430)Peak memory usage: 32 MB
% 36.60/11.11 % (3684430)Instructions burned: 865 (million)
% 36.60/11.11 % (3684438)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3316372173:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 36.60/11.11 % (3684434)Instruction limit reached!
% 36.60/11.11 % (3684434)------------------------------
% 36.60/11.11 % (3684434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684434)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684434)Termination reason: Instruction limit
% 36.60/11.11 % (3684434)Termination phase: Finite model building constraint generation
% 36.60/11.11 % (3684434)Time elapsed: 0.689 s
% 36.60/11.11 % (3684434)Peak memory usage: 103 MB
% 36.60/11.11 % (3684434)Instructions burned: 889 (million)
% 36.60/11.11 % TRYING [5]
% 36.60/11.11 % (3684441)fmb+10_1_sil=64000:random_seed=3779873843:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 36.60/11.11 % (3684436)Instruction limit reached!
% 36.60/11.11 % (3684436)------------------------------
% 36.60/11.11 % (3684436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684436)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684436)Termination reason: Instruction limit
% 36.60/11.11 % (3684436)Termination phase: Saturation
% 36.60/11.11 % (3684436)Time elapsed: 0.697 s
% 36.60/11.11 % (3684436)Peak memory usage: 21 MB
% 36.60/11.11 % (3684436)Instructions burned: 693 (million)
% 36.60/11.11 % (3684443)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2233207041:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 36.60/11.11 % TRYING [1]
% 36.60/11.11 % TRYING [2]
% 36.60/11.11 % TRYING [20]
% 36.60/11.11 % (3684438)Instruction limit reached!
% 36.60/11.11 % (3684438)------------------------------
% 36.60/11.11 % (3684438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684438)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684438)Termination reason: Instruction limit
% 36.60/11.11 % (3684438)Termination phase: Saturation
% 36.60/11.11 % (3684438)Time elapsed: 0.654 s
% 36.60/11.11 % (3684438)Peak memory usage: 20 MB
% 36.60/11.11 % (3684438)Instructions burned: 880 (million)
% 36.60/11.11 % (3684445)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3123303195:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 36.60/11.11 % TRYING [3]
% 36.60/11.11 % TRYING [8]
% 36.60/11.11 % (3684432)Instruction limit reached!
% 36.60/11.11 % (3684432)------------------------------
% 36.60/11.11 % (3684432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684432)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684432)Termination reason: Instruction limit
% 36.60/11.11 % (3684432)Termination phase: Saturation
% 36.60/11.11 % (3684432)Time elapsed: 1.246 s
% 36.60/11.11 % (3684432)Peak memory usage: 29 MB
% 36.60/11.11 % (3684432)Instructions burned: 1180 (million)
% 36.60/11.11 % (3684447)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2788532274:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 36.60/11.11 % (3684445)Instruction limit reached!
% 36.60/11.11 % (3684445)------------------------------
% 36.60/11.11 % (3684445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684445)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684445)Termination reason: Instruction limit
% 36.60/11.11 % (3684445)Termination phase: Finite model building constraint generation
% 36.60/11.11 % (3684445)Time elapsed: 0.667 s
% 36.60/11.11 % (3684445)Peak memory usage: 65 MB
% 36.60/11.11 % (3684445)Instructions burned: 920 (million)
% 36.60/11.11 % (3684449)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4071009465:i=1472:ins=7:fdi=8:gsp=on_2974 on theBenchmark for (2974ds/1472Mi)
% 36.60/11.11 % (3684449)Instruction limit reached!
% 36.60/11.11 % (3684449)------------------------------
% 36.60/11.11 % (3684449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684449)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684449)Termination reason: Instruction limit
% 36.60/11.11 % (3684449)Termination phase: Saturation
% 36.60/11.11 % (3684449)Time elapsed: 1.255 s
% 36.60/11.11 % (3684449)Peak memory usage: 22 MB
% 36.60/11.11 % (3684449)Instructions burned: 1473 (million)
% 36.60/11.11 % (3684451)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2807085645:i=6324_2961 on theBenchmark for (2961ds/6324Mi)
% 36.60/11.11 % (3684451)Cannot represent all propositional literals internally
% 36.60/11.11 % (3684451)Refutation not found, incomplete strategy
% 36.60/11.11 % (3684451)------------------------------
% 36.60/11.11 % (3684451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684451)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684451)Termination reason: Refutation not found, incomplete strategy
% 36.60/11.11 % (3684451)Time elapsed: 0.064 s
% 36.60/11.11 % (3684451)Peak memory usage: 13 MB
% 36.60/11.11 % (3684451)Instructions burned: 96 (million)
% 36.60/11.11 % (3684451)------------------------------
% 36.60/11.11 % (3684451)------------------------------
% 36.60/11.11 % (3684453)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2682897559:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 36.60/11.11 % TRYING [16]
% 36.60/11.11 % TRYING [4]
% 36.60/11.11 % (3684453)Instruction limit reached!
% 36.60/11.11 % (3684453)------------------------------
% 36.60/11.11 % (3684453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684453)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684453)Termination reason: Instruction limit
% 36.60/11.11 % (3684453)Termination phase: Finite model building constraint generation
% 36.60/11.11 % (3684453)Time elapsed: 1.294 s
% 36.60/11.11 % (3684453)Peak memory usage: 121 MB
% 36.60/11.11 % (3684453)Instructions burned: 2174 (million)
% 36.60/11.11 % (3684455)ott-2_1_sil=16000:newcnf=on:random_seed=3984697936:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2947 on theBenchmark for (2947ds/869Mi)
% 36.60/11.11 % TRYING [6]
% 36.60/11.11 % (3684455)Instruction limit reached!
% 36.60/11.11 % (3684455)------------------------------
% 36.60/11.11 % (3684455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684455)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684455)Termination reason: Instruction limit
% 36.60/11.11 % (3684455)Termination phase: Saturation
% 36.60/11.11 % (3684455)Time elapsed: 0.869 s
% 36.60/11.11 % (3684455)Peak memory usage: 18 MB
% 36.60/11.11 % (3684455)Instructions burned: 869 (million)
% 36.60/11.11 % (3684457)ott+10_1_sil=32000:tgt=ground:random_seed=3821462776:i=5114:av=off_2938 on theBenchmark for (2938ds/5114Mi)
% 36.60/11.11 % (3684447)Instruction limit reached!
% 36.60/11.11 % (3684447)------------------------------
% 36.60/11.11 % (3684447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684447)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684447)Termination reason: Instruction limit
% 36.60/11.11 % (3684447)Termination phase: Saturation
% 36.60/11.11 % (3684447)Time elapsed: 4.761 s
% 36.60/11.11 % (3684447)Peak memory usage: 40 MB
% 36.60/11.11 % (3684447)Instructions burned: 5132 (million)
% 36.60/11.11 % (3684459)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1045025830:i=54282_2932 on theBenchmark for (2932ds/54282Mi)
% 36.60/11.11 % TRYING [1]
% 36.60/11.11 % TRYING [2]
% 36.60/11.11 % TRYING [3]
% 36.60/11.11 % TRYING [4]
% 36.60/11.11 % TRYING [5]
% 36.60/11.11 % (3684443)Instruction limit reached!
% 36.60/11.11 % (3684443)------------------------------
% 36.60/11.11 % (3684443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.11 % (3684443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.11 % (3684443)CaDiCaL version: 2.1.3
% 36.60/11.11 % (3684443)Termination reason: Instruction limit
% 36.60/11.11 % (3684443)Termination phase: Finite model building constraint generation
% 36.60/11.11 % (3684443)Time elapsed: 6.889 s
% 36.60/11.11 % (3684443)Peak memory usage: 596 MB
% 36.60/11.11 % (3684443)Instructions burned: 9515 (million)
% 36.60/11.11 % (3684461)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=971355440:i=3512:aac=none_2913 on theBenchmark for (2913ds/3512Mi)
% 36.60/11.11 % (3684407) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3684401-3684407"...
% 36.60/11.11 % (3684407)...printing done.
% 36.60/11.11 % (3684407)Refutation found. Thanks to Tanya!
% 36.60/11.11 % SZS status Theorem for theBenchmark
% 36.60/11.11 % SZS output start Proof for theBenchmark
% See solution above
% 36.60/11.12 % (3684407)------------------------------
% 36.60/11.12 % (3684407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.60/11.12 % (3684407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.60/11.12 % (3684407)CaDiCaL version: 2.1.3
% 36.60/11.12 % (3684407)Termination reason: Refutation
% 36.60/11.12 % (3684407)Time elapsed: 10.662 s
% 36.60/11.12 % (3684407)Peak memory usage: 124 MB
% 36.60/11.12 % (3684407)Instructions burned: 21305 (million)
% 36.60/11.12 % (3684401)Success in time 10.831 s
% 36.60/11.12 % Vampire exiting
%------------------------------------------------------------------------------