%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX024+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 : n026.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 1.03s 0.41s
% Output : Refutation 1.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 16
% Syntax : Number of formulae : 107 ( 21 unt; 11 def)
% Number of atoms : 341 ( 45 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 362 ( 128 ~; 173 |; 33 &)
% ( 12 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 12 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-2 aty)
% Number of variables : 139 ( 1 sgn 108 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] : nil != cons(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id5) ).
fof(f45,axiom,
! [X0,X1] :
( member_succeeds(X0,X1)
<=> ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id45) ).
fof(f170,axiom,
! [X0,X1,X2,X3] :
( ( member_succeeds(X0,cons(X1,X3))
& X0 != X1 )
=> member_succeeds(X0,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(member:cons)') ).
fof(f218,axiom,
( ! [X0,X1,X2] :
( ( ? [X3,X4,X5] :
( X0 = cons(X3,X4)
& X2 = cons(X3,X5)
& append_succeeds(X4,X1,X5)
& ! [X6] :
( member_succeeds(X6,X5)
=> ( member_succeeds(X6,X4)
| member_succeeds(X6,X1) ) ) )
| ( X0 = nil
& X2 = X1 ) )
=> ! [X6] :
( member_succeeds(X6,X2)
=> ( member_succeeds(X6,X0)
| member_succeeds(X6,X1) ) ) )
=> ! [X0,X1,X2] :
( append_succeeds(X0,X1,X2)
=> ! [X6] :
( member_succeeds(X6,X2)
=> ( member_succeeds(X6,X0)
| member_succeeds(X6,X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f219,conjecture,
! [X0,X1,X2,X3] :
( ( append_succeeds(X1,X2,X3)
& member_succeeds(X0,X3) )
=> ( member_succeeds(X0,X1)
| member_succeeds(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(append:member:3)') ).
fof(f220,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( append_succeeds(X1,X2,X3)
& member_succeeds(X0,X3) )
=> ( member_succeeds(X0,X1)
| member_succeeds(X0,X2) ) ),
inference(negated_conjecture,[status(cth)],[f219]) ).
fof(f224,plain,
! [X0,X1,X3] :
( ( member_succeeds(X0,cons(X1,X3))
& X0 != X1 )
=> member_succeeds(X0,X3) ),
inference(rectify,[],[f170]) ).
fof(f225,plain,
( ! [X0,X1,X2] :
( ( ? [X3,X4,X5] :
( X0 = cons(X3,X4)
& X2 = cons(X3,X5)
& append_succeeds(X4,X1,X5)
& ! [X6] :
( member_succeeds(X6,X5)
=> ( member_succeeds(X6,X4)
| member_succeeds(X6,X1) ) ) )
| ( X0 = nil
& X2 = X1 ) )
=> ! [X7] :
( member_succeeds(X7,X2)
=> ( member_succeeds(X7,X0)
| member_succeeds(X7,X1) ) ) )
=> ! [X8,X9,X10] :
( append_succeeds(X8,X9,X10)
=> ! [X11] :
( member_succeeds(X11,X10)
=> ( member_succeeds(X11,X8)
| member_succeeds(X11,X9) ) ) ) ),
inference(rectify,[],[f218]) ).
fof(f414,plain,
! [X0,X1,X3] :
( member_succeeds(X0,X3)
| ~ member_succeeds(X0,cons(X1,X3))
| X0 = X1 ),
inference(ennf_transformation,[],[f224]) ).
fof(f415,plain,
! [X0,X1,X3] :
( member_succeeds(X0,X3)
| ~ member_succeeds(X0,cons(X1,X3))
| X0 = X1 ),
inference(flattening,[],[f414]) ).
fof(f484,plain,
( ! [X8,X9,X10] :
( ! [X11] :
( member_succeeds(X11,X8)
| member_succeeds(X11,X9)
| ~ member_succeeds(X11,X10) )
| ~ append_succeeds(X8,X9,X10) )
| ? [X0,X1,X2] :
( ? [X7] :
( ~ member_succeeds(X7,X0)
& ~ member_succeeds(X7,X1)
& member_succeeds(X7,X2) )
& ( ? [X3,X4,X5] :
( X0 = cons(X3,X4)
& X2 = cons(X3,X5)
& append_succeeds(X4,X1,X5)
& ! [X6] :
( member_succeeds(X6,X4)
| member_succeeds(X6,X1)
| ~ member_succeeds(X6,X5) ) )
| ( X0 = nil
& X2 = X1 ) ) ) ),
inference(ennf_transformation,[],[f225]) ).
fof(f485,plain,
( ! [X8,X9,X10] :
( ! [X11] :
( member_succeeds(X11,X8)
| member_succeeds(X11,X9)
| ~ member_succeeds(X11,X10) )
| ~ append_succeeds(X8,X9,X10) )
| ? [X0,X1,X2] :
( ? [X7] :
( ~ member_succeeds(X7,X0)
& ~ member_succeeds(X7,X1)
& member_succeeds(X7,X2) )
& ( ? [X3,X4,X5] :
( X0 = cons(X3,X4)
& X2 = cons(X3,X5)
& append_succeeds(X4,X1,X5)
& ! [X6] :
( member_succeeds(X6,X4)
| member_succeeds(X6,X1)
| ~ member_succeeds(X6,X5) ) )
| ( X0 = nil
& X2 = X1 ) ) ) ),
inference(flattening,[],[f484]) ).
fof(f486,plain,
? [X0,X1,X2,X3] :
( ~ member_succeeds(X0,X1)
& ~ member_succeeds(X0,X2)
& append_succeeds(X1,X2,X3)
& member_succeeds(X0,X3) ),
inference(ennf_transformation,[],[f220]) ).
fof(f487,plain,
? [X0,X1,X2,X3] :
( ~ member_succeeds(X0,X1)
& ~ member_succeeds(X0,X2)
& append_succeeds(X1,X2,X3)
& member_succeeds(X0,X3) ),
inference(flattening,[],[f486]) ).
fof(f492,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[],[f5]) ).
fof(f586,plain,
! [X2,X3,X0,X1] :
( ~ member_succeeds(X0,X3)
| cons(X2,X3) != X1
| member_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
fof(f589,plain,
! [X0,X1,X4] :
( cons(X0,X4) != X1
| member_succeeds(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
fof(f823,plain,
! [X3,X0,X1] :
( ~ member_succeeds(X0,cons(X1,X3))
| X0 = X1
| member_succeeds(X0,X3) ),
inference(cnf_transformation,[],[f415]) ).
fof(f876,plain,
! [X10,X11,X8,X6,X9] :
( sK91 = sK92
| ~ member_succeeds(X6,sK96)
| member_succeeds(X6,sK91)
| member_succeeds(X6,sK95)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f879,plain,
! [X10,X11,X8,X9] :
( sK91 = sK92
| sK90 = cons(sK94,sK95)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f881,plain,
! [X10,X11,X8,X9] :
( nil = sK90
| sK92 = cons(sK94,sK96)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f883,plain,
! [X10,X11,X8,X9] :
( ~ member_succeeds(sK93,sK90)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f884,plain,
! [X10,X11,X8,X9] :
( ~ member_succeeds(sK93,sK91)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f885,plain,
! [X10,X11,X8,X9] :
( member_succeeds(sK93,sK92)
| ~ append_succeeds(X8,X9,X10)
| ~ member_succeeds(X11,X10)
| member_succeeds(X11,X9)
| member_succeeds(X11,X8) ),
inference(cnf_transformation,[],[f485]) ).
fof(f886,plain,
member_succeeds(sK97,sK100),
inference(cnf_transformation,[],[f487]) ).
fof(f887,plain,
append_succeeds(sK98,sK99,sK100),
inference(cnf_transformation,[],[f487]) ).
fof(f888,plain,
~ member_succeeds(sK97,sK99),
inference(cnf_transformation,[],[f487]) ).
fof(f889,plain,
~ member_succeeds(sK97,sK98),
inference(cnf_transformation,[],[f487]) ).
fof(f918,plain,
! [X0,X4] : member_succeeds(X0,cons(X0,X4)),
inference(equality_resolution,[],[f589]) ).
fof(f919,plain,
! [X2,X3,X0] :
( member_succeeds(X0,cons(X2,X3))
| ~ member_succeeds(X0,X3) ),
inference(equality_resolution,[],[f586]) ).
fof(f978,definition,
( spl101_1
<=> ! [X10,X11,X9,X8] :
( ~ append_succeeds(X8,X9,X10)
| member_succeeds(X11,X8)
| member_succeeds(X11,X9)
| ~ member_succeeds(X11,X10) ) ),
introduced(definition,[new_symbols(definition,[spl101_1])],[avatar_definition]) ).
fof(f979,plain,
( ! [X10,X11,X8,X9] :
( ~ append_succeeds(X8,X9,X10)
| member_succeeds(X11,X8)
| member_succeeds(X11,X9)
| ~ member_succeeds(X11,X10) )
| ~ spl101_1 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f981,definition,
( spl101_2
<=> ! [X6] :
( ~ member_succeeds(X6,sK96)
| member_succeeds(X6,sK95)
| member_succeeds(X6,sK91) ) ),
introduced(definition,[new_symbols(definition,[spl101_2])],[avatar_definition]) ).
fof(f982,plain,
( ! [X6] :
( ~ member_succeeds(X6,sK96)
| member_succeeds(X6,sK95)
| member_succeeds(X6,sK91) )
| ~ spl101_2 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,definition,
( spl101_3
<=> nil = sK90 ),
introduced(definition,[new_symbols(definition,[spl101_3])],[avatar_definition]) ).
fof(f986,plain,
( nil = sK90
| ~ spl101_3 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f989,definition,
( spl101_4
<=> sK91 = sK92 ),
introduced(definition,[new_symbols(definition,[spl101_4])],[avatar_definition]) ).
fof(f991,plain,
( sK91 = sK92
| ~ spl101_4 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f992,plain,
( spl101_1
| spl101_2
| spl101_4 ),
inference(avatar_split_clause,[],[f876,f989,f981,f978]) ).
fof(f999,definition,
( spl101_6
<=> sK92 = cons(sK94,sK96) ),
introduced(definition,[new_symbols(definition,[spl101_6])],[avatar_definition]) ).
fof(f1001,plain,
( sK92 = cons(sK94,sK96)
| ~ spl101_6 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1004,definition,
( spl101_7
<=> sK90 = cons(sK94,sK95) ),
introduced(definition,[new_symbols(definition,[spl101_7])],[avatar_definition]) ).
fof(f1006,plain,
( sK90 = cons(sK94,sK95)
| ~ spl101_7 ),
inference(avatar_component_clause,[],[f1004]) ).
fof(f1007,plain,
( spl101_1
| spl101_7
| spl101_4 ),
inference(avatar_split_clause,[],[f879,f989,f1004,f978]) ).
fof(f1009,plain,
( spl101_1
| spl101_6
| spl101_3 ),
inference(avatar_split_clause,[],[f881,f984,f999,f978]) ).
fof(f1012,definition,
( spl101_8
<=> member_succeeds(sK93,sK90) ),
introduced(definition,[new_symbols(definition,[spl101_8])],[avatar_definition]) ).
fof(f1014,plain,
( ~ member_succeeds(sK93,sK90)
| spl101_8 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1015,plain,
( spl101_1
| ~ spl101_8 ),
inference(avatar_split_clause,[],[f883,f1012,f978]) ).
fof(f1017,definition,
( spl101_9
<=> member_succeeds(sK93,sK91) ),
introduced(definition,[new_symbols(definition,[spl101_9])],[avatar_definition]) ).
fof(f1019,plain,
( ~ member_succeeds(sK93,sK91)
| spl101_9 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1020,plain,
( spl101_1
| ~ spl101_9 ),
inference(avatar_split_clause,[],[f884,f1017,f978]) ).
fof(f1022,definition,
( spl101_10
<=> member_succeeds(sK93,sK92) ),
introduced(definition,[new_symbols(definition,[spl101_10])],[avatar_definition]) ).
fof(f1024,plain,
( member_succeeds(sK93,sK92)
| ~ spl101_10 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1025,plain,
( spl101_1
| spl101_10 ),
inference(avatar_split_clause,[],[f885,f1022,f978]) ).
fof(f1197,plain,
( ! [X0] :
( ~ member_succeeds(X0,sK100)
| member_succeeds(X0,sK99)
| member_succeeds(X0,sK98) )
| ~ spl101_1 ),
inference(resolution,[],[f979,f887]) ).
fof(f1202,plain,
( member_succeeds(sK97,sK99)
| member_succeeds(sK97,sK98)
| ~ spl101_1 ),
inference(resolution,[],[f1197,f886]) ).
fof(f1203,plain,
( member_succeeds(sK97,sK98)
| ~ spl101_1 ),
inference(forward_subsumption_resolution,[],[f1202,f888]) ).
fof(f1204,plain,
( $false
| ~ spl101_1 ),
inference(forward_subsumption_resolution,[],[f1203,f889]) ).
fof(f1205,plain,
~ spl101_1,
inference(avatar_contradiction_clause,[],[f1204]) ).
fof(f1234,plain,
( member_succeeds(sK93,sK91)
| ~ spl101_4
| ~ spl101_10 ),
inference(forward_demodulation,[],[f1024,f991]) ).
fof(f1235,plain,
( $false
| ~ spl101_4
| spl101_9
| ~ spl101_10 ),
inference(forward_subsumption_resolution,[],[f1234,f1019]) ).
fof(f1236,plain,
( ~ spl101_4
| spl101_9
| ~ spl101_10 ),
inference(avatar_contradiction_clause,[],[f1235]) ).
fof(f1237,plain,
( nil = cons(sK94,sK95)
| ~ spl101_3
| ~ spl101_7 ),
inference(forward_demodulation,[],[f1006,f986]) ).
fof(f1238,plain,
( $false
| ~ spl101_3
| ~ spl101_7 ),
inference(forward_subsumption_resolution,[],[f1237,f492]) ).
fof(f1239,plain,
( ~ spl101_3
| ~ spl101_7 ),
inference(avatar_contradiction_clause,[],[f1238]) ).
fof(f1292,plain,
( ! [X0] :
( ~ member_succeeds(X0,sK92)
| sK94 = X0
| member_succeeds(X0,sK96) )
| ~ spl101_6 ),
inference(superposition,[],[f823,f1001]) ).
fof(f1379,plain,
( member_succeeds(sK94,sK90)
| ~ spl101_7 ),
inference(superposition,[],[f918,f1006]) ).
fof(f1380,plain,
( ! [X0] :
( ~ member_succeeds(X0,sK95)
| member_succeeds(X0,sK90) )
| ~ spl101_7 ),
inference(superposition,[],[f919,f1006]) ).
fof(f2001,plain,
( sK93 = sK94
| member_succeeds(sK93,sK96)
| ~ spl101_6
| ~ spl101_10 ),
inference(resolution,[],[f1292,f1024]) ).
fof(f2004,definition,
( spl101_51
<=> member_succeeds(sK93,sK96) ),
introduced(definition,[new_symbols(definition,[spl101_51])],[avatar_definition]) ).
fof(f2006,plain,
( member_succeeds(sK93,sK96)
| ~ spl101_51 ),
inference(avatar_component_clause,[],[f2004]) ).
fof(f2008,definition,
( spl101_52
<=> sK93 = sK94 ),
introduced(definition,[new_symbols(definition,[spl101_52])],[avatar_definition]) ).
fof(f2010,plain,
( sK93 = sK94
| ~ spl101_52 ),
inference(avatar_component_clause,[],[f2008]) ).
fof(f2011,plain,
( spl101_51
| spl101_52
| ~ spl101_6
| ~ spl101_10 ),
inference(avatar_split_clause,[],[f2001,f1022,f999,f2008,f2004]) ).
fof(f2014,plain,
( member_succeeds(sK93,sK95)
| member_succeeds(sK93,sK91)
| ~ spl101_2
| ~ spl101_51 ),
inference(resolution,[],[f2006,f982]) ).
fof(f2016,plain,
( member_succeeds(sK93,sK95)
| ~ spl101_2
| spl101_9
| ~ spl101_51 ),
inference(forward_subsumption_resolution,[],[f2014,f1019]) ).
fof(f2017,plain,
( member_succeeds(sK93,sK90)
| ~ spl101_2
| ~ spl101_7
| spl101_9
| ~ spl101_51 ),
inference(resolution,[],[f2016,f1380]) ).
fof(f2021,plain,
( $false
| ~ spl101_2
| ~ spl101_7
| spl101_8
| spl101_9
| ~ spl101_51 ),
inference(forward_subsumption_resolution,[],[f2017,f1014]) ).
fof(f2022,plain,
( ~ spl101_2
| ~ spl101_7
| spl101_8
| spl101_9
| ~ spl101_51 ),
inference(avatar_contradiction_clause,[],[f2021]) ).
fof(f2026,plain,
( ~ member_succeeds(sK94,sK90)
| spl101_8
| ~ spl101_52 ),
inference(superposition,[],[f1014,f2010]) ).
fof(f2028,plain,
( $false
| ~ spl101_7
| spl101_8
| ~ spl101_52 ),
inference(forward_subsumption_resolution,[],[f2026,f1379]) ).
fof(f2029,plain,
( ~ spl101_7
| spl101_8
| ~ spl101_52 ),
inference(avatar_contradiction_clause,[],[f2028]) ).
cnf(s2,plain,
( spl101_1
| spl101_2
| spl101_4 ),
inference(sat_conversion,[],[f992]) ).
cnf(s5,plain,
( spl101_1
| spl101_4
| spl101_7 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s7,plain,
( spl101_1
| spl101_3
| spl101_6 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s9,plain,
( spl101_1
| ~ spl101_8 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s10,plain,
( spl101_1
| ~ spl101_9 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s11,plain,
( spl101_1
| spl101_10 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s17,plain,
~ spl101_1,
inference(sat_conversion,[],[f1205]) ).
cnf(s18,plain,
( ~ spl101_4
| spl101_9
| ~ spl101_10 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s19,plain,
( ~ spl101_3
| ~ spl101_7 ),
inference(sat_conversion,[],[f1239]) ).
cnf(s44,plain,
( ~ spl101_6
| ~ spl101_10
| spl101_51
| spl101_52 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s45,plain,
( ~ spl101_2
| ~ spl101_7
| spl101_8
| spl101_9
| ~ spl101_51 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s46,plain,
( ~ spl101_7
| spl101_8
| ~ spl101_52 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s48,plain,
spl101_10,
inference(rat,[],[s11,s17]) ).
cnf(s49,plain,
~ spl101_9,
inference(rat,[],[s10,s17]) ).
cnf(s50,plain,
~ spl101_4,
inference(rat,[],[s18,s48,s49]) ).
cnf(s51,plain,
~ spl101_8,
inference(rat,[],[s9,s17]) ).
cnf(s53,plain,
( spl101_3
| spl101_6 ),
inference(rat,[],[s7,s17]) ).
cnf(s55,plain,
spl101_7,
inference(rat,[],[s5,s50,s17]) ).
cnf(s56,plain,
~ spl101_52,
inference(rat,[],[s46,s51,s55]) ).
cnf(s57,plain,
~ spl101_3,
inference(rat,[],[s19,s55]) ).
cnf(s58,plain,
spl101_6,
inference(rat,[],[s53,s57]) ).
cnf(s60,plain,
spl101_51,
inference(rat,[],[s44,s56,s48,s58]) ).
cnf(s62,plain,
~ spl101_2,
inference(rat,[],[s45,s55,s49,s51,s60]) ).
cnf(s64,plain,
$false,
inference(rat,[],[s2,s50,s62,s17]) ).
fof(f2030,plain,
$false,
inference(avatar_sat_refutation,[],[s64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX024+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.19 % Computer : n026.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:54:42 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 1.03/0.41 % (3910266)Will run a generic schedule for satisfiability detection.
% 1.03/0.41 % (3910272)% WARNING: option uhcvi not known.
% 1.03/0.41 % (3910277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2940742370:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.03/0.41 % (3910271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1681331090_2999 on theBenchmark for (2999ds/0Mi)
% 1.03/0.41 % (3910274)dis+10_1_sil=32000:sp=arity:random_seed=4176238363:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.03/0.41 % (3910273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1838897170:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.03/0.41 % (3910275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3555399825:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.03/0.41 % (3910276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=425115199:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.03/0.41 % (3910272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2054752253:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.03/0.41 % TRYING [1]
% 1.03/0.41 % TRYING [2]
% 1.03/0.41 % TRYING [3]
% 1.03/0.41 % (3910274)Instruction limit reached!
% 1.03/0.41 % (3910274)------------------------------
% 1.03/0.41 % (3910274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.03/0.41 % (3910274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.03/0.41 % (3910274)CaDiCaL version: 2.1.3
% 1.03/0.41 % (3910274)Termination reason: Instruction limit
% 1.03/0.41 % (3910274)Termination phase: Saturation
% 1.03/0.41 % (3910274)Time elapsed: 0.071 s
% 1.03/0.41 % (3910274)Peak memory usage: 13 MB
% 1.03/0.41 % (3910274)Instructions burned: 104 (million)
% 1.03/0.41 % (3910275)Instruction limit reached!
% 1.03/0.41 % (3910275)------------------------------
% 1.03/0.41 % (3910275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.03/0.41 % (3910275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.03/0.41 % (3910275)CaDiCaL version: 2.1.3
% 1.03/0.41 % (3910275)Termination reason: Instruction limit
% 1.03/0.41 % (3910275)Termination phase: Saturation
% 1.03/0.41 % (3910275)Time elapsed: 0.073 s
% 1.03/0.41 % (3910275)Peak memory usage: 13 MB
% 1.03/0.41 % (3910275)Instructions burned: 116 (million)
% 1.03/0.41 % TRYING [4]
% 1.03/0.41 % (3910276)Instruction limit reached!
% 1.03/0.41 % (3910276)------------------------------
% 1.03/0.41 % (3910276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.03/0.41 % (3910276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.03/0.41 % (3910276)CaDiCaL version: 2.1.3
% 1.03/0.41 % (3910276)Termination reason: Instruction limit
% 1.03/0.41 % (3910276)Termination phase: Saturation
% 1.03/0.41 % (3910276)Time elapsed: 0.084 s
% 1.03/0.41 % (3910276)Peak memory usage: 14 MB
% 1.03/0.41 % (3910276)Instructions burned: 132 (million)
% 1.03/0.41 % (3910285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3098021493:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.03/0.41 % (3910286)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3902862348:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.03/0.41 % (3910287)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=2249102357:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.03/0.41 % (3910277)Instruction limit reached!
% 1.03/0.41 % (3910277)------------------------------
% 1.03/0.41 % (3910277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.03/0.41 % (3910277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.03/0.41 % (3910277)CaDiCaL version: 2.1.3
% 1.03/0.41 % (3910277)Termination reason: Instruction limit
% 1.03/0.41 % (3910277)Termination phase: Saturation
% 1.03/0.41 % (3910277)Time elapsed: 0.107 s
% 1.03/0.41 % (3910277)Peak memory usage: 14 MB
% 1.03/0.41 % (3910277)Instructions burned: 160 (million)
% 1.03/0.41 % TRYING [1]
% 1.03/0.41 % TRYING [2]
% 1.03/0.41 % (3910291)ott-21_1_sil=16000:fs=off:random_seed=1950680258:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.03/0.41 % TRYING [3]
% 1.03/0.41 % (3910287) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3910266-3910287"...
% 1.03/0.41 % (3910287)...printing done.
% 1.03/0.41 % (3910287)Refutation found. Thanks to Tanya!
% 1.03/0.41 % SZS status Theorem for theBenchmark
% 1.03/0.41 % SZS output start Proof for theBenchmark
% See solution above
% 1.03/0.41 % (3910287)------------------------------
% 1.03/0.41 % (3910287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.03/0.41 % (3910287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.03/0.41 % (3910287)CaDiCaL version: 2.1.3
% 1.03/0.41 % (3910287)Termination reason: Refutation
% 1.03/0.41 % (3910287)Time elapsed: 0.041 s
% 1.03/0.41 % (3910287)Peak memory usage: 14 MB
% 1.03/0.41 % (3910287)Instructions burned: 57 (million)
% 1.03/0.41 % (3910266)Success in time 0.182 s
% 1.03/0.41 % Vampire exiting
%------------------------------------------------------------------------------