%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC099-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 : n004.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:02:26 PM UTC 2026
% Result : Unsatisfiable 4.63s 1.61s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 41
% Syntax : Number of formulae : 161 ( 21 unt; 11 def)
% Number of atoms : 582 ( 78 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 821 ( 400 ~; 410 |; 0 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 12 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 119 ( 0 sgn 119 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f12,axiom,
! [X0] : ssItem(skaf83(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
fof(f48,axiom,
! [X0,X1] : ssList(skaf48(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f56,axiom,
! [X0] :
( ~ ssList(X0)
| segmentP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f60,axiom,
! [X0] :
( ~ ssList(X0)
| frontsegP(X0,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f64,axiom,
! [X0] :
( ~ ssItem(X0)
| equalelemsP(cons(X0,nil)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f77,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,axiom,
! [X0] :
( ~ ssList(X0)
| ssItem(hd(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f84,axiom,
! [X0] :
( ~ frontsegP(nil,X0)
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
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] :
( tl(cons(X0,X1)) = X1
| ~ ssList(X1)
| ~ ssItem(X0) ),
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(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f102,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f192,axiom,
! [X2,X3,X0,X1] :
( ~ frontsegP(X0,X1)
| X2 != X3
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X2)
| frontsegP(cons(X2,X0),cons(X3,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
frontsegP(sk4,sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
equalelemsP(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
! [X0] :
( ~ neq(sk3,X0)
| ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ segmentP(X0,sk3)
| ~ equalelemsP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f210,negated_conjecture,
( nil = sk2
| ~ neq(sk1,nil)
| ~ frontsegP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
( nil != sk1
| neq(sk2,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f212,negated_conjecture,
( nil != sk1
| ~ neq(sk1,nil)
| ~ frontsegP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_13) ).
fof(f216,plain,
( nil = sk4
| ~ neq(sk3,nil)
| ~ frontsegP(sk4,sk3) ),
inference(definition_unfolding,[],[f210,f204,f205,f204,f205]) ).
fof(f217,plain,
( nil != sk3
| neq(sk4,nil) ),
inference(definition_unfolding,[],[f211,f205,f204]) ).
fof(f218,plain,
( nil != sk3
| ~ neq(sk3,nil)
| ~ frontsegP(sk4,sk3) ),
inference(definition_unfolding,[],[f212,f205,f205,f204,f205]) ).
fof(f235,plain,
! [X3,X0,X1] :
( ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ ssItem(X3)
| frontsegP(cons(X3,X0),cons(X3,X1)) ),
inference(equality_resolution,[],[f192]) ).
fof(f236,plain,
! [X2,X3,X0,X1] :
( ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(X3) ),
inference(equality_resolution,[],[f193]) ).
fof(f243,plain,
! [X3,X0,X1] :
( frontsegP(cons(X3,X0),cons(X3,X1))
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X3)
| ~ frontsegP(X0,X1) ),
inference(duplicate_literal_removal,[],[f235]) ).
fof(f250,definition,
( spl0_1
<=> frontsegP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f251,plain,
( frontsegP(sk4,sk3)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl0_2
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f256,plain,
( ~ neq(sk3,nil)
| spl0_2 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f258,definition,
( spl0_3
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f259,plain,
( nil = sk3
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f260,plain,
( nil != sk3
| spl0_3 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f261,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f218,f258,f254,f250]) ).
fof(f263,definition,
( spl0_4
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f265,plain,
( neq(sk4,nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f266,plain,
( spl0_4
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f217,f258,f263]) ).
fof(f268,definition,
( spl0_5
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f270,plain,
( nil = sk4
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f271,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(avatar_split_clause,[],[f216,f268,f254,f250]) ).
fof(f273,plain,
spl0_1,
inference(avatar_split_clause,[],[f206,f250]) ).
fof(f279,definition,
( spl0_7
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f280,plain,
( ssList(nil)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f307,definition,
( spl0_13
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f308,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,definition,
( spl0_14
<=> ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f311,plain,
( ! [X0] :
( ~ ssList(X0)
| duplicatefreeP(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f312,plain,
( spl0_13
| spl0_14 ),
inference(avatar_split_clause,[],[f72,f310,f307]) ).
fof(f315,plain,
spl0_7,
inference(avatar_split_clause,[],[f8,f279]) ).
fof(f316,plain,
( ~ ssList(sk3)
| ~ ssList(nil)
| nil = sk3
| spl0_2 ),
inference(resolution,[],[f102,f256]) ).
fof(f317,plain,
( ~ ssList(nil)
| nil = sk3
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f316,f202]) ).
fof(f318,plain,
( nil = sk3
| spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f317,f280]) ).
fof(f319,plain,
( spl0_3
| spl0_2
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f318,f279,f254,f258]) ).
fof(f343,plain,
( ! [X0] :
( sk4 = X0
| ~ frontsegP(nil,X0)
| ~ ssList(X0) )
| ~ spl0_5 ),
inference(backward_demodulation,[],[f84,f270]) ).
fof(f362,plain,
( sk3 != sk4
| spl0_3
| ~ spl0_5 ),
inference(backward_demodulation,[],[f260,f270]) ).
fof(f385,plain,
( ! [X0] :
( ~ frontsegP(sk4,X0)
| sk4 = X0
| ~ ssList(X0) )
| ~ spl0_5 ),
inference(forward_demodulation,[],[f343,f270]) ).
fof(f399,plain,
( sk3 = sk4
| ~ ssList(sk3)
| ~ spl0_1
| ~ spl0_5 ),
inference(resolution,[],[f385,f251]) ).
fof(f400,plain,
( ~ ssList(sk3)
| ~ spl0_1
| spl0_3
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f399,f362]) ).
fof(f401,plain,
( $false
| ~ spl0_1
| spl0_3
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f400,f202]) ).
fof(f402,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[],[f401]) ).
fof(f403,plain,
( ~ neq(sk3,sk3)
| spl0_2
| ~ spl0_3 ),
inference(backward_demodulation,[],[f256,f259]) ).
fof(f412,plain,
( ! [X0] :
( segmentP(X0,sk3)
| ~ ssList(X0) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f56,f259]) ).
fof(f414,plain,
( ! [X0] :
( frontsegP(X0,sk3)
| ~ ssList(X0) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f60,f259]) ).
fof(f423,plain,
( ! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f77,f259]) ).
fof(f429,plain,
( ! [X0] :
( cons(hd(X0),tl(X0)) = X0
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f107,f259]) ).
fof(f430,plain,
( ! [X0] :
( cons(skaf83(X0),skaf82(X0)) = X0
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f112,f259]) ).
fof(f444,plain,
( neq(sk4,sk3)
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f265,f259]) ).
fof(f501,plain,
! [X0] :
( ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ segmentP(X0,sk3)
| ~ equalelemsP(X0)
| ~ ssList(sk3)
| ~ ssList(X0)
| sk3 = X0 ),
inference(resolution,[],[f208,f102]) ).
fof(f502,plain,
! [X0] :
( ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ segmentP(X0,sk3)
| ~ equalelemsP(X0)
| ~ ssList(sk3)
| sk3 = X0 ),
inference(duplicate_literal_removal,[],[f501]) ).
fof(f503,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ frontsegP(sk4,X0)
| ~ equalelemsP(X0)
| ~ ssList(sk3)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f502,f412]) ).
fof(f504,plain,
( ! [X0] :
( ~ frontsegP(sk4,X0)
| ~ ssList(X0)
| ~ equalelemsP(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f503,f202]) ).
fof(f511,definition,
( spl0_15
<=> sk3 = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f512,plain,
( sk3 != sk4
| spl0_15 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f513,plain,
( sk3 = sk4
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f628,plain,
( ! [X0,X1] :
( frontsegP(X0,cons(hd(X0),X1))
| ~ ssList(X1)
| ~ ssList(tl(X0))
| ~ ssItem(hd(X0))
| ~ frontsegP(tl(X0),X1)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f243,f429]) ).
fof(f635,plain,
( ! [X0,X1] :
( frontsegP(X0,cons(hd(X0),X1))
| ~ ssList(X1)
| ~ ssItem(hd(X0))
| ~ frontsegP(tl(X0),X1)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f628,f423]) ).
fof(f656,plain,
( ~ neq(sk4,sk4)
| spl0_2
| ~ spl0_3
| ~ spl0_15 ),
inference(backward_demodulation,[],[f403,f513]) ).
fof(f675,plain,
( neq(sk4,sk4)
| ~ spl0_3
| ~ spl0_4
| ~ spl0_15 ),
inference(backward_demodulation,[],[f444,f513]) ).
fof(f726,plain,
( $false
| spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f656,f675]) ).
fof(f727,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f726]) ).
fof(f733,plain,
( ! [X0] :
( equalelemsP(cons(X0,sk3))
| ~ ssItem(X0) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f64,f259]) ).
fof(f739,plain,
( ! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f78,f259]) ).
fof(f740,plain,
( ! [X0,X1] :
( cons(X0,X1) != sk3
| ~ ssItem(X0)
| ~ ssList(X1) )
| ~ spl0_3 ),
inference(forward_demodulation,[],[f99,f259]) ).
fof(f841,plain,
( ! [X0] :
( skaf82(X0) = tl(X0)
| ~ ssList(skaf82(X0))
| ~ ssItem(skaf83(X0))
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f96,f430]) ).
fof(f845,plain,
( ! [X0] :
( skaf82(X0) = tl(X0)
| ~ ssItem(skaf83(X0))
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f841,f13]) ).
fof(f847,plain,
( ! [X0] :
( skaf82(X0) = tl(X0)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f845,f12]) ).
fof(f1001,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(app(X1,X0),cons(skaf83(X0),X2)))
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssItem(skaf83(X0))
| ~ duplicatefreeP(app(app(X1,X0),cons(skaf83(X0),X2)))
| ~ ssList(X2)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3 ),
inference(superposition,[],[f236,f430]) ).
fof(f1022,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(app(X1,X0),cons(skaf83(X0),X2)))
| ~ ssList(skaf82(X0))
| ~ ssList(X1)
| ~ ssItem(skaf83(X0))
| ~ ssList(X2)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1001,f311]) ).
fof(f1034,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(app(X1,X0),cons(skaf83(X0),X2)))
| ~ ssList(X1)
| ~ ssItem(skaf83(X0))
| ~ ssList(X2)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1022,f13]) ).
fof(f1044,plain,
( ! [X2,X0,X1] :
( ~ ssList(app(app(X1,X0),cons(skaf83(X0),X2)))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1034,f12]) ).
fof(f1046,plain,
( ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| sk3 = X2
| ~ ssList(app(X0,X2))
| ~ ssList(cons(skaf83(X2),X1)) )
| ~ spl0_3
| ~ spl0_14 ),
inference(resolution,[],[f1044,f85]) ).
fof(f1066,plain,
( ! [X2,X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X2)
| sk3 = X2
| ~ ssList(cons(skaf83(X2),X1)) )
| ~ spl0_3
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1046,f85]) ).
fof(f1068,definition,
( spl0_18
<=> ! [X2,X1] :
( ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(cons(skaf83(X1),X2))
| sk3 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f1069,plain,
( ! [X2,X1] :
( ~ ssList(cons(skaf83(X1),X2))
| ~ ssList(X1)
| ~ ssList(X2)
| sk3 = X1 )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1071,definition,
( spl0_19
<=> ! [X0] : ~ ssList(X0) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f1072,plain,
( ! [X0] : ~ ssList(X0)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f1071]) ).
fof(f1074,plain,
( spl0_18
| spl0_19
| ~ spl0_3
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1066,f310,f258,f1071,f1068]) ).
fof(f1165,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssItem(hd(sk4))
| ~ frontsegP(tl(sk4),X0)
| ~ ssList(sk4)
| sk3 = sk4
| ~ ssList(cons(hd(sk4),X0))
| ~ equalelemsP(cons(hd(sk4),X0))
| sk3 = cons(hd(sk4),X0) )
| ~ spl0_3 ),
inference(resolution,[],[f635,f504]) ).
fof(f1184,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssItem(hd(sk4))
| ~ frontsegP(tl(sk4),X0)
| ~ ssList(sk4)
| sk3 = sk4
| ~ equalelemsP(cons(hd(sk4),X0))
| sk3 = cons(hd(sk4),X0) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1165,f86]) ).
fof(f1188,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssItem(hd(sk4))
| ~ frontsegP(tl(sk4),X0)
| ~ ssList(sk4)
| sk3 = sk4
| ~ equalelemsP(cons(hd(sk4),X0)) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1184,f740]) ).
fof(f1190,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ frontsegP(tl(sk4),X0)
| ~ ssList(sk4)
| sk3 = sk4
| ~ equalelemsP(cons(hd(sk4),X0)) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1188,f739]) ).
fof(f1191,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ frontsegP(tl(sk4),X0)
| sk3 = sk4
| ~ equalelemsP(cons(hd(sk4),X0)) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1190,f203]) ).
fof(f1192,plain,
( ! [X0] :
( ~ equalelemsP(cons(hd(sk4),X0))
| ~ frontsegP(tl(sk4),X0)
| ~ ssList(X0) )
| ~ spl0_3
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1191,f512]) ).
fof(f1215,plain,
( ~ frontsegP(tl(sk4),sk3)
| ~ ssList(sk3)
| ~ ssItem(hd(sk4))
| ~ spl0_3
| spl0_15 ),
inference(resolution,[],[f1192,f733]) ).
fof(f1220,plain,
( ~ frontsegP(tl(sk4),sk3)
| ~ ssItem(hd(sk4))
| ~ spl0_3
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1215,f202]) ).
fof(f1222,plain,
( ~ frontsegP(tl(sk4),sk3)
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1220,f308]) ).
fof(f1760,plain,
( ~ ssList(tl(sk4))
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(resolution,[],[f1222,f414]) ).
fof(f1767,plain,
( ~ ssList(skaf82(sk4))
| ~ ssList(sk4)
| sk3 = sk4
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(superposition,[],[f1760,f847]) ).
fof(f1768,plain,
( ~ ssList(sk4)
| sk3 = sk4
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1767,f13]) ).
fof(f1770,plain,
( sk3 = sk4
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1768,f203]) ).
fof(f1773,plain,
( $false
| ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(forward_subsumption_resolution,[],[f1770,f512]) ).
fof(f1774,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(avatar_contradiction_clause,[],[f1773]) ).
fof(f1809,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(X0)
| ~ ssList(skaf82(X0))
| sk3 = X0
| ~ ssList(X0)
| sk3 = X0 )
| ~ spl0_3
| ~ spl0_18 ),
inference(superposition,[],[f1069,f430]) ).
fof(f1810,plain,
( ! [X0] :
( ~ ssList(X0)
| ~ ssList(skaf82(X0))
| sk3 = X0 )
| ~ spl0_3
| ~ spl0_18 ),
inference(duplicate_literal_removal,[],[f1809]) ).
fof(f1812,plain,
( ! [X0] :
( sk3 = X0
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1810,f13]) ).
fof(f1816,plain,
( ! [X0] :
( equalelemsP(X0)
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_18 ),
inference(superposition,[],[f207,f1812]) ).
fof(f1817,plain,
( ! [X0,X1] :
( ~ neq(X0,X1)
| ~ ssList(X1)
| ~ frontsegP(sk4,X1)
| ~ segmentP(X1,X0)
| ~ equalelemsP(X1)
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_18 ),
inference(superposition,[],[f208,f1812]) ).
fof(f1818,plain,
( ! [X0] :
( frontsegP(sk4,X0)
| ~ ssList(X0) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_18 ),
inference(superposition,[],[f251,f1812]) ).
fof(f1822,plain,
( ! [X0,X1] :
( segmentP(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl0_3
| ~ spl0_18 ),
inference(superposition,[],[f412,f1812]) ).
fof(f1848,plain,
( ! [X0,X1] :
( ~ neq(X0,X1)
| ~ ssList(X1)
| ~ segmentP(X1,X0)
| ~ equalelemsP(X1)
| ~ ssList(X0) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1817,f1818]) ).
fof(f1849,plain,
( ! [X0,X1] :
( ~ neq(X0,X1)
| ~ ssList(X1)
| ~ equalelemsP(X1)
| ~ ssList(X0) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1848,f1822]) ).
fof(f1850,plain,
( ! [X0,X1] :
( ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1849,f1816]) ).
fof(f1853,plain,
( ~ ssList(sk3)
| ~ ssList(sk4)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(resolution,[],[f1850,f444]) ).
fof(f1855,plain,
( ~ ssList(sk4)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1853,f202]) ).
fof(f1856,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f1855,f203]) ).
fof(f1857,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(avatar_contradiction_clause,[],[f1856]) ).
fof(f1858,plain,
( $false
| ~ spl0_19 ),
inference(resolution,[],[f1072,f48]) ).
fof(f1876,plain,
~ spl0_19,
inference(avatar_contradiction_clause,[],[f1858]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f261]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f266]) ).
cnf(s3,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_5 ),
inference(sat_conversion,[],[f271]) ).
cnf(s5,plain,
spl0_1,
inference(sat_conversion,[],[f273]) ).
cnf(s12,plain,
( spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f312]) ).
cnf(s15,plain,
spl0_7,
inference(sat_conversion,[],[f315]) ).
cnf(s16,plain,
( spl0_2
| spl0_3
| ~ spl0_7 ),
inference(sat_conversion,[],[f319]) ).
cnf(s17,plain,
( ~ spl0_1
| spl0_3
| ~ spl0_5 ),
inference(sat_conversion,[],[f402]) ).
cnf(s20,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_15 ),
inference(sat_conversion,[],[f727]) ).
cnf(s24,plain,
( ~ spl0_3
| ~ spl0_14
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f1074]) ).
cnf(s28,plain,
( ~ spl0_3
| ~ spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s33,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_4
| ~ spl0_18 ),
inference(sat_conversion,[],[f1857]) ).
cnf(s41,plain,
~ spl0_19,
inference(sat_conversion,[],[f1876]) ).
cnf(s42,plain,
( ~ spl0_3
| ~ spl0_14
| spl0_18 ),
inference(rat,[],[s24,s41]) ).
cnf(s48,plain,
( ~ spl0_2
| spl0_5 ),
inference(rat,[],[s3,s5]) ).
cnf(s49,plain,
( ~ spl0_2
| ~ spl0_3 ),
inference(rat,[],[s1,s5]) ).
cnf(s50,plain,
spl0_2,
inference(rat,[],[s12,s28,s42,s20,s33,s2,s16,s5,s15]) ).
cnf(s51,plain,
spl0_5,
inference(rat,[],[s48,s50]) ).
cnf(s52,plain,
~ spl0_3,
inference(rat,[],[s49,s50]) ).
cnf(s53,plain,
$false,
inference(rat,[],[s17,s5,s51,s52]) ).
fof(f1877,plain,
$false,
inference(avatar_sat_refutation,[],[s53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC099-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n004.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 28 07:52:37 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 4.63/1.61 % (191540)Input is clausal, will run a generic CNF schedule.
% 4.63/1.61 % (191547)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1478280224:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.63/1.61 % (191548)lrs+10_1_sil=8000:sp=occurrence:random_seed=2182686428:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.63/1.61 % (191549)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2819908382:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.63/1.61 % (191551)dis-21_1_sil=8000:lcm=predicate:random_seed=528796092: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)
% 4.63/1.61 % (191545)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=2669449521:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.63/1.61 % (191546)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1108698726:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.63/1.61 % (191550)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3991804656:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.63/1.61 % (191551)Instruction limit reached!
% 4.63/1.61 % (191551)------------------------------
% 4.63/1.61 % (191551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191551)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191551)Termination reason: Instruction limit
% 4.63/1.61 % (191551)Termination phase: Saturation
% 4.63/1.61 % (191551)Time elapsed: 0.049 s
% 4.63/1.61 % (191551)Peak memory usage: 88 MB
% 4.63/1.61 % (191551)Instructions burned: 120 (million)
% 4.63/1.61 % (191549)Instruction limit reached!
% 4.63/1.61 % (191549)------------------------------
% 4.63/1.61 % (191549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191549)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191549)Termination reason: Instruction limit
% 4.63/1.61 % (191549)Termination phase: Saturation
% 4.63/1.61 % (191549)Time elapsed: 0.058 s
% 4.63/1.61 % (191549)Peak memory usage: 88 MB
% 4.63/1.61 % (191549)Instructions burned: 117 (million)
% 4.63/1.61 % (191548)Instruction limit reached!
% 4.63/1.61 % (191548)------------------------------
% 4.63/1.61 % (191548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191548)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191548)Termination reason: Instruction limit
% 4.63/1.61 % (191548)Termination phase: Saturation
% 4.63/1.61 % (191548)Time elapsed: 0.069 s
% 4.63/1.61 % (191548)Peak memory usage: 89 MB
% 4.63/1.61 % (191548)Instructions burned: 107 (million)
% 4.63/1.61 % (191550)Instruction limit reached!
% 4.63/1.61 % (191550)------------------------------
% 4.63/1.61 % (191550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191550)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191550)Termination reason: Instruction limit
% 4.63/1.61 % (191550)Termination phase: Saturation
% 4.63/1.61 % (191550)Time elapsed: 0.122 s
% 4.63/1.61 % (191550)Peak memory usage: 90 MB
% 4.63/1.61 % (191550)Instructions burned: 180 (million)
% 4.63/1.61 % (191560)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=402043668:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.63/1.61 % (191559)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=4243967254:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.63/1.61 % (191559)Refutation not found, incomplete strategy
% 4.63/1.61 % (191559)------------------------------
% 4.63/1.61 % (191559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191559)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191559)Termination reason: Refutation not found, incomplete strategy
% 4.63/1.61 % (191559)Time elapsed: 0.005 s
% 4.63/1.61 % (191559)Peak memory usage: 88 MB
% 4.63/1.61 % (191559)Instructions burned: 4 (million)
% 4.63/1.61 % (191561)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2999133242:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.63/1.61 % (191562)lrs+10_64_to=lpo:sil=8000:random_seed=1663622895:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.63/1.61 % (191560)Instruction limit reached!
% 4.63/1.61 % (191560)------------------------------
% 4.63/1.61 % (191560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191560)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191560)Termination reason: Instruction limit
% 4.63/1.61 % (191560)Termination phase: Saturation
% 4.63/1.61 % (191560)Time elapsed: 0.100 s
% 4.63/1.61 % (191560)Peak memory usage: 91 MB
% 4.63/1.61 % (191560)Instructions burned: 191 (million)
% 4.63/1.61 % (191561)Instruction limit reached!
% 4.63/1.61 % (191561)------------------------------
% 4.63/1.61 % (191561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191561)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191561)Termination reason: Instruction limit
% 4.63/1.61 % (191561)Termination phase: Saturation
% 4.63/1.61 % (191561)Time elapsed: 0.086 s
% 4.63/1.61 % (191561)Peak memory usage: 88 MB
% 4.63/1.61 % (191561)Instructions burned: 221 (million)
% 4.63/1.61 % (191562)Instruction limit reached!
% 4.63/1.61 % (191562)------------------------------
% 4.63/1.61 % (191562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191562)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191562)Termination reason: Instruction limit
% 4.63/1.61 % (191562)Termination phase: Saturation
% 4.63/1.61 % (191562)Time elapsed: 0.066 s
% 4.63/1.61 % (191562)Peak memory usage: 90 MB
% 4.63/1.61 % (191562)Instructions burned: 126 (million)
% 4.63/1.61 % (191547)First to succeed.
% 4.63/1.61 % (191547)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-191540"
% 4.63/1.61 % (191559)------------------------------
% 4.63/1.61 % (191559)------------------------------
% 4.63/1.61 % (191567)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=743775725:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 4.63/1.61 % (191568)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3117284601:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 4.63/1.61 % (191569)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3538447629:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 4.63/1.61 % (191568)Instruction limit reached!
% 4.63/1.61 % (191568)------------------------------
% 4.63/1.61 % (191568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191568)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191568)Termination reason: Instruction limit
% 4.63/1.61 % (191568)Termination phase: Saturation
% 4.63/1.61 % (191568)Time elapsed: 0.092 s
% 4.63/1.61 % (191568)Peak memory usage: 91 MB
% 4.63/1.61 % (191568)Instructions burned: 158 (million)
% 4.63/1.61 % (191567)Instruction limit reached!
% 4.63/1.61 % (191567)------------------------------
% 4.63/1.61 % (191567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.61 % (191567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.61 % (191567)CaDiCaL version: 2.1.3
% 4.63/1.61 % (191567)Termination reason: Instruction limit
% 4.63/1.61 % (191567)Termination phase: Saturation
% 4.63/1.61 % (191567)Time elapsed: 0.124 s
% 4.63/1.61 % (191567)Peak memory usage: 90 MB
% 4.63/1.61 % (191567)Instructions burned: 194 (million)
% 4.63/1.61 % (191547)Refutation found. Thanks to Tanya!
% 4.63/1.61 % SZS status Unsatisfiable for theBenchmark
% 4.63/1.61 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/1.81 % (191547)------------------------------
% 0.17/1.81 % (191547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/1.81 % (191547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/1.81 % (191547)CaDiCaL version: 2.1.3
% 0.17/1.81 % (191547)Termination reason: Refutation
% 0.17/1.81 % (191547)Time elapsed: 0.468 s
% 0.17/1.81 % (191547)Peak memory usage: 133 MB
% 0.17/1.81 % (191547)Instructions burned: 1238 (million)
% 0.17/1.81 % (191547)------------------------------
% 0.17/1.81 % (191547)------------------------------
% 0.17/1.81 % (191540)Success in time 0.754 s
% 0.17/1.81 % Vampire exiting
%------------------------------------------------------------------------------