%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC299-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:03:21 PM UTC 2026
% Result : Unsatisfiable 5.60s 1.15s
% Output : Refutation 5.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 38
% Syntax : Number of formulae : 170 ( 38 unt; 19 def)
% Number of atoms : 473 ( 115 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 582 ( 279 ~; 291 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 13 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-2 aty)
% Number of variables : 27 ( 0 sgn 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f77,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f121,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f122,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X0 ),
inference(reorient_equations,[],[f121]) ).
fof(f123,axiom,
! [X0,X1] :
( app(X0,X1) != nil
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f124,plain,
! [X0,X1] :
( nil != app(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| nil = X1 ),
inference(reorient_equations,[],[f123]) ).
fof(f144,axiom,
! [X0,X1] :
( ~ ssList(X1)
| ~ ssList(X0)
| nil = X1
| tl(app(X1,X0)) = app(tl(X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f215,negated_conjecture,
( ssItem(sk10)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_15) ).
fof(f226,negated_conjecture,
( cons(sk10,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_24) ).
fof(f227,plain,
( sk3 = cons(sk10,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f226]) ).
fof(f234,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(definition_unfolding,[],[f212,f205]) ).
fof(f259,definition,
sF0 = cons(sk5,nil),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f260,plain,
cons(sk5,nil) = sF0,
inference(reorient_equations,[],[f259]) ).
fof(f261,definition,
sF1 = app(sk7,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f262,plain,
app(sk7,sF0) = sF1,
inference(reorient_equations,[],[f261]) ).
fof(f263,definition,
sF2 = app(sF1,sk8),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f264,plain,
app(sF1,sk8) = sF2,
inference(reorient_equations,[],[f263]) ).
fof(f265,definition,
sF3 = cons(sk6,nil),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f266,plain,
cons(sk6,nil) = sF3,
inference(reorient_equations,[],[f265]) ).
fof(f267,definition,
sF4 = app(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f268,plain,
app(sF2,sF3) = sF4,
inference(reorient_equations,[],[f267]) ).
fof(f269,definition,
sF5 = app(sF4,sk9),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f270,plain,
app(sF4,sk9) = sF5,
inference(reorient_equations,[],[f269]) ).
fof(f271,plain,
sk3 = sF5,
inference(definition_folding,[],[f234,f270,f268,f266,f264,f262,f260]) ).
fof(f272,definition,
sF6 = cons(sk10,nil),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f273,plain,
cons(sk10,nil) = sF6,
inference(reorient_equations,[],[f272]) ).
fof(f280,plain,
( sk3 = sF6
| nil = sk3 ),
inference(definition_folding,[],[f227,f273]) ).
fof(f289,definition,
( spl9_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
fof(f291,plain,
( nil = sk3
| ~ spl9_1 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f306,definition,
( spl9_5
<=> sk3 = sF6 ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
fof(f308,plain,
( sk3 = sF6
| ~ spl9_5 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( spl9_1
| spl9_5 ),
inference(avatar_split_clause,[],[f280,f306,f289]) ).
fof(f331,definition,
( spl9_9
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
fof(f333,plain,
( ssItem(sk10)
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f334,plain,
( spl9_1
| spl9_9 ),
inference(avatar_split_clause,[],[f215,f331,f289]) ).
fof(f341,definition,
( spl9_11
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f342,plain,
( ssList(nil)
| ~ spl9_11 ),
inference(avatar_component_clause,[],[f341]) ).
fof(f377,plain,
spl9_11,
inference(avatar_split_clause,[],[f8,f341]) ).
fof(f378,plain,
sk3 = app(sF4,sk9),
inference(forward_demodulation,[],[f270,f271]) ).
fof(f379,plain,
( ssList(sF0)
| ~ ssList(nil)
| ~ ssItem(sk5) ),
inference(superposition,[],[f86,f260]) ).
fof(f380,plain,
( ssList(sF3)
| ~ ssList(nil)
| ~ ssItem(sk6) ),
inference(superposition,[],[f86,f266]) ).
fof(f383,plain,
( ssList(sF3)
| ~ ssItem(sk6)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f380,f342]) ).
fof(f384,plain,
( ssList(sF0)
| ~ ssItem(sk5)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f379,f342]) ).
fof(f386,plain,
( ssList(sF3)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f383,f207]) ).
fof(f387,plain,
( ssList(sF0)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f384,f206]) ).
fof(f389,plain,
( ssList(sF1)
| ~ ssList(sk7)
| ~ ssList(sF0) ),
inference(superposition,[],[f85,f262]) ).
fof(f391,plain,
( ssList(sF2)
| ~ ssList(sF1)
| ~ ssList(sk8) ),
inference(superposition,[],[f85,f264]) ).
fof(f392,plain,
( ssList(sF4)
| ~ ssList(sF2)
| ~ ssList(sF3) ),
inference(superposition,[],[f85,f268]) ).
fof(f396,plain,
( ssList(sF4)
| ~ ssList(sF2)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f392,f386]) ).
fof(f397,plain,
( ssList(sF2)
| ~ ssList(sF1) ),
inference(forward_subsumption_resolution,[],[f391,f209]) ).
fof(f399,plain,
( ssList(sF1)
| ~ ssList(sF0) ),
inference(forward_subsumption_resolution,[],[f389,f208]) ).
fof(f402,definition,
( spl9_19
<=> ssList(sF2) ),
introduced(definition,[new_symbols(definition,[spl9_19])],[avatar_definition]) ).
fof(f403,plain,
( ssList(sF2)
| ~ spl9_19 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,definition,
( spl9_20
<=> ssList(sF4) ),
introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition]) ).
fof(f408,plain,
( ssList(sF4)
| ~ spl9_20 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f409,plain,
( ~ spl9_19
| spl9_20
| ~ spl9_11 ),
inference(avatar_split_clause,[],[f396,f341,f406,f402]) ).
fof(f411,definition,
( spl9_21
<=> ssList(sF1) ),
introduced(definition,[new_symbols(definition,[spl9_21])],[avatar_definition]) ).
fof(f412,plain,
( ssList(sF1)
| ~ spl9_21 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
( ~ spl9_21
| spl9_19 ),
inference(avatar_split_clause,[],[f397,f402,f411]) ).
fof(f416,plain,
( ssList(sF1)
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f399,f387]) ).
fof(f417,plain,
( spl9_21
| ~ spl9_11 ),
inference(avatar_split_clause,[],[f416,f341,f411]) ).
fof(f418,plain,
( nil != sF0
| ~ ssItem(sk5)
| ~ ssList(nil) ),
inference(superposition,[],[f99,f260]) ).
fof(f419,plain,
( nil != sF3
| ~ ssItem(sk6)
| ~ ssList(nil) ),
inference(superposition,[],[f99,f266]) ).
fof(f422,plain,
( nil != sF3
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[],[f419,f207]) ).
fof(f423,plain,
( nil != sF0
| ~ ssList(nil) ),
inference(forward_subsumption_resolution,[],[f418,f206]) ).
fof(f425,plain,
( nil != sF3
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f422,f342]) ).
fof(f426,plain,
( nil != sF0
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f423,f342]) ).
fof(f449,plain,
( sF1 = app(sF1,nil)
| ~ spl9_21 ),
inference(resolution,[],[f73,f412]) ).
fof(f455,plain,
( nil != sF1
| ~ ssList(sF0)
| ~ ssList(sk7)
| nil = sF0 ),
inference(superposition,[],[f124,f262]) ).
fof(f457,plain,
( nil != sF2
| ~ ssList(sk8)
| ~ ssList(sF1)
| nil = sk8 ),
inference(superposition,[],[f124,f264]) ).
fof(f458,plain,
( nil != sF4
| ~ ssList(sF3)
| ~ ssList(sF2)
| nil = sF3 ),
inference(superposition,[],[f124,f268]) ).
fof(f462,plain,
( nil != sF4
| ~ ssList(sF2)
| nil = sF3
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f458,f386]) ).
fof(f463,plain,
( nil != sF2
| ~ ssList(sF1)
| nil = sk8 ),
inference(forward_subsumption_resolution,[],[f457,f209]) ).
fof(f465,plain,
( nil != sF1
| ~ ssList(sk7)
| nil = sF0
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f455,f387]) ).
fof(f467,plain,
( nil != sF4
| nil = sF3
| ~ spl9_11
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f462,f403]) ).
fof(f468,plain,
( nil != sF2
| nil = sk8
| ~ spl9_21 ),
inference(forward_subsumption_resolution,[],[f463,f412]) ).
fof(f470,plain,
( nil != sF1
| nil = sF0
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f465,f208]) ).
fof(f472,plain,
( nil != sF4
| ~ spl9_11
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f467,f425]) ).
fof(f474,definition,
( spl9_22
<=> nil = sk8 ),
introduced(definition,[new_symbols(definition,[spl9_22])],[avatar_definition]) ).
fof(f476,plain,
( nil = sk8
| ~ spl9_22 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f478,definition,
( spl9_23
<=> nil = sF2 ),
introduced(definition,[new_symbols(definition,[spl9_23])],[avatar_definition]) ).
fof(f479,plain,
( nil = sF2
| ~ spl9_23 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( nil != sF2
| spl9_23 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f481,plain,
( spl9_22
| ~ spl9_23
| ~ spl9_21 ),
inference(avatar_split_clause,[],[f468,f411,f478,f474]) ).
fof(f483,plain,
( nil != sF1
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f470,f426]) ).
fof(f551,plain,
( nil != sk3
| ~ ssList(sk9)
| ~ ssList(sF4)
| nil = sF4 ),
inference(superposition,[],[f122,f378]) ).
fof(f605,plain,
( ! [X0] :
( ~ ssList(X0)
| nil = sF2
| tl(app(sF2,X0)) = app(tl(sF2),X0) )
| ~ spl9_19 ),
inference(resolution,[],[f144,f403]) ).
fof(f607,plain,
( ! [X0] :
( ~ ssList(X0)
| nil = sF4
| tl(app(sF4,X0)) = app(tl(sF4),X0) )
| ~ spl9_20 ),
inference(resolution,[],[f144,f408]) ).
fof(f610,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sF4,X0)) = app(tl(sF4),X0) )
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f607,f472]) ).
fof(f612,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(app(sF2,X0)) = app(tl(sF2),X0) )
| ~ spl9_19
| spl9_23 ),
inference(forward_subsumption_resolution,[],[f605,f480]) ).
fof(f657,plain,
( ~ ssList(sk9)
| ~ ssList(sF4)
| nil = sF4
| ~ spl9_1 ),
inference(forward_subsumption_resolution,[],[f551,f291]) ).
fof(f662,plain,
( ~ ssList(sF4)
| nil = sF4
| ~ spl9_1 ),
inference(forward_subsumption_resolution,[],[f657,f210]) ).
fof(f674,plain,
( nil = sF4
| ~ spl9_1
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f662,f408]) ).
fof(f678,plain,
( $false
| ~ spl9_1
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f674,f472]) ).
fof(f679,plain,
( ~ spl9_1
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(avatar_contradiction_clause,[],[f678]) ).
fof(f720,plain,
( sF2 = app(sF1,nil)
| ~ spl9_22 ),
inference(superposition,[],[f264,f476]) ).
fof(f721,plain,
( sF1 = sF2
| ~ spl9_21
| ~ spl9_22 ),
inference(forward_demodulation,[],[f720,f449]) ).
fof(f749,plain,
( tl(app(sF2,sF3)) = app(tl(sF2),sF3)
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(resolution,[],[f612,f386]) ).
fof(f811,plain,
( tl(app(sF4,sk9)) = app(tl(sF4),sk9)
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(resolution,[],[f610,f210]) ).
fof(f3946,plain,
( tl(sF4) = app(tl(sF2),sF3)
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(forward_demodulation,[],[f749,f268]) ).
fof(f4098,plain,
( ssList(tl(sF4))
| ~ ssList(tl(sF2))
| ~ ssList(sF3)
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(superposition,[],[f85,f3946]) ).
fof(f4100,plain,
( nil != tl(sF4)
| ~ ssList(sF3)
| ~ ssList(tl(sF2))
| nil = sF3
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(superposition,[],[f124,f3946]) ).
fof(f4109,plain,
( nil != tl(sF4)
| ~ ssList(tl(sF2))
| nil = sF3
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(forward_subsumption_resolution,[],[f4100,f386]) ).
fof(f4111,plain,
( ssList(tl(sF4))
| ~ ssList(tl(sF2))
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(forward_subsumption_resolution,[],[f4098,f386]) ).
fof(f4113,definition,
( spl9_72
<=> ssList(tl(sF4)) ),
introduced(definition,[new_symbols(definition,[spl9_72])],[avatar_definition]) ).
fof(f4114,plain,
( ssList(tl(sF4))
| ~ spl9_72 ),
inference(avatar_component_clause,[],[f4113]) ).
fof(f4117,definition,
( spl9_73
<=> ssList(tl(sF2)) ),
introduced(definition,[new_symbols(definition,[spl9_73])],[avatar_definition]) ).
fof(f4119,plain,
( ~ ssList(tl(sF2))
| spl9_73 ),
inference(avatar_component_clause,[],[f4117]) ).
fof(f4135,plain,
( nil != tl(sF4)
| ~ ssList(tl(sF2))
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(forward_subsumption_resolution,[],[f4109,f425]) ).
fof(f4141,definition,
( spl9_78
<=> nil = tl(sF4) ),
introduced(definition,[new_symbols(definition,[spl9_78])],[avatar_definition]) ).
fof(f4143,plain,
( nil != tl(sF4)
| spl9_78 ),
inference(avatar_component_clause,[],[f4141]) ).
fof(f4145,plain,
( ~ spl9_73
| spl9_72
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(avatar_split_clause,[],[f4111,f478,f402,f341,f4113,f4117]) ).
fof(f4146,plain,
( ~ spl9_73
| ~ spl9_78
| ~ spl9_11
| ~ spl9_19
| spl9_23 ),
inference(avatar_split_clause,[],[f4135,f478,f402,f341,f4141,f4117]) ).
fof(f4147,plain,
( ~ ssList(sF2)
| nil = sF2
| spl9_73 ),
inference(resolution,[],[f4119,f77]) ).
fof(f4148,plain,
( nil = sF2
| ~ spl9_19
| spl9_73 ),
inference(forward_subsumption_resolution,[],[f4147,f403]) ).
fof(f4149,plain,
( $false
| ~ spl9_19
| spl9_23
| spl9_73 ),
inference(forward_subsumption_resolution,[],[f4148,f480]) ).
fof(f4150,plain,
( ~ spl9_19
| spl9_23
| spl9_73 ),
inference(avatar_contradiction_clause,[],[f4149]) ).
fof(f5004,plain,
( ! [X0] :
( ~ ssList(X0)
| tl(cons(sk10,X0)) = X0 )
| ~ spl9_9 ),
inference(resolution,[],[f333,f96]) ).
fof(f5021,plain,
( nil = tl(cons(sk10,nil))
| ~ spl9_9
| ~ spl9_11 ),
inference(resolution,[],[f5004,f342]) ).
fof(f5054,plain,
( nil = tl(sF6)
| ~ spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f5021,f273]) ).
fof(f5063,plain,
( nil = tl(sk3)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11 ),
inference(forward_demodulation,[],[f5054,f308]) ).
fof(f5427,plain,
( tl(sk3) = app(tl(sF4),sk9)
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_demodulation,[],[f811,f378]) ).
fof(f5468,plain,
( nil = app(tl(sF4),sk9)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_demodulation,[],[f5427,f5063]) ).
fof(f5647,plain,
( nil != nil
| ~ ssList(sk9)
| ~ ssList(tl(sF4))
| nil = tl(sF4)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(superposition,[],[f122,f5468]) ).
fof(f5654,plain,
( ~ ssList(sk9)
| ~ ssList(tl(sF4))
| nil = tl(sF4)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(trivial_inequality_removal,[],[f5647]) ).
fof(f5660,plain,
( ~ ssList(tl(sF4))
| nil = tl(sF4)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f5654,f210]) ).
fof(f5666,plain,
( nil = tl(sF4)
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20
| ~ spl9_72 ),
inference(forward_subsumption_resolution,[],[f5660,f4114]) ).
fof(f5669,plain,
( $false
| ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20
| ~ spl9_72
| spl9_78 ),
inference(forward_subsumption_resolution,[],[f5666,f4143]) ).
fof(f5670,plain,
( ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20
| ~ spl9_72
| spl9_78 ),
inference(avatar_contradiction_clause,[],[f5669]) ).
fof(f5673,plain,
( nil = sF1
| ~ spl9_21
| ~ spl9_22
| ~ spl9_23 ),
inference(forward_demodulation,[],[f479,f721]) ).
fof(f5689,plain,
( $false
| ~ spl9_11
| ~ spl9_21
| ~ spl9_22
| ~ spl9_23 ),
inference(forward_subsumption_resolution,[],[f5673,f483]) ).
fof(f5690,plain,
( ~ spl9_11
| ~ spl9_21
| ~ spl9_22
| ~ spl9_23 ),
inference(avatar_contradiction_clause,[],[f5689]) ).
cnf(s4,plain,
( spl9_1
| spl9_5 ),
inference(sat_conversion,[],[f309]) ).
cnf(s13,plain,
( spl9_1
| spl9_9 ),
inference(sat_conversion,[],[f334]) ).
cnf(s24,plain,
spl9_11,
inference(sat_conversion,[],[f377]) ).
cnf(s25,plain,
( ~ spl9_11
| ~ spl9_19
| spl9_20 ),
inference(sat_conversion,[],[f409]) ).
cnf(s26,plain,
( spl9_19
| ~ spl9_21 ),
inference(sat_conversion,[],[f414]) ).
cnf(s27,plain,
( ~ spl9_11
| spl9_21 ),
inference(sat_conversion,[],[f417]) ).
cnf(s29,plain,
( ~ spl9_21
| spl9_22
| ~ spl9_23 ),
inference(sat_conversion,[],[f481]) ).
cnf(s39,plain,
( ~ spl9_1
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20 ),
inference(sat_conversion,[],[f679]) ).
cnf(s90,plain,
( ~ spl9_11
| ~ spl9_19
| spl9_23
| spl9_72
| ~ spl9_73 ),
inference(sat_conversion,[],[f4145]) ).
cnf(s91,plain,
( ~ spl9_11
| ~ spl9_19
| spl9_23
| ~ spl9_73
| ~ spl9_78 ),
inference(sat_conversion,[],[f4146]) ).
cnf(s92,plain,
( ~ spl9_19
| spl9_23
| spl9_73 ),
inference(sat_conversion,[],[f4150]) ).
cnf(s147,plain,
( ~ spl9_5
| ~ spl9_9
| ~ spl9_11
| ~ spl9_19
| ~ spl9_20
| ~ spl9_72
| spl9_78 ),
inference(sat_conversion,[],[f5670]) ).
cnf(s148,plain,
( ~ spl9_11
| ~ spl9_21
| ~ spl9_22
| ~ spl9_23 ),
inference(sat_conversion,[],[f5690]) ).
cnf(s151,plain,
spl9_21,
inference(rat,[],[s27,s24]) ).
cnf(s164,plain,
spl9_19,
inference(rat,[],[s26,s151]) ).
cnf(s165,plain,
spl9_20,
inference(rat,[],[s25,s24,s164]) ).
cnf(s166,plain,
~ spl9_1,
inference(rat,[],[s39,s165,s24,s164]) ).
cnf(s171,plain,
spl9_9,
inference(rat,[],[s13,s166]) ).
cnf(s176,plain,
spl9_5,
inference(rat,[],[s4,s166]) ).
cnf(s181,plain,
( spl9_23
| ~ spl9_73 ),
inference(rat,[],[s147,s91,s90,s176,s171,s165,s164,s24]) ).
cnf(s182,plain,
spl9_23,
inference(rat,[],[s181,s92,s164]) ).
cnf(s183,plain,
~ spl9_22,
inference(rat,[],[s148,s151,s24,s182]) ).
cnf(s184,plain,
$false,
inference(rat,[],[s29,s151,s182,s183]) ).
fof(f5703,plain,
$false,
inference(avatar_sat_refutation,[],[s184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC299-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.00/0.10 % Computer : n012.cluster.edu
% 0.00/0.10 % Model : x86_64 x86_64
% 0.00/0.10 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.10 % Memory : 8046.5625MB
% 0.00/0.10 % OS : Linux 6.8.0-71-generic
% 0.00/0.10 % CPULimit : 300
% 0.00/0.10 % WCLimit : 300
% 0.00/0.10 % DateTime : Mon Sep 28 08:57:35 UTC 2026
% 0.00/0.10 % CPUTime :
% 0.00/0.10 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.12 Running first-order theorem proving
% 0.08/0.12 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.60/1.15 % (3244346)Input is clausal, will run a generic CNF schedule.
% 5.60/1.15 % (3244351)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=2414157833:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.60/1.15 % (3244353)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3643858709:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.60/1.15 % (3244352)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4083132103:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.60/1.15 % (3244354)lrs+10_1_sil=8000:sp=occurrence:random_seed=734485785:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.60/1.15 % (3244355)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2585933265:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.60/1.15 % (3244357)dis-21_1_sil=8000:lcm=predicate:random_seed=375359599:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.60/1.15 % (3244356)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2814986699:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.60/1.15 % (3244354)Instruction limit reached!
% 5.60/1.15 % (3244354)------------------------------
% 5.60/1.15 % (3244354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244354)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244354)Termination reason: Instruction limit
% 5.60/1.15 % (3244354)Termination phase: Saturation
% 5.60/1.15 % (3244354)Time elapsed: 0.034 s
% 5.60/1.15 % (3244354)Peak memory usage: 89 MB
% 5.60/1.15 % (3244354)Instructions burned: 108 (million)
% 5.60/1.15 % (3244355)Instruction limit reached!
% 5.60/1.15 % (3244355)------------------------------
% 5.60/1.15 % (3244355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244355)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244355)Termination reason: Instruction limit
% 5.60/1.15 % (3244355)Termination phase: Saturation
% 5.60/1.15 % (3244355)Time elapsed: 0.038 s
% 5.60/1.15 % (3244355)Peak memory usage: 89 MB
% 5.60/1.15 % (3244355)Instructions burned: 117 (million)
% 5.60/1.15 % (3244357)Instruction limit reached!
% 5.60/1.15 % (3244357)------------------------------
% 5.60/1.15 % (3244357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244357)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244357)Termination reason: Instruction limit
% 5.60/1.15 % (3244357)Termination phase: Saturation
% 5.60/1.15 % (3244357)Time elapsed: 0.033 s
% 5.60/1.15 % (3244357)Peak memory usage: 89 MB
% 5.60/1.15 % (3244357)Instructions burned: 119 (million)
% 5.60/1.15 % (3244356)Instruction limit reached!
% 5.60/1.15 % (3244356)------------------------------
% 5.60/1.15 % (3244356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244356)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244356)Termination reason: Instruction limit
% 5.60/1.15 % (3244356)Termination phase: Saturation
% 5.60/1.15 % (3244356)Time elapsed: 0.065 s
% 5.60/1.15 % (3244356)Peak memory usage: 90 MB
% 5.60/1.15 % (3244356)Instructions burned: 183 (million)
% 5.60/1.15 % (3244367)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2128125685:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 5.60/1.15 % (3244365)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1875638128:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.60/1.15 % (3244366)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1448326511:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 5.60/1.15 % (3244368)lrs+10_64_to=lpo:sil=8000:random_seed=1298375524:i=126:bd=preordered_2998 on theBenchmark for (2998ds/126Mi)
% 5.60/1.15 % (3244365)Instruction limit reached!
% 5.60/1.15 % (3244365)------------------------------
% 5.60/1.15 % (3244365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244365)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244365)Termination reason: Instruction limit
% 5.60/1.15 % (3244365)Termination phase: Saturation
% 5.60/1.15 % (3244365)Time elapsed: 0.051 s
% 5.60/1.15 % (3244365)Peak memory usage: 90 MB
% 5.60/1.15 % (3244365)Instructions burned: 143 (million)
% 5.60/1.15 % (3244366)Instruction limit reached!
% 5.60/1.15 % (3244366)------------------------------
% 5.60/1.15 % (3244366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244366)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244366)Termination reason: Instruction limit
% 5.60/1.15 % (3244366)Termination phase: Saturation
% 5.60/1.15 % (3244366)Time elapsed: 0.056 s
% 5.60/1.15 % (3244366)Peak memory usage: 91 MB
% 5.60/1.15 % (3244366)Instructions burned: 192 (million)
% 5.60/1.15 % (3244367)Instruction limit reached!
% 5.60/1.15 % (3244367)------------------------------
% 5.60/1.15 % (3244367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244367)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244367)Termination reason: Instruction limit
% 5.60/1.15 % (3244367)Termination phase: Saturation
% 5.60/1.15 % (3244367)Time elapsed: 0.075 s
% 5.60/1.15 % (3244367)Peak memory usage: 91 MB
% 5.60/1.15 % (3244367)Instructions burned: 221 (million)
% 5.60/1.15 % (3244368)Instruction limit reached!
% 5.60/1.15 % (3244368)------------------------------
% 5.60/1.15 % (3244368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244368)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244368)Termination reason: Instruction limit
% 5.60/1.15 % (3244368)Termination phase: Saturation
% 5.60/1.15 % (3244368)Time elapsed: 0.036 s
% 5.60/1.15 % (3244368)Peak memory usage: 90 MB
% 5.60/1.15 % (3244368)Instructions burned: 128 (million)
% 5.60/1.15 % (3244374)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1550906237:i=157:gtg=all_2997 on theBenchmark for (2997ds/157Mi)
% 5.60/1.15 % (3244373)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1176359071:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 5.60/1.15 % (3244375)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1530029188:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 5.60/1.15 % (3244376)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3442749018:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi)
% 5.60/1.15 % (3244374)Instruction limit reached!
% 5.60/1.15 % (3244374)------------------------------
% 5.60/1.15 % (3244374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244374)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244374)Termination reason: Instruction limit
% 5.60/1.15 % (3244374)Termination phase: Saturation
% 5.60/1.15 % (3244374)Time elapsed: 0.051 s
% 5.60/1.15 % (3244374)Peak memory usage: 91 MB
% 5.60/1.15 % (3244374)Instructions burned: 159 (million)
% 5.60/1.15 % (3244376)Instruction limit reached!
% 5.60/1.15 % (3244376)------------------------------
% 5.60/1.15 % (3244376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244376)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244376)Termination reason: Instruction limit
% 5.60/1.15 % (3244376)Termination phase: Saturation
% 5.60/1.15 % (3244376)Time elapsed: 0.030 s
% 5.60/1.15 % (3244376)Peak memory usage: 90 MB
% 5.60/1.15 % (3244376)Instructions burned: 109 (million)
% 5.60/1.15 % (3244373)Instruction limit reached!
% 5.60/1.15 % (3244373)------------------------------
% 5.60/1.15 % (3244373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244373)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244373)Termination reason: Instruction limit
% 5.60/1.15 % (3244373)Termination phase: Saturation
% 5.60/1.15 % (3244373)Time elapsed: 0.070 s
% 5.60/1.15 % (3244373)Peak memory usage: 90 MB
% 5.60/1.15 % (3244373)Instructions burned: 195 (million)
% 5.60/1.15 % (3244381)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4245886902:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 5.60/1.15 % (3244382)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1722958465:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2995 on theBenchmark for (2995ds/242Mi)
% 5.60/1.15 % (3244383)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=899288681:cond=fast:i=5208:av=off_2995 on theBenchmark for (2995ds/5208Mi)
% 5.60/1.15 % (3244381)Instruction limit reached!
% 5.60/1.15 % (3244381)------------------------------
% 5.60/1.15 % (3244381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244381)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244381)Termination reason: Instruction limit
% 5.60/1.15 % (3244381)Termination phase: Saturation
% 5.60/1.15 % (3244381)Time elapsed: 0.034 s
% 5.60/1.15 % (3244381)Peak memory usage: 89 MB
% 5.60/1.15 % (3244381)Instructions burned: 108 (million)
% 5.60/1.15 % (3244382)Instruction limit reached!
% 5.60/1.15 % (3244382)------------------------------
% 5.60/1.15 % (3244382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244382)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244382)Termination reason: Instruction limit
% 5.60/1.15 % (3244382)Termination phase: Saturation
% 5.60/1.15 % (3244382)Time elapsed: 0.083 s
% 5.60/1.15 % (3244382)Peak memory usage: 89 MB
% 5.60/1.15 % (3244382)Instructions burned: 244 (million)
% 5.60/1.15 % (3244387)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=365229993:i=134:sd=2:doe=on:ss=axioms:sgt=14_2994 on theBenchmark for (2994ds/134Mi)
% 5.60/1.15 % (3244351)First to succeed.
% 5.60/1.15 % (3244351)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3244346"
% 5.60/1.15 % (3244387)Instruction limit reached!
% 5.60/1.15 % (3244387)------------------------------
% 5.60/1.15 % (3244387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.15 % (3244387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.15 % (3244387)CaDiCaL version: 2.1.3
% 5.60/1.15 % (3244387)Termination reason: Instruction limit
% 5.60/1.15 % (3244387)Termination phase: Saturation
% 5.60/1.15 % (3244387)Time elapsed: 0.049 s
% 5.60/1.15 % (3244387)Peak memory usage: 90 MB
% 5.60/1.15 % (3244387)Instructions burned: 134 (million)
% 5.60/1.15 % (3244388)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=177159362:i=499:bd=all_2993 on theBenchmark for (2993ds/499Mi)
% 5.60/1.15 % (3244391)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=452423814:i=191:fgj=on:bd=all_2992 on theBenchmark for (2992ds/191Mi)
% 5.60/1.15 % (3244351)Refutation found. Thanks to Tanya!
% 5.60/1.15 % SZS status Unsatisfiable for theBenchmark
% 5.60/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 5.99/1.24 % (3244351)------------------------------
% 5.99/1.24 % (3244351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.99/1.24 % (3244351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.99/1.24 % (3244351)CaDiCaL version: 2.1.3
% 5.99/1.24 % (3244351)Termination reason: Refutation
% 5.99/1.24 % (3244351)Time elapsed: 0.561 s
% 5.99/1.24 % (3244351)Peak memory usage: 135 MB
% 5.99/1.24 % (3244351)Instructions burned: 1602 (million)
% 5.99/1.24 % (3244351)------------------------------
% 5.99/1.24 % (3244351)------------------------------
% 5.99/1.24 % (3244346)Success in time 0.83 s
% 5.99/1.24 % Vampire exiting
%------------------------------------------------------------------------------