%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC261-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:05:18 PM UTC 2026
% Result : Unsatisfiable 19.70s 3.13s
% Output : Refutation 19.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 29
% Syntax : Number of formulae : 126 ( 33 unt; 9 def)
% Number of atoms : 344 ( 12 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 368 ( 150 ~; 209 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 10 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 95 ( 0 sgn 95 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X0] : ssList(skaf68(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause27) ).
fof(f28,axiom,
! [X0] : ssList(skaf67(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause28) ).
fof(f29,axiom,
! [X0] : ssList(skaf66(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause29) ).
fof(f30,axiom,
! [X0] : ssItem(skaf65(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause30) ).
fof(f31,axiom,
! [X0] : ssItem(skaf64(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause31) ).
fof(f62,axiom,
! [X0] :
( leq(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause62) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f91,axiom,
! [X0] :
( ~ leq(skaf64(X0),skaf65(X0))
| ~ ssList(X0)
| totalorderedP(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause91) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause140) ).
fof(f177,axiom,
! [X0] :
( ~ ssList(X0)
| totalorderedP(X0)
| app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0))) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause164) ).
fof(f189,axiom,
! [X2,X3,X0,X1] :
( app(X0,cons(X1,X2)) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(X3)
| memberP(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001-0.ax',clause175) ).
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/sandbox/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f207,negated_conjecture,
! [X0] :
( ~ memberP(sk3,X0)
| sk5 = X0
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
~ totalorderedP(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f210,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f211,plain,
~ totalorderedP(sk3),
inference(definition_unfolding,[],[f208,f205]) ).
fof(f227,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f229,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f248,plain,
! [X0] : ~ ssList(skaf68(X0)),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f249,plain,
! [X0] : ~ ssList(skaf67(X0)),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f250,plain,
! [X0] : ~ ssList(skaf66(X0)),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f275,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f288,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f289,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ~ ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f294,plain,
! [X0] :
( ~ leq(skaf64(X0),skaf65(X0))
| ssList(X0)
| totalorderedP(X0) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f342,plain,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f365,plain,
! [X0] :
( totalorderedP(X0)
| ssList(X0)
| app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0))) = X0 ),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f376,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ~ ssItem(X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f380,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f387,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f388,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f210]) ).
fof(f430,definition,
( spl0_8
<=> ! [X1] : ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f431,plain,
( ! [X1] : ssItem(X1)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f433,definition,
( spl0_9
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f434,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f275,f433,f430]) ).
fof(f2149,plain,
( ssList(sk3)
| sk3 = app(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))),cons(skaf65(sk3),skaf68(sk3))) ),
inference(resolution,[],[f365,f211]) ).
fof(f2156,plain,
sk3 = app(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))),cons(skaf65(sk3),skaf68(sk3))),
inference(forward_subsumption_resolution,[],[f2149,f387]) ).
fof(f2293,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ~ ssItem(X1)
| ssList(X3) )
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f380,f434]) ).
fof(f2321,definition,
( spl0_30
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f2322,plain,
( ! [X3] : ssList(X3)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f2321]) ).
fof(f2324,definition,
( spl0_31
<=> ! [X2,X0,X1] :
( ssList(X0)
| ssList(X1)
| ssList(app(X1,cons(X2,X0)))
| ~ ssItem(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f2325,plain,
( ! [X2,X0,X1] :
( ssList(app(X1,cons(X2,X0)))
| ssList(X1)
| ssList(X0)
| ~ ssItem(X2) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f2324]) ).
fof(f2419,plain,
( ! [X0] : leq(X0,X0)
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f62,f431]) ).
fof(f2427,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| sk5 = X0 )
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f207,f431]) ).
fof(f2453,plain,
( ! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ssList(X2)
| ssList(X0)
| memberP(app(X0,X2),X1) )
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f342,f431]) ).
fof(f2468,plain,
( ! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_8 ),
inference(backward_subsumption_resolution,[],[f376,f431]) ).
fof(f3108,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(app(X0,cons(X1,X2)))
| memberP(app(app(X0,cons(X1,X2)),X3),X1) )
| ~ spl0_8 ),
inference(resolution,[],[f2468,f2453]) ).
fof(f3115,plain,
( ! [X2,X3,X0,X1] :
( memberP(app(app(X0,cons(X1,X2)),X3),X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2)
| ssList(X3)
| ssList(X0) )
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f3108]) ).
fof(f4280,definition,
( spl0_38
<=> ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3)))) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f4282,plain,
( ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f4280]) ).
fof(f4284,definition,
( spl0_39
<=> ssList(cons(skaf65(sk3),skaf68(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f4285,plain,
( ~ ssList(cons(skaf65(sk3),skaf68(sk3)))
| spl0_39 ),
inference(avatar_component_clause,[],[f4284]) ).
fof(f4286,plain,
( ssList(cons(skaf65(sk3),skaf68(sk3)))
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f4284]) ).
fof(f4344,definition,
( spl0_51
<=> ssList(cons(skaf64(sk3),skaf67(sk3))) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f4345,plain,
( ~ ssList(cons(skaf64(sk3),skaf67(sk3)))
| spl0_51 ),
inference(avatar_component_clause,[],[f4344]) ).
fof(f4346,plain,
( ssList(cons(skaf64(sk3),skaf67(sk3)))
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f4344]) ).
fof(f4354,definition,
( spl0_53
<=> memberP(sk3,skaf65(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f4356,plain,
( memberP(sk3,skaf65(sk3))
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f4354]) ).
fof(f4441,plain,
( ssList(skaf68(sk3))
| ~ ssItem(skaf65(sk3))
| ~ spl0_39 ),
inference(resolution,[],[f289,f4286]) ).
fof(f4477,plain,
( ~ ssItem(skaf65(sk3))
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f4441,f248]) ).
fof(f4478,plain,
( $false
| ~ spl0_39 ),
inference(forward_subsumption_resolution,[],[f4477,f30]) ).
fof(f4479,plain,
~ spl0_39,
inference(avatar_contradiction_clause,[],[f4478]) ).
fof(f4681,plain,
( ssList(skaf67(sk3))
| ~ ssItem(skaf64(sk3))
| ~ spl0_51 ),
inference(resolution,[],[f4346,f289]) ).
fof(f4682,plain,
( ~ ssItem(skaf64(sk3))
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f4681,f249]) ).
fof(f4683,plain,
( $false
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f4682,f31]) ).
fof(f4684,plain,
~ spl0_51,
inference(avatar_contradiction_clause,[],[f4683]) ).
fof(f5575,plain,
( memberP(sk3,skaf65(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ~ ssItem(skaf65(sk3))
| ssList(sk3)
| ssList(skaf68(sk3)) ),
inference(superposition,[],[f376,f2156]) ).
fof(f5580,plain,
( memberP(sk3,skaf65(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(sk3)
| ssList(skaf68(sk3)) ),
inference(forward_subsumption_resolution,[],[f5575,f30]) ).
fof(f5584,plain,
( memberP(sk3,skaf65(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(skaf68(sk3)) ),
inference(forward_subsumption_resolution,[],[f5580,f387]) ).
fof(f5588,plain,
( memberP(sk3,skaf65(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3)))) ),
inference(forward_subsumption_resolution,[],[f5584,f248]) ).
fof(f5591,plain,
( spl0_38
| spl0_53 ),
inference(avatar_split_clause,[],[f5588,f4354,f4280]) ).
fof(f6678,plain,
( $false
| ~ spl0_30 ),
inference(backward_subsumption_resolution,[],[f388,f2322]) ).
fof(f6714,plain,
~ spl0_30,
inference(avatar_contradiction_clause,[],[f6678]) ).
fof(f8710,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0)))
| ssList(cons(X2,X3)) )
| ~ spl0_9 ),
inference(resolution,[],[f2293,f288]) ).
fof(f8737,plain,
( ! [X2,X3,X0,X1] :
( ssList(X0)
| ssList(X1)
| ~ ssItem(X2)
| ssList(X3)
| ssList(app(X1,cons(X2,X0))) )
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f8710,f289]) ).
fof(f8751,plain,
( spl0_30
| spl0_31
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f8737,f433,f2324,f2321]) ).
fof(f14977,plain,
( ssList(sk3)
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(skaf68(sk3))
| ~ ssItem(skaf65(sk3))
| ~ spl0_31 ),
inference(superposition,[],[f2325,f2156]) ).
fof(f14979,plain,
( ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(skaf68(sk3))
| ~ ssItem(skaf65(sk3))
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f14977,f387]) ).
fof(f14987,plain,
( ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ~ ssItem(skaf65(sk3))
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f14979,f248]) ).
fof(f14998,plain,
( ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f14987,f30]) ).
fof(f14999,plain,
( spl0_38
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f14998,f2324,f4280]) ).
fof(f45685,plain,
( memberP(sk3,skaf64(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(skaf67(sk3))
| ssList(cons(skaf65(sk3),skaf68(sk3)))
| ssList(skaf66(sk3))
| ~ spl0_8 ),
inference(superposition,[],[f3115,f2156]) ).
fof(f45687,plain,
( memberP(sk3,skaf64(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(cons(skaf65(sk3),skaf68(sk3)))
| ssList(skaf66(sk3))
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f45685,f249]) ).
fof(f45729,plain,
( memberP(sk3,skaf64(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ssList(skaf66(sk3))
| ~ spl0_8
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f45687,f4285]) ).
fof(f45735,plain,
( memberP(sk3,skaf64(sk3))
| ssList(app(skaf66(sk3),cons(skaf64(sk3),skaf67(sk3))))
| ~ spl0_8
| spl0_39 ),
inference(forward_subsumption_resolution,[],[f45729,f250]) ).
fof(f45741,definition,
( spl0_367
<=> memberP(sk3,skaf64(sk3)) ),
introduced(definition,[new_symbols(definition,[spl0_367])],[avatar_definition]) ).
fof(f45743,plain,
( memberP(sk3,skaf64(sk3))
| ~ spl0_367 ),
inference(avatar_component_clause,[],[f45741]) ).
fof(f45744,plain,
( spl0_38
| spl0_367
| ~ spl0_8
| spl0_39 ),
inference(avatar_split_clause,[],[f45735,f4284,f430,f45741,f4280]) ).
fof(f61315,plain,
( ssList(skaf66(sk3))
| ssList(cons(skaf64(sk3),skaf67(sk3)))
| ~ spl0_38 ),
inference(resolution,[],[f4282,f288]) ).
fof(f61316,plain,
( ssList(cons(skaf64(sk3),skaf67(sk3)))
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f61315,f250]) ).
fof(f61317,plain,
( $false
| ~ spl0_38
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f61316,f4345]) ).
fof(f61318,plain,
( ~ spl0_38
| spl0_51 ),
inference(avatar_contradiction_clause,[],[f61317]) ).
fof(f61325,plain,
( sk5 = skaf65(sk3)
| ~ spl0_8
| ~ spl0_53 ),
inference(resolution,[],[f4356,f2427]) ).
fof(f61341,plain,
( sk5 = skaf64(sk3)
| ~ spl0_8
| ~ spl0_367 ),
inference(resolution,[],[f45743,f2427]) ).
fof(f61543,plain,
( ~ leq(sk5,skaf65(sk3))
| ssList(sk3)
| totalorderedP(sk3)
| ~ spl0_8
| ~ spl0_367 ),
inference(superposition,[],[f294,f61341]) ).
fof(f61545,plain,
( ~ leq(sk5,skaf65(sk3))
| totalorderedP(sk3)
| ~ spl0_8
| ~ spl0_367 ),
inference(forward_subsumption_resolution,[],[f61543,f387]) ).
fof(f61547,plain,
( ~ leq(sk5,skaf65(sk3))
| ~ spl0_8
| ~ spl0_367 ),
inference(forward_subsumption_resolution,[],[f61545,f211]) ).
fof(f61548,plain,
( ~ leq(sk5,sk5)
| ~ spl0_8
| ~ spl0_53
| ~ spl0_367 ),
inference(forward_demodulation,[],[f61547,f61325]) ).
fof(f61549,plain,
( $false
| ~ spl0_8
| ~ spl0_53
| ~ spl0_367 ),
inference(forward_subsumption_resolution,[],[f61548,f2419]) ).
fof(f61550,plain,
( ~ spl0_8
| ~ spl0_53
| ~ spl0_367 ),
inference(avatar_contradiction_clause,[],[f61549]) ).
cnf(s7,plain,
( spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f435]) ).
cnf(s66,plain,
~ spl0_39,
inference(sat_conversion,[],[f4479]) ).
cnf(s75,plain,
~ spl0_51,
inference(sat_conversion,[],[f4684]) ).
cnf(s136,plain,
( spl0_38
| spl0_53 ),
inference(sat_conversion,[],[f5591]) ).
cnf(s188,plain,
~ spl0_30,
inference(sat_conversion,[],[f6714]) ).
cnf(s355,plain,
( ~ spl0_9
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f8751]) ).
cnf(s540,plain,
( ~ spl0_31
| spl0_38 ),
inference(sat_conversion,[],[f14999]) ).
cnf(s773,plain,
( ~ spl0_8
| spl0_38
| spl0_39
| spl0_367 ),
inference(sat_conversion,[],[f45744]) ).
cnf(s1934,plain,
( ~ spl0_38
| spl0_51 ),
inference(sat_conversion,[],[f61318]) ).
cnf(s1945,plain,
( ~ spl0_8
| ~ spl0_53
| ~ spl0_367 ),
inference(sat_conversion,[],[f61550]) ).
cnf(s1989,plain,
~ spl0_38,
inference(rat,[],[s1934,s75]) ).
cnf(s1990,plain,
~ spl0_31,
inference(rat,[],[s540,s1989]) ).
cnf(s1993,plain,
spl0_53,
inference(rat,[],[s136,s1989]) ).
cnf(s1994,plain,
~ spl0_9,
inference(rat,[],[s355,s188,s1990]) ).
cnf(s2342,plain,
spl0_8,
inference(rat,[],[s7,s1994]) ).
cnf(s2343,plain,
~ spl0_367,
inference(rat,[],[s1945,s1993,s2342]) ).
cnf(s2391,plain,
$false,
inference(rat,[],[s773,s66,s1989,s2343,s2342]) ).
fof(f61551,plain,
$false,
inference(avatar_sat_refutation,[],[s2391]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC261-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n013.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 08:44:51 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.26 Running first-order model finding
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.70/3.13 % (1031759)Will run a generic schedule for satisfiability detection.
% 19.70/3.13 % (1031769)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3033344608:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.70/3.13 % (1031764)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2136339346_2999 on theBenchmark for (2999ds/0Mi)
% 19.70/3.13 % (1031765)% WARNING: option uhcvi not known.
% 19.70/3.13 % (1031766)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3695970007:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.70/3.13 % (1031765)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3729628553:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.70/3.13 % (1031767)dis+10_1_sil=32000:sp=arity:random_seed=136534998:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.70/3.13 % (1031768)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=876338360:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.70/3.13 % TRYING [1]
% 19.70/3.13 % (1031770)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=34683196:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.70/3.13 % TRYING [2]
% 19.70/3.13 % TRYING [3]
% 19.70/3.13 % TRYING [4]
% 19.70/3.13 % (1031769)Instruction limit reached!
% 19.70/3.13 % (1031769)------------------------------
% 19.70/3.13 % (1031769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031769)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031769)Termination reason: Instruction limit
% 19.70/3.13 % (1031769)Termination phase: Saturation
% 19.70/3.13 % (1031769)Time elapsed: 0.063 s
% 19.70/3.13 % (1031769)Peak memory usage: 14 MB
% 19.70/3.13 % (1031769)Instructions burned: 132 (million)
% 19.70/3.13 % (1031778)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1314455557:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 19.70/3.13 % TRYING [1]
% 19.70/3.13 % TRYING [2]
% 19.70/3.13 % TRYING [3]
% 19.70/3.13 % (1031767)Instruction limit reached!
% 19.70/3.13 % (1031767)------------------------------
% 19.70/3.13 % (1031767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031767)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031767)Termination reason: Instruction limit
% 19.70/3.13 % (1031767)Termination phase: Saturation
% 19.70/3.13 % (1031767)Time elapsed: 0.101 s
% 19.70/3.13 % (1031767)Peak memory usage: 13 MB
% 19.70/3.13 % (1031767)Instructions burned: 104 (million)
% 19.70/3.13 % (1031768)Instruction limit reached!
% 19.70/3.13 % (1031768)------------------------------
% 19.70/3.13 % (1031768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031768)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031768)Termination reason: Instruction limit
% 19.70/3.13 % (1031768)Termination phase: Saturation
% 19.70/3.13 % (1031768)Time elapsed: 0.103 s
% 19.70/3.13 % (1031768)Peak memory usage: 13 MB
% 19.70/3.13 % (1031768)Instructions burned: 116 (million)
% 19.70/3.13 % TRYING [4]
% 19.70/3.13 % TRYING [5]
% 19.70/3.13 % (1031780)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3481141291:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 19.70/3.13 % (1031781)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=3718644501:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 19.70/3.13 % (1031770)Instruction limit reached!
% 19.70/3.13 % (1031770)------------------------------
% 19.70/3.13 % (1031770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031770)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031770)Termination reason: Instruction limit
% 19.70/3.13 % (1031770)Termination phase: Saturation
% 19.70/3.13 % (1031770)Time elapsed: 0.161 s
% 19.70/3.13 % (1031770)Peak memory usage: 14 MB
% 19.70/3.13 % (1031770)Instructions burned: 159 (million)
% 19.70/3.13 % TRYING [5]
% 19.70/3.13 % (1031785)ott-21_1_sil=16000:fs=off:random_seed=2297454697:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 19.70/3.13 % (1031780)Instruction limit reached!
% 19.70/3.13 % (1031780)------------------------------
% 19.70/3.13 % (1031780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031780)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031780)Termination reason: Instruction limit
% 19.70/3.13 % (1031780)Termination phase: Saturation
% 19.70/3.13 % (1031780)Time elapsed: 0.109 s
% 19.70/3.13 % (1031780)Peak memory usage: 13 MB
% 19.70/3.13 % (1031780)Instructions burned: 131 (million)
% 19.70/3.13 % (1031787)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1242284418:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 19.70/3.13 % TRYING [6]
% 19.70/3.13 % (1031778)Instruction limit reached!
% 19.70/3.13 % (1031778)------------------------------
% 19.70/3.13 % (1031778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031778)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031778)Termination reason: Instruction limit
% 19.70/3.13 % (1031778)Termination phase: Finite model building constraint generation
% 19.70/3.13 % (1031778)Time elapsed: 0.283 s
% 19.70/3.13 % (1031778)Peak memory usage: 36 MB
% 19.70/3.13 % (1031778)Instructions burned: 714 (million)
% 19.70/3.13 % (1031785)Instruction limit reached!
% 19.70/3.13 % (1031785)------------------------------
% 19.70/3.13 % (1031785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031785)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031785)Termination reason: Instruction limit
% 19.70/3.13 % (1031785)Termination phase: Saturation
% 19.70/3.13 % (1031785)Time elapsed: 0.166 s
% 19.70/3.13 % (1031785)Peak memory usage: 13 MB
% 19.70/3.13 % (1031785)Instructions burned: 180 (million)
% 19.70/3.13 % (1031789)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2840886476:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 19.70/3.13 % TRYING [1]
% 19.70/3.13 % TRYING [2]
% 19.70/3.13 % TRYING [6]
% 19.70/3.13 % TRYING [3]
% 19.70/3.13 % (1031790)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3101658978:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 19.70/3.13 % TRYING [4]
% 19.70/3.13 % TRYING [5]
% 19.70/3.13 % (1031789)Instruction limit reached!
% 19.70/3.13 % (1031789)------------------------------
% 19.70/3.13 % (1031789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031789)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031789)Termination reason: Instruction limit
% 19.70/3.13 % (1031789)Termination phase: Finite model building SAT solving
% 19.70/3.13 % (1031789)Time elapsed: 0.313 s
% 19.70/3.13 % (1031789)Peak memory usage: 22 MB
% 19.70/3.13 % (1031789)Instructions burned: 866 (million)
% 19.70/3.13 % (1031794)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3434014983:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 19.70/3.13 % (1031787)Instruction limit reached!
% 19.70/3.13 % (1031787)------------------------------
% 19.70/3.13 % (1031787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031787)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031787)Termination reason: Instruction limit
% 19.70/3.13 % (1031787)Termination phase: Saturation
% 19.70/3.13 % (1031787)Time elapsed: 0.495 s
% 19.70/3.13 % (1031787)Peak memory usage: 14 MB
% 19.70/3.13 % (1031787)Instructions burned: 477 (million)
% 19.70/3.13 % (1031796)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=662196932:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 19.70/3.13 % (1031781)Instruction limit reached!
% 19.70/3.13 % (1031781)------------------------------
% 19.70/3.13 % (1031781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031781)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031781)Termination reason: Instruction limit
% 19.70/3.13 % (1031781)Termination phase: Saturation
% 19.70/3.13 % (1031781)Time elapsed: 0.709 s
% 19.70/3.13 % (1031781)Peak memory usage: 20 MB
% 19.70/3.13 % (1031781)Instructions burned: 684 (million)
% 19.70/3.13 % TRYING [14]
% 19.70/3.13 % (1031798)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2822936145:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 19.70/3.13 % TRYING [7]
% 19.70/3.13 % (1031794)Instruction limit reached!
% 19.70/3.13 % (1031794)------------------------------
% 19.70/3.13 % (1031794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031794)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031794)Termination reason: Instruction limit
% 19.70/3.13 % (1031794)Termination phase: Finite model building constraint generation
% 19.70/3.13 % (1031794)Time elapsed: 0.359 s
% 19.70/3.13 % (1031794)Peak memory usage: 73 MB
% 19.70/3.13 % (1031794)Instructions burned: 892 (million)
% 19.70/3.13 % (1031800)fmb+10_1_sil=64000:random_seed=4173264612:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 19.70/3.13 % TRYING [1]
% 19.70/3.13 % TRYING [2]
% 19.70/3.13 % TRYING [3]
% 19.70/3.13 % TRYING [4]
% 19.70/3.13 % TRYING [5]
% 19.70/3.13 % (1031796)Instruction limit reached!
% 19.70/3.13 % (1031796)------------------------------
% 19.70/3.13 % (1031796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031796)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031796)Termination reason: Instruction limit
% 19.70/3.13 % (1031796)Termination phase: Saturation
% 19.70/3.13 % (1031796)Time elapsed: 0.638 s
% 19.70/3.13 % (1031796)Peak memory usage: 20 MB
% 19.70/3.13 % (1031796)Instructions burned: 692 (million)
% 19.70/3.13 % (1031803)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=752269259:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 19.70/3.13 % TRYING [20]
% 19.70/3.13 % (1031790)Instruction limit reached!
% 19.70/3.13 % (1031790)------------------------------
% 19.70/3.13 % (1031790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031790)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031790)Termination reason: Instruction limit
% 19.70/3.13 % (1031790)Termination phase: Saturation
% 19.70/3.13 % (1031790)Time elapsed: 1.108 s
% 19.70/3.13 % (1031790)Peak memory usage: 28 MB
% 19.70/3.13 % (1031790)Instructions burned: 1179 (million)
% 19.70/3.13 % (1031805)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2766297313:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 19.70/3.13 % TRYING [8]
% 19.70/3.13 % (1031798)Instruction limit reached!
% 19.70/3.13 % (1031798)------------------------------
% 19.70/3.13 % (1031798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031798)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031798)Termination reason: Instruction limit
% 19.70/3.13 % (1031798)Termination phase: Saturation
% 19.70/3.13 % (1031798)Time elapsed: 0.788 s
% 19.70/3.13 % (1031798)Peak memory usage: 20 MB
% 19.70/3.13 % (1031798)Instructions burned: 880 (million)
% 19.70/3.13 % (1031808)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3898395557:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 19.70/3.13 % TRYING [6]
% 19.70/3.13 % (1031805)Instruction limit reached!
% 19.70/3.13 % (1031805)------------------------------
% 19.70/3.13 % (1031805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031805)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031805)Termination reason: Instruction limit
% 19.70/3.13 % (1031805)Termination phase: Finite model building constraint generation
% 19.70/3.13 % (1031805)Time elapsed: 0.671 s
% 19.70/3.13 % (1031805)Peak memory usage: 79 MB
% 19.70/3.13 % (1031805)Instructions burned: 920 (million)
% 19.70/3.13 % (1031810)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1693504640:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 19.70/3.13 % TRYING [8]
% 19.70/3.13 % TRYING [7]
% 19.70/3.13 % (1031765) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1031759-1031765"...
% 19.70/3.13 % (1031765)...printing done.
% 19.70/3.13 % (1031765)Refutation found. Thanks to Tanya!
% 19.70/3.13 % SZS status Unsatisfiable for theBenchmark
% 19.70/3.13 % SZS output start Proof for theBenchmark
% See solution above
% 19.70/3.13 % (1031765)------------------------------
% 19.70/3.13 % (1031765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.70/3.13 % (1031765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.70/3.13 % (1031765)CaDiCaL version: 2.1.3
% 19.70/3.13 % (1031765)Termination reason: Refutation
% 19.70/3.13 % (1031765)Time elapsed: 2.766 s
% 19.70/3.13 % (1031765)Peak memory usage: 39 MB
% 19.70/3.13 % (1031765)Instructions burned: 3055 (million)
% 19.70/3.13 % (1031759)Success in time 2.853 s
% 19.70/3.13 % Vampire exiting
%------------------------------------------------------------------------------