%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX023+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:41 PM UTC 2026
% Result : Theorem 5.77s 1.53s
% Output : Refutation 6.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 27
% Syntax : Number of formulae : 167 ( 29 unt; 16 def)
% Number of atoms : 463 ( 129 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 492 ( 196 ~; 236 |; 25 &)
% ( 16 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 17 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 108 ( 0 sgn 92 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] : nil != cons(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id5) ).
fof(f82,axiom,
! [X0] : '@+'('0',X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(plus:zero:1)') ).
fof(f83,axiom,
! [X0,X1] :
( nat_succeeds(X0)
=> '@+'(s(X0),X1) = s('@+'(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','axiom-(plus:successor:1)') ).
fof(f181,axiom,
! [X0] : '**'(nil,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(app:nil)') ).
fof(f182,axiom,
! [X0,X1,X2] :
( list_succeeds(X1)
=> '**'(cons(X0,X1),X2) = cons(X0,'**'(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(app:cons)') ).
fof(f183,axiom,
! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1) )
=> list_succeeds('**'(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(app:types:1)') ).
fof(f194,axiom,
lh(nil) = '0',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(lh:nil)') ).
fof(f195,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> lh(cons(X0,X1)) = s(lh(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(lh:cons)') ).
fof(f196,axiom,
! [X0] :
( list_succeeds(X0)
=> nat_succeeds(lh(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(lh:types)') ).
fof(f199,axiom,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3] :
( list_succeeds(X3)
=> lh('**'(X2,X3)) = '@+'(lh(X2),lh(X3)) ) )
| X0 = nil )
=> ! [X3] :
( list_succeeds(X3)
=> lh('**'(X0,X3)) = '@+'(lh(X0),lh(X3)) ) )
=> ! [X0] :
( list_succeeds(X0)
=> ! [X3] :
( list_succeeds(X3)
=> lh('**'(X0,X3)) = '@+'(lh(X0),lh(X3)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f200,conjecture,
! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1) )
=> lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','theorem-(app:lh)') ).
fof(f201,negated_conjecture,
~ ! [X0,X1] :
( ( list_succeeds(X0)
& list_succeeds(X1) )
=> lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1)) ),
inference(negated_conjecture,[status(cth)],[f200]) ).
fof(f222,plain,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3] :
( list_succeeds(X3)
=> lh('**'(X2,X3)) = '@+'(lh(X2),lh(X3)) ) )
| X0 = nil )
=> ! [X4] :
( list_succeeds(X4)
=> lh('**'(X0,X4)) = '@+'(lh(X0),lh(X4)) ) )
=> ! [X5] :
( list_succeeds(X5)
=> ! [X6] :
( list_succeeds(X6)
=> lh('**'(X5,X6)) = '@+'(lh(X5),lh(X6)) ) ) ),
inference(rectify,[],[f199]) ).
fof(f277,plain,
! [X0,X1] :
( '@+'(s(X0),X1) = s('@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(ennf_transformation,[],[f83]) ).
fof(f428,plain,
! [X0,X1,X2] :
( '**'(cons(X0,X1),X2) = cons(X0,'**'(X1,X2))
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f182]) ).
fof(f429,plain,
! [X0,X1] :
( list_succeeds('**'(X0,X1))
| ~ list_succeeds(X0)
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f183]) ).
fof(f430,plain,
! [X0,X1] :
( list_succeeds('**'(X0,X1))
| ~ list_succeeds(X0)
| ~ list_succeeds(X1) ),
inference(flattening,[],[f429]) ).
fof(f446,plain,
! [X0,X1] :
( lh(cons(X0,X1)) = s(lh(X1))
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f195]) ).
fof(f447,plain,
! [X0] :
( nat_succeeds(lh(X0))
| ~ list_succeeds(X0) ),
inference(ennf_transformation,[],[f196]) ).
fof(f452,plain,
( ! [X5] :
( ! [X6] :
( lh('**'(X5,X6)) = '@+'(lh(X5),lh(X6))
| ~ list_succeeds(X6) )
| ~ list_succeeds(X5) )
| ? [X0] :
( ? [X4] :
( lh('**'(X0,X4)) != '@+'(lh(X0),lh(X4))
& list_succeeds(X4) )
& ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3] :
( lh('**'(X2,X3)) = '@+'(lh(X2),lh(X3))
| ~ list_succeeds(X3) ) )
| X0 = nil ) ) ),
inference(ennf_transformation,[],[f222]) ).
fof(f453,plain,
? [X0,X1] :
( lh('**'(X0,X1)) != '@+'(lh(X0),lh(X1))
& list_succeeds(X0)
& list_succeeds(X1) ),
inference(ennf_transformation,[],[f201]) ).
fof(f454,plain,
? [X0,X1] :
( lh('**'(X0,X1)) != '@+'(lh(X0),lh(X1))
& list_succeeds(X0)
& list_succeeds(X1) ),
inference(flattening,[],[f453]) ).
fof(f592,plain,
( ! [X0] :
( ! [X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1) )
| ~ list_succeeds(X0) )
| ? [X2] :
( ? [X3] :
( lh('**'(X2,X3)) != '@+'(lh(X2),lh(X3))
& list_succeeds(X3) )
& ( ? [X4,X5] :
( cons(X4,X5) = X2
& list_succeeds(X5)
& ! [X6] :
( lh('**'(X5,X6)) = '@+'(lh(X5),lh(X6))
| ~ list_succeeds(X6) ) )
| nil = X2 ) ) ),
inference(rectify,[],[f452]) ).
fof(f593,plain,
( ! [X0] :
( ! [X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1) )
| ~ list_succeeds(X0) )
| ( lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
& list_succeeds(sK88)
& ( ( sK87 = cons(sK89,sK90)
& list_succeeds(sK90)
& ! [X6] :
( lh('**'(sK90,X6)) = '@+'(lh(sK90),lh(X6))
| ~ list_succeeds(X6) ) )
| nil = sK87 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88,sK89,sK90]),skolemize(X2,sK87),skolemize(X3,sK88),skolemize(X4,sK89),skolemize(X5,sK90)],[f592]) ).
fof(f594,plain,
( lh('**'(sK91,sK92)) != '@+'(lh(sK91),lh(sK92))
& list_succeeds(sK91)
& list_succeeds(sK92) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91,sK92]),skolemize(X0,sK91),skolemize(X1,sK92)],[f454]) ).
fof(f599,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[],[f5]) ).
fof(f823,plain,
! [X0] : '@+'('0',X0) = X0,
inference(cnf_transformation,[],[f82]) ).
fof(f824,plain,
! [X0,X1] :
( '@+'(s(X0),X1) = s('@+'(X0,X1))
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[],[f277]) ).
fof(f925,plain,
! [X0] : '**'(nil,X0) = X0,
inference(cnf_transformation,[],[f181]) ).
fof(f926,plain,
! [X2,X0,X1] :
( '**'(cons(X0,X1),X2) = cons(X0,'**'(X1,X2))
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f428]) ).
fof(f927,plain,
! [X0,X1] :
( list_succeeds('**'(X0,X1))
| ~ list_succeeds(X0)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f430]) ).
fof(f940,plain,
'0' = lh(nil),
inference(cnf_transformation,[],[f194]) ).
fof(f941,plain,
! [X0,X1] :
( lh(cons(X0,X1)) = s(lh(X1))
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f446]) ).
fof(f942,plain,
! [X0] :
( nat_succeeds(lh(X0))
| ~ list_succeeds(X0) ),
inference(cnf_transformation,[],[f447]) ).
fof(f945,plain,
! [X0,X1,X6] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| lh('**'(sK90,X6)) = '@+'(lh(sK90),lh(X6))
| ~ list_succeeds(X6)
| nil = sK87 ),
inference(cnf_transformation,[],[f593]) ).
fof(f946,plain,
! [X0,X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| list_succeeds(sK90)
| nil = sK87 ),
inference(cnf_transformation,[],[f593]) ).
fof(f947,plain,
! [X0,X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| sK87 = cons(sK89,sK90)
| nil = sK87 ),
inference(cnf_transformation,[],[f593]) ).
fof(f948,plain,
! [X0,X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| list_succeeds(sK88) ),
inference(cnf_transformation,[],[f593]) ).
fof(f949,plain,
! [X0,X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88)) ),
inference(cnf_transformation,[],[f593]) ).
fof(f950,plain,
list_succeeds(sK92),
inference(cnf_transformation,[],[f594]) ).
fof(f951,plain,
list_succeeds(sK91),
inference(cnf_transformation,[],[f594]) ).
fof(f952,plain,
lh('**'(sK91,sK92)) != '@+'(lh(sK91),lh(sK92)),
inference(cnf_transformation,[],[f594]) ).
fof(f1042,plain,
! [X6] :
( lh('**'(sK90,X6)) = '@+'(lh(sK90),lh(X6))
| ~ list_succeeds(X6)
| sP94 ),
inference(cnf_transformation,[],[f1042_D]) ).
fof(f1042_D,definition,
( ! [X6] :
( lh('**'(sK90,X6)) = '@+'(lh(sK90),lh(X6))
| ~ list_succeeds(X6) )
<=> ~ sP94 ),
introduced(definition,[new_symbols(definition,[sP94])],[general_splitting_component_introduction]) ).
fof(f1043,plain,
! [X0,X1] :
( lh('**'(X0,X1)) = '@+'(lh(X0),lh(X1))
| ~ list_succeeds(X1)
| ~ list_succeeds(X0)
| nil = sK87
| ~ sP94 ),
inference(general_splitting,[],[f945,f1042_D]) ).
fof(f1045,definition,
( spl95_1
<=> lh('**'(sK91,sK92)) = '@+'(lh(sK91),lh(sK92)) ),
introduced(definition,[new_symbols(definition,[spl95_1])],[avatar_definition]) ).
fof(f1047,plain,
( lh('**'(sK91,sK92)) != '@+'(lh(sK91),lh(sK92))
| spl95_1 ),
inference(avatar_component_clause,[],[f1045]) ).
fof(f1048,plain,
~ spl95_1,
inference(avatar_split_clause,[],[f952,f1045]) ).
fof(f1051,plain,
( lh('**'(sK91,sK92)) != lh('**'(sK91,sK92))
| ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| list_succeeds(sK90)
| nil = sK87
| spl95_1 ),
inference(superposition,[],[f1047,f946]) ).
fof(f1052,plain,
( lh('**'(sK91,sK92)) != lh('**'(sK91,sK92))
| ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| sK87 = cons(sK89,sK90)
| nil = sK87
| spl95_1 ),
inference(superposition,[],[f1047,f947]) ).
fof(f1053,plain,
( lh('**'(sK91,sK92)) != lh('**'(sK91,sK92))
| ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| list_succeeds(sK88)
| spl95_1 ),
inference(superposition,[],[f1047,f948]) ).
fof(f1054,plain,
( lh('**'(sK91,sK92)) != lh('**'(sK91,sK92))
| ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
| spl95_1 ),
inference(superposition,[],[f1047,f949]) ).
fof(f1055,plain,
( lh('**'(sK91,sK92)) != lh('**'(sK91,sK92))
| ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| nil = sK87
| ~ sP94
| spl95_1 ),
inference(superposition,[],[f1047,f1043]) ).
fof(f1056,plain,
( ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| nil = sK87
| ~ sP94
| spl95_1 ),
inference(trivial_inequality_removal,[],[f1055]) ).
fof(f1057,plain,
( ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
| spl95_1 ),
inference(trivial_inequality_removal,[],[f1054]) ).
fof(f1058,plain,
( ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| list_succeeds(sK88)
| spl95_1 ),
inference(trivial_inequality_removal,[],[f1053]) ).
fof(f1059,plain,
( ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| sK87 = cons(sK89,sK90)
| nil = sK87
| spl95_1 ),
inference(trivial_inequality_removal,[],[f1052]) ).
fof(f1060,plain,
( ~ list_succeeds(sK92)
| ~ list_succeeds(sK91)
| list_succeeds(sK90)
| nil = sK87
| spl95_1 ),
inference(trivial_inequality_removal,[],[f1051]) ).
fof(f1061,plain,
( ~ list_succeeds(sK91)
| nil = sK87
| ~ sP94
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1056,f950]) ).
fof(f1062,plain,
( ~ list_succeeds(sK91)
| lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1057,f950]) ).
fof(f1063,plain,
( ~ list_succeeds(sK91)
| list_succeeds(sK88)
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1058,f950]) ).
fof(f1064,plain,
( ~ list_succeeds(sK91)
| sK87 = cons(sK89,sK90)
| nil = sK87
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1059,f950]) ).
fof(f1065,plain,
( ~ list_succeeds(sK91)
| list_succeeds(sK90)
| nil = sK87
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1060,f950]) ).
fof(f1068,plain,
( nil = sK87
| ~ sP94
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1061,f951]) ).
fof(f1069,plain,
( lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1062,f951]) ).
fof(f1070,plain,
( list_succeeds(sK88)
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1063,f951]) ).
fof(f1071,plain,
( sK87 = cons(sK89,sK90)
| nil = sK87
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1064,f951]) ).
fof(f1072,plain,
( list_succeeds(sK90)
| nil = sK87
| spl95_1 ),
inference(forward_subsumption_resolution,[],[f1065,f951]) ).
fof(f1074,definition,
( spl95_2
<=> lh('**'(sK87,sK88)) = '@+'(lh(sK87),lh(sK88)) ),
introduced(definition,[new_symbols(definition,[spl95_2])],[avatar_definition]) ).
fof(f1076,plain,
( lh('**'(sK87,sK88)) != '@+'(lh(sK87),lh(sK88))
| spl95_2 ),
inference(avatar_component_clause,[],[f1074]) ).
fof(f1077,plain,
( ~ spl95_2
| spl95_1 ),
inference(avatar_split_clause,[],[f1069,f1045,f1074]) ).
fof(f1107,definition,
( spl95_3
<=> list_succeeds(sK88) ),
introduced(definition,[new_symbols(definition,[spl95_3])],[avatar_definition]) ).
fof(f1109,plain,
( list_succeeds(sK88)
| ~ spl95_3 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1110,plain,
( spl95_3
| spl95_1 ),
inference(avatar_split_clause,[],[f1070,f1045,f1107]) ).
fof(f1153,plain,
( lh('**'(sK90,sK88)) = '@+'(lh(sK90),lh(sK88))
| sP94
| ~ spl95_3 ),
inference(resolution,[],[f1109,f1042]) ).
fof(f1257,definition,
( spl95_6
<=> nil = sK87 ),
introduced(definition,[new_symbols(definition,[spl95_6])],[avatar_definition]) ).
fof(f1259,plain,
( nil = sK87
| ~ spl95_6 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1261,definition,
( spl95_7
<=> list_succeeds(sK90) ),
introduced(definition,[new_symbols(definition,[spl95_7])],[avatar_definition]) ).
fof(f1263,plain,
( list_succeeds(sK90)
| ~ spl95_7 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1264,plain,
( spl95_6
| spl95_7
| spl95_1 ),
inference(avatar_split_clause,[],[f1072,f1045,f1261,f1257]) ).
fof(f1292,plain,
( ! [X0] : lh(cons(X0,sK90)) = s(lh(sK90))
| ~ spl95_7 ),
inference(resolution,[],[f1263,f941]) ).
fof(f1311,definition,
( spl95_8
<=> ! [X0] : lh(cons(X0,sK90)) = s(lh(sK90)) ),
introduced(definition,[new_symbols(definition,[spl95_8])],[avatar_definition]) ).
fof(f1312,plain,
( ! [X0] : lh(cons(X0,sK90)) = s(lh(sK90))
| ~ spl95_8 ),
inference(avatar_component_clause,[],[f1311]) ).
fof(f1313,plain,
( spl95_8
| ~ spl95_7 ),
inference(avatar_split_clause,[],[f1292,f1261,f1311]) ).
fof(f1345,definition,
( spl95_9
<=> sK87 = cons(sK89,sK90) ),
introduced(definition,[new_symbols(definition,[spl95_9])],[avatar_definition]) ).
fof(f1347,plain,
( sK87 = cons(sK89,sK90)
| ~ spl95_9 ),
inference(avatar_component_clause,[],[f1345]) ).
fof(f1348,plain,
( spl95_6
| spl95_9
| spl95_1 ),
inference(avatar_split_clause,[],[f1071,f1045,f1345,f1257]) ).
fof(f1355,plain,
( lh(sK87) = s(lh(sK90))
| ~ spl95_8
| ~ spl95_9 ),
inference(superposition,[],[f1312,f1347]) ).
fof(f1357,plain,
( nil != sK87
| ~ spl95_9 ),
inference(superposition,[],[f599,f1347]) ).
fof(f1410,plain,
( ~ sP94
| spl95_1
| ~ spl95_9 ),
inference(backward_subsumption_resolution,[],[f1068,f1357]) ).
fof(f1418,plain,
( lh('**'(sK90,sK88)) = '@+'(lh(sK90),lh(sK88))
| spl95_1
| ~ spl95_3
| ~ spl95_9 ),
inference(backward_subsumption_resolution,[],[f1153,f1410]) ).
fof(f1458,plain,
( lh('**'(nil,sK88)) != '@+'(lh(nil),lh(sK88))
| spl95_2
| ~ spl95_6 ),
inference(superposition,[],[f1076,f1259]) ).
fof(f1460,plain,
( lh('**'(nil,sK88)) != '@+'('0',lh(sK88))
| spl95_2
| ~ spl95_6 ),
inference(forward_demodulation,[],[f1458,f940]) ).
fof(f1461,plain,
( lh(sK88) != lh('**'(nil,sK88))
| spl95_2
| ~ spl95_6 ),
inference(forward_demodulation,[],[f1460,f823]) ).
fof(f1462,plain,
( lh(sK88) != lh(sK88)
| spl95_2
| ~ spl95_6 ),
inference(forward_demodulation,[],[f1461,f925]) ).
fof(f1463,plain,
( $false
| spl95_2
| ~ spl95_6 ),
inference(trivial_inequality_removal,[],[f1462]) ).
fof(f1464,plain,
( spl95_2
| ~ spl95_6 ),
inference(avatar_contradiction_clause,[],[f1463]) ).
fof(f1520,definition,
( spl95_11
<=> lh('**'(sK90,sK88)) = '@+'(lh(sK90),lh(sK88)) ),
introduced(definition,[new_symbols(definition,[spl95_11])],[avatar_definition]) ).
fof(f1522,plain,
( lh('**'(sK90,sK88)) = '@+'(lh(sK90),lh(sK88))
| ~ spl95_11 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1523,plain,
( spl95_11
| spl95_1
| ~ spl95_3
| ~ spl95_9 ),
inference(avatar_split_clause,[],[f1418,f1345,f1107,f1045,f1520]) ).
fof(f1700,plain,
( ! [X0] :
( cons(sK89,'**'(sK90,X0)) = '**'(sK87,X0)
| ~ list_succeeds(sK90) )
| ~ spl95_9 ),
inference(superposition,[],[f926,f1347]) ).
fof(f1731,plain,
( ! [X0] : cons(sK89,'**'(sK90,X0)) = '**'(sK87,X0)
| ~ spl95_7
| ~ spl95_9 ),
inference(forward_subsumption_resolution,[],[f1700,f1263]) ).
fof(f1825,definition,
( spl95_16
<=> ! [X0] : cons(sK89,'**'(sK90,X0)) = '**'(sK87,X0) ),
introduced(definition,[new_symbols(definition,[spl95_16])],[avatar_definition]) ).
fof(f1826,plain,
( ! [X0] : cons(sK89,'**'(sK90,X0)) = '**'(sK87,X0)
| ~ spl95_16 ),
inference(avatar_component_clause,[],[f1825]) ).
fof(f1827,plain,
( spl95_16
| ~ spl95_7
| ~ spl95_9 ),
inference(avatar_split_clause,[],[f1731,f1345,f1261,f1825]) ).
fof(f1856,plain,
( nat_succeeds(lh(sK90))
| ~ spl95_7 ),
inference(resolution,[],[f1263,f942]) ).
fof(f2048,plain,
( ! [X0] :
( s(lh('**'(sK90,X0))) = lh('**'(sK87,X0))
| ~ list_succeeds('**'(sK90,X0)) )
| ~ spl95_16 ),
inference(superposition,[],[f941,f1826]) ).
fof(f2132,definition,
( spl95_19
<=> ! [X0] :
( s(lh('**'(sK90,X0))) = lh('**'(sK87,X0))
| ~ list_succeeds('**'(sK90,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl95_19])],[avatar_definition]) ).
fof(f2133,plain,
( ! [X0] :
( s(lh('**'(sK90,X0))) = lh('**'(sK87,X0))
| ~ list_succeeds('**'(sK90,X0)) )
| ~ spl95_19 ),
inference(avatar_component_clause,[],[f2132]) ).
fof(f2134,plain,
( spl95_19
| ~ spl95_16 ),
inference(avatar_split_clause,[],[f2048,f1825,f2132]) ).
fof(f2203,definition,
( spl95_20
<=> lh(sK87) = s(lh(sK90)) ),
introduced(definition,[new_symbols(definition,[spl95_20])],[avatar_definition]) ).
fof(f2205,plain,
( lh(sK87) = s(lh(sK90))
| ~ spl95_20 ),
inference(avatar_component_clause,[],[f2203]) ).
fof(f2206,plain,
( spl95_20
| ~ spl95_8
| ~ spl95_9 ),
inference(avatar_split_clause,[],[f1355,f1345,f1311,f2203]) ).
fof(f2214,plain,
( ! [X0] :
( '@+'(lh(sK87),X0) = s('@+'(lh(sK90),X0))
| ~ nat_succeeds(lh(sK90)) )
| ~ spl95_20 ),
inference(superposition,[],[f824,f2205]) ).
fof(f2261,plain,
( ! [X0] : '@+'(lh(sK87),X0) = s('@+'(lh(sK90),X0))
| ~ spl95_7
| ~ spl95_20 ),
inference(forward_subsumption_resolution,[],[f2214,f1856]) ).
fof(f3636,definition,
( spl95_46
<=> ! [X0] : '@+'(lh(sK87),X0) = s('@+'(lh(sK90),X0)) ),
introduced(definition,[new_symbols(definition,[spl95_46])],[avatar_definition]) ).
fof(f3637,plain,
( ! [X0] : '@+'(lh(sK87),X0) = s('@+'(lh(sK90),X0))
| ~ spl95_46 ),
inference(avatar_component_clause,[],[f3636]) ).
fof(f3638,plain,
( spl95_46
| ~ spl95_7
| ~ spl95_20 ),
inference(avatar_split_clause,[],[f2261,f2203,f1261,f3636]) ).
fof(f3642,plain,
( '@+'(lh(sK87),lh(sK88)) = s(lh('**'(sK90,sK88)))
| ~ spl95_11
| ~ spl95_46 ),
inference(superposition,[],[f3637,f1522]) ).
fof(f3718,definition,
( spl95_47
<=> '@+'(lh(sK87),lh(sK88)) = s(lh('**'(sK90,sK88))) ),
introduced(definition,[new_symbols(definition,[spl95_47])],[avatar_definition]) ).
fof(f3720,plain,
( '@+'(lh(sK87),lh(sK88)) = s(lh('**'(sK90,sK88)))
| ~ spl95_47 ),
inference(avatar_component_clause,[],[f3718]) ).
fof(f3721,plain,
( spl95_47
| ~ spl95_11
| ~ spl95_46 ),
inference(avatar_split_clause,[],[f3642,f3636,f1520,f3718]) ).
fof(f3726,plain,
( lh('**'(sK87,sK88)) != s(lh('**'(sK90,sK88)))
| spl95_2
| ~ spl95_47 ),
inference(superposition,[],[f1076,f3720]) ).
fof(f3805,definition,
( spl95_48
<=> lh('**'(sK87,sK88)) = s(lh('**'(sK90,sK88))) ),
introduced(definition,[new_symbols(definition,[spl95_48])],[avatar_definition]) ).
fof(f3807,plain,
( lh('**'(sK87,sK88)) != s(lh('**'(sK90,sK88)))
| spl95_48 ),
inference(avatar_component_clause,[],[f3805]) ).
fof(f3808,plain,
( ~ spl95_48
| spl95_2
| ~ spl95_47 ),
inference(avatar_split_clause,[],[f3726,f3718,f1074,f3805]) ).
fof(f3811,plain,
( lh('**'(sK87,sK88)) != lh('**'(sK87,sK88))
| ~ list_succeeds('**'(sK90,sK88))
| ~ spl95_19
| spl95_48 ),
inference(superposition,[],[f3807,f2133]) ).
fof(f3812,plain,
( ~ list_succeeds('**'(sK90,sK88))
| ~ spl95_19
| spl95_48 ),
inference(trivial_inequality_removal,[],[f3811]) ).
fof(f3815,definition,
( spl95_49
<=> list_succeeds('**'(sK90,sK88)) ),
introduced(definition,[new_symbols(definition,[spl95_49])],[avatar_definition]) ).
fof(f3817,plain,
( ~ list_succeeds('**'(sK90,sK88))
| spl95_49 ),
inference(avatar_component_clause,[],[f3815]) ).
fof(f3818,plain,
( ~ spl95_49
| ~ spl95_19
| spl95_48 ),
inference(avatar_split_clause,[],[f3812,f3805,f2132,f3815]) ).
fof(f3819,plain,
( ~ list_succeeds(sK90)
| ~ list_succeeds(sK88)
| spl95_49 ),
inference(resolution,[],[f3817,f927]) ).
fof(f3831,plain,
( ~ list_succeeds(sK88)
| ~ spl95_7
| spl95_49 ),
inference(forward_subsumption_resolution,[],[f3819,f1263]) ).
fof(f3833,plain,
( $false
| ~ spl95_3
| ~ spl95_7
| spl95_49 ),
inference(forward_subsumption_resolution,[],[f3831,f1109]) ).
fof(f3834,plain,
( ~ spl95_3
| ~ spl95_7
| spl95_49 ),
inference(avatar_contradiction_clause,[],[f3833]) ).
cnf(s1,plain,
~ spl95_1,
inference(sat_conversion,[],[f1048]) ).
cnf(s2,plain,
( spl95_1
| ~ spl95_2 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s3,plain,
( spl95_1
| spl95_3 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s6,plain,
( spl95_1
| spl95_6
| spl95_7 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s7,plain,
( ~ spl95_7
| spl95_8 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s8,plain,
( spl95_1
| spl95_6
| spl95_9 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s11,plain,
( spl95_2
| ~ spl95_6 ),
inference(sat_conversion,[],[f1464]) ).
cnf(s13,plain,
( spl95_1
| ~ spl95_3
| ~ spl95_9
| spl95_11 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s18,plain,
( ~ spl95_7
| ~ spl95_9
| spl95_16 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s21,plain,
( ~ spl95_16
| spl95_19 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s22,plain,
( ~ spl95_8
| ~ spl95_9
| spl95_20 ),
inference(sat_conversion,[],[f2206]) ).
cnf(s48,plain,
( ~ spl95_7
| ~ spl95_20
| spl95_46 ),
inference(sat_conversion,[],[f3638]) ).
cnf(s49,plain,
( ~ spl95_11
| ~ spl95_46
| spl95_47 ),
inference(sat_conversion,[],[f3721]) ).
cnf(s50,plain,
( spl95_2
| ~ spl95_47
| ~ spl95_48 ),
inference(sat_conversion,[],[f3808]) ).
cnf(s51,plain,
( ~ spl95_19
| spl95_48
| ~ spl95_49 ),
inference(sat_conversion,[],[f3818]) ).
cnf(s52,plain,
( ~ spl95_3
| ~ spl95_7
| spl95_49 ),
inference(sat_conversion,[],[f3834]) ).
cnf(s55,plain,
spl95_3,
inference(rat,[],[s3,s1]) ).
cnf(s56,plain,
~ spl95_2,
inference(rat,[],[s2,s1]) ).
cnf(s59,plain,
~ spl95_6,
inference(rat,[],[s11,s56]) ).
cnf(s60,plain,
spl95_9,
inference(rat,[],[s8,s1,s59]) ).
cnf(s61,plain,
spl95_7,
inference(rat,[],[s6,s1,s59]) ).
cnf(s66,plain,
spl95_11,
inference(rat,[],[s13,s55,s1,s60]) ).
cnf(s67,plain,
spl95_49,
inference(rat,[],[s52,s55,s61]) ).
cnf(s71,plain,
spl95_16,
inference(rat,[],[s18,s60,s61]) ).
cnf(s73,plain,
spl95_8,
inference(rat,[],[s7,s61]) ).
cnf(s81,plain,
spl95_19,
inference(rat,[],[s21,s71]) ).
cnf(s83,plain,
spl95_20,
inference(rat,[],[s22,s60,s73]) ).
cnf(s86,plain,
spl95_48,
inference(rat,[],[s51,s67,s81]) ).
cnf(s88,plain,
spl95_46,
inference(rat,[],[s48,s61,s83]) ).
cnf(s91,plain,
~ spl95_47,
inference(rat,[],[s50,s56,s86]) ).
cnf(s92,plain,
$false,
inference(rat,[],[s49,s66,s91,s88]) ).
fof(f3835,plain,
$false,
inference(avatar_sat_refutation,[],[s92]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX023+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n018.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 14:54:10 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.77/1.53 % (3458291)Detected formulas, will run a generic FOF schedule.
% 5.77/1.53 % (3458298)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=2665403506:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 5.77/1.53 % (3458296)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=2144683154:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 5.77/1.53 % (3458299)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2501599361:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 5.77/1.53 % (3458302)dis-21_1_sil=8000:lcm=predicate:random_seed=3958568428: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)
% 5.77/1.53 % (3458301)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=84833025:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 5.77/1.53 % (3458300)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3990546029:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 5.77/1.53 % (3458297)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=940992312:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 5.77/1.53 % (3458299)Refutation not found, incomplete strategy
% 5.77/1.53 % (3458299)------------------------------
% 5.77/1.53 % (3458299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458299)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458299)Termination reason: Refutation not found, incomplete strategy
% 5.77/1.53 % (3458299)Time elapsed: 0.004 s
% 5.77/1.53 % (3458299)Peak memory usage: 88 MB
% 5.77/1.53 % (3458299)Instructions burned: 4 (million)
% 5.77/1.53 % (3458300)Instruction limit reached!
% 5.77/1.53 % (3458300)------------------------------
% 5.77/1.53 % (3458300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458300)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458300)Termination reason: Instruction limit
% 5.77/1.53 % (3458300)Termination phase: Saturation
% 5.77/1.53 % (3458300)Time elapsed: 0.073 s
% 5.77/1.53 % (3458300)Peak memory usage: 88 MB
% 5.77/1.53 % (3458300)Instructions burned: 120 (million)
% 5.77/1.53 % (3458302)Instruction limit reached!
% 5.77/1.53 % (3458302)------------------------------
% 5.77/1.53 % (3458302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458302)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458302)Termination reason: Instruction limit
% 5.77/1.53 % (3458302)Termination phase: Saturation
% 5.77/1.53 % (3458302)Time elapsed: 0.082 s
% 5.77/1.53 % (3458302)Peak memory usage: 89 MB
% 5.77/1.53 % (3458302)Instructions burned: 130 (million)
% 5.77/1.53 % (3458301)Instruction limit reached!
% 5.77/1.53 % (3458301)------------------------------
% 5.77/1.53 % (3458301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458301)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458301)Termination reason: Instruction limit
% 5.77/1.53 % (3458301)Termination phase: Saturation
% 5.77/1.53 % (3458301)Time elapsed: 0.102 s
% 5.77/1.53 % (3458301)Peak memory usage: 90 MB
% 5.77/1.53 % (3458301)Instructions burned: 140 (million)
% 5.77/1.53 % (3458311)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2932301805:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 5.77/1.53 % (3458310)lrs+10_1_sil=8000:sp=occurrence:random_seed=4164946954:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 5.77/1.53 % (3458299)------------------------------
% 5.77/1.53 % (3458299)------------------------------
% 5.77/1.53 % (3458312)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3779063155:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 5.77/1.53 % (3458311)Instruction limit reached!
% 5.77/1.53 % (3458311)------------------------------
% 5.77/1.53 % (3458311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458311)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458311)Termination reason: Instruction limit
% 5.77/1.53 % (3458311)Termination phase: Saturation
% 5.77/1.53 % (3458311)Time elapsed: 0.077 s
% 5.77/1.53 % (3458311)Peak memory usage: 91 MB
% 5.77/1.53 % (3458311)Instructions burned: 159 (million)
% 5.77/1.53 % (3458315)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=94950726:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.77/1.53 % (3458310)Instruction limit reached!
% 5.77/1.53 % (3458310)------------------------------
% 5.77/1.53 % (3458310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458310)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458310)Termination reason: Instruction limit
% 5.77/1.53 % (3458310)Termination phase: Saturation
% 5.77/1.53 % (3458310)Time elapsed: 0.188 s
% 5.77/1.53 % (3458310)Peak memory usage: 92 MB
% 5.77/1.53 % (3458310)Instructions burned: 286 (million)
% 5.77/1.53 % (3458312)Instruction limit reached!
% 5.77/1.53 % (3458312)------------------------------
% 5.77/1.53 % (3458312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458312)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458312)Termination reason: Instruction limit
% 5.77/1.53 % (3458312)Termination phase: Saturation
% 5.77/1.53 % (3458312)Time elapsed: 0.188 s
% 5.77/1.53 % (3458312)Peak memory usage: 92 MB
% 5.77/1.53 % (3458312)Instructions burned: 325 (million)
% 5.77/1.53 % (3458317)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2556117525:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 5.77/1.53 % (3458298)First to succeed.
% 5.77/1.53 % (3458298)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3458291"
% 5.77/1.53 % (3458315)Instruction limit reached!
% 5.77/1.53 % (3458315)------------------------------
% 5.77/1.53 % (3458315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458315)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458315)Termination reason: Instruction limit
% 5.77/1.53 % (3458315)Termination phase: Saturation
% 5.77/1.53 % (3458315)Time elapsed: 0.144 s
% 5.77/1.53 % (3458315)Peak memory usage: 94 MB
% 5.77/1.53 % (3458315)Instructions burned: 248 (million)
% 5.77/1.53 % (3458319)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3654044647:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 5.77/1.53 % (3458320)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3822105908:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 5.77/1.53 % (3458317)Instruction limit reached!
% 5.77/1.53 % (3458317)------------------------------
% 5.77/1.53 % (3458317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.53 % (3458317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.53 % (3458317)CaDiCaL version: 2.1.3
% 5.77/1.53 % (3458317)Termination reason: Instruction limit
% 5.77/1.53 % (3458317)Termination phase: Saturation
% 5.77/1.53 % (3458317)Time elapsed: 0.180 s
% 5.77/1.53 % (3458317)Peak memory usage: 90 MB
% 5.77/1.53 % (3458317)Instructions burned: 294 (million)
% 5.77/1.53 % (3458298)Refutation found. Thanks to Tanya!
% 5.77/1.53 % SZS status Theorem for theBenchmark
% 5.77/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 6.63/1.62 % (3458298)------------------------------
% 6.63/1.62 % (3458298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.63/1.62 % (3458298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.63/1.62 % (3458298)CaDiCaL version: 2.1.3
% 6.63/1.62 % (3458298)Termination reason: Refutation
% 6.63/1.62 % (3458298)Time elapsed: 0.571 s
% 6.63/1.62 % (3458298)Peak memory usage: 137 MB
% 6.63/1.62 % (3458298)Instructions burned: 1581 (million)
% 6.63/1.62 % (3458298)------------------------------
% 6.63/1.62 % (3458298)------------------------------
% 6.63/1.62 % (3458291)Success in time 0.863 s
% 6.63/1.62 % Vampire exiting
%------------------------------------------------------------------------------