%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC246+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:14 PM UTC 2026
% Result : Theorem 99.41s 29.83s
% Output : Refutation 99.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 16
% Syntax : Number of formulae : 121 ( 18 unt; 5 def)
% Number of atoms : 470 ( 112 equ)
% Maximal formula atoms : 32 ( 3 avg)
% Number of connectives : 592 ( 243 ~; 251 |; 70 &)
% ( 5 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 6 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 130 ( 0 sgn 99 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> ssList(cons(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax16) ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax17) ).
fof(f20,axiom,
! [X0] :
( ssList(X0)
=> ( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax20) ).
fof(f22,axiom,
! [X0] :
( ssList(X0)
=> ( nil != X0
=> ssItem(hd(X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax22) ).
fof(f23,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> hd(cons(X1,X0)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax23) ).
fof(f24,axiom,
! [X0] :
( ssList(X0)
=> ( nil != X0
=> ssList(tl(X0)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax24) ).
fof(f25,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> tl(cons(X1,X0)) = X0 ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax25) ).
fof(f28,axiom,
! [X0] :
( ssList(X0)
=> app(nil,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax28) ).
fof(f38,axiom,
! [X0] :
( ssItem(X0)
=> ~ memberP(nil,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax38) ).
fof(f81,axiom,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssItem(X1)
=> cons(X1,X0) = app(cons(X1,nil),X0) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax',ax81) ).
fof(f96,conjecture,
! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ~ ssList(X3)
| X1 != X3
| X0 != X2
| nil = X0
| ? [X4] :
( ssItem(X4)
& ? [X5] :
( ssList(X5)
& ? [X6] :
( ssList(X6)
& app(app(X5,cons(X4,nil)),X6) = X0
& ! [X7] :
( ~ ssItem(X7)
| ~ memberP(X5,X7)
| ~ memberP(X6,X7)
| ~ lt(X4,X7)
| leq(X4,X7) ) ) ) )
| ! [X8] :
( ssList(X8)
=> ! [X9] :
( ~ ssList(X9)
| app(app(X8,X2),X9) != X3
| ~ equalelemsP(X2)
| ? [X10] :
( ssItem(X10)
& ? [X11] :
( ssList(X11)
& app(X11,cons(X10,nil)) = X8
& ? [X12] :
( ssList(X12)
& app(cons(X10,nil),X12) = X2 ) ) )
| ? [X13] :
( ssItem(X13)
& ? [X14] :
( ssList(X14)
& app(cons(X13,nil),X14) = X9
& ? [X15] :
( ssList(X15)
& app(X15,cons(X13,nil)) = X2 ) ) ) ) )
| ( nil != X3
& nil = X2 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f97,negated_conjecture,
~ ! [X0] :
( ssList(X0)
=> ! [X1] :
( ssList(X1)
=> ! [X2] :
( ssList(X2)
=> ! [X3] :
( ~ ssList(X3)
| X1 != X3
| X0 != X2
| nil = X0
| ? [X4] :
( ssItem(X4)
& ? [X5] :
( ssList(X5)
& ? [X6] :
( ssList(X6)
& app(app(X5,cons(X4,nil)),X6) = X0
& ! [X7] :
( ~ ssItem(X7)
| ~ memberP(X5,X7)
| ~ memberP(X6,X7)
| ~ lt(X4,X7)
| leq(X4,X7) ) ) ) )
| ! [X8] :
( ssList(X8)
=> ! [X9] :
( ~ ssList(X9)
| app(app(X8,X2),X9) != X3
| ~ equalelemsP(X2)
| ? [X10] :
( ssItem(X10)
& ? [X11] :
( ssList(X11)
& app(X11,cons(X10,nil)) = X8
& ? [X12] :
( ssList(X12)
& app(cons(X10,nil),X12) = X2 ) ) )
| ? [X13] :
( ssItem(X13)
& ? [X14] :
( ssList(X14)
& app(cons(X13,nil),X14) = X9
& ? [X15] :
( ssList(X15)
& app(X15,cons(X13,nil)) = X2 ) ) ) ) )
| ( nil != X3
& nil = X2 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f119,plain,
! [X0] :
( ! [X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f123,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f124,plain,
! [X0] :
( nil = X0
| ? [X1] :
( ssList(X1)
& ? [X2] :
( ssItem(X2)
& cons(X2,X1) = X0 ) )
| ~ ssList(X0) ),
inference(flattening,[],[f123]) ).
fof(f126,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f127,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(flattening,[],[f126]) ).
fof(f128,plain,
! [X0] :
( ! [X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f129,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f24]) ).
fof(f130,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(flattening,[],[f129]) ).
fof(f131,plain,
! [X0] :
( ! [X1] :
( tl(cons(X1,X0)) = X0
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f134,plain,
! [X0] :
( app(nil,X0) = X0
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f148,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(ennf_transformation,[],[f38]) ).
fof(f198,plain,
! [X0] :
( ! [X1] :
( cons(X1,X0) = app(cons(X1,nil),X0)
| ~ ssItem(X1) )
| ~ ssList(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f221,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ? [X3] :
( ssList(X3)
& X1 = X3
& X0 = X2
& nil != X0
& ! [X4] :
( ~ ssItem(X4)
| ! [X5] :
( ~ ssList(X5)
| ! [X6] :
( ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != X0
| ? [X7] :
( ssItem(X7)
& memberP(X5,X7)
& memberP(X6,X7)
& lt(X4,X7)
& ~ leq(X4,X7) ) ) ) )
& ? [X8] :
( ? [X9] :
( ssList(X9)
& app(app(X8,X2),X9) = X3
& equalelemsP(X2)
& ! [X10] :
( ~ ssItem(X10)
| ! [X11] :
( ~ ssList(X11)
| app(X11,cons(X10,nil)) != X8
| ! [X12] :
( ~ ssList(X12)
| app(cons(X10,nil),X12) != X2 ) ) )
& ! [X13] :
( ~ ssItem(X13)
| ! [X14] :
( ~ ssList(X14)
| app(cons(X13,nil),X14) != X9
| ! [X15] :
( ~ ssList(X15)
| app(X15,cons(X13,nil)) != X2 ) ) ) )
& ssList(X8) )
& ( nil = X3
| nil != X2 ) )
& ssList(X2) )
& ssList(X1) )
& ssList(X0) ),
inference(ennf_transformation,[],[f97]) ).
fof(f273,plain,
! [X0] :
( nil = X0
| ( ssList(sK49(X0))
& ssItem(sK50(X0))
& cons(sK50(X0),sK49(X0)) = X0 )
| ~ ssList(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49,sK50]),skolemize(X1,sK49(X0)),skolemize(X2,sK50(X0))],[f124]) ).
fof(f295,plain,
( ssList(sK56)
& sK54 = sK56
& sK53 = sK55
& nil != sK53
& ! [X4] :
( ~ ssItem(X4)
| ! [X5] :
( ~ ssList(X5)
| ! [X6] :
( ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != sK53
| ( ssItem(sK57(X4,X5,X6))
& memberP(X5,sK57(X4,X5,X6))
& memberP(X6,sK57(X4,X5,X6))
& lt(X4,sK57(X4,X5,X6))
& ~ leq(X4,sK57(X4,X5,X6)) ) ) ) )
& ssList(sK59)
& sK56 = app(app(sK58,sK55),sK59)
& equalelemsP(sK55)
& ! [X10] :
( ~ ssItem(X10)
| ! [X11] :
( ~ ssList(X11)
| app(X11,cons(X10,nil)) != sK58
| ! [X12] :
( ~ ssList(X12)
| app(cons(X10,nil),X12) != sK55 ) ) )
& ! [X13] :
( ~ ssItem(X13)
| ! [X14] :
( ~ ssList(X14)
| app(cons(X13,nil),X14) != sK59
| ! [X15] :
( ~ ssList(X15)
| app(X15,cons(X13,nil)) != sK55 ) ) )
& ssList(sK58)
& ( nil = sK56
| nil != sK55 )
& ssList(sK55)
& ssList(sK54)
& ssList(sK53) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53,sK54,sK55,sK56,sK57,sK58,sK59]),skolemize(X0,sK53),skolemize(X1,sK54),skolemize(X2,sK55),skolemize(X3,sK56),skolemize(X7,sK57(X4,X5,X6)),skolemize(X8,sK58),skolemize(X9,sK59)],[f221]) ).
fof(f387,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f388,plain,
ssList(nil),
inference(cnf_transformation,[],[f17]) ).
fof(f392,plain,
! [X0] :
( ~ ssList(X0)
| cons(sK50(X0),sK49(X0)) = X0
| nil = X0 ),
inference(cnf_transformation,[],[f273]) ).
fof(f393,plain,
! [X0] :
( ssItem(sK50(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f394,plain,
! [X0] :
( ssList(sK49(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f396,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f397,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| hd(cons(X1,X0)) = X1 ),
inference(cnf_transformation,[],[f128]) ).
fof(f398,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[],[f130]) ).
fof(f399,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| tl(cons(X1,X0)) = X0 ),
inference(cnf_transformation,[],[f131]) ).
fof(f402,plain,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
inference(cnf_transformation,[],[f134]) ).
fof(f418,plain,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f476,plain,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssItem(X1)
| cons(X1,X0) = app(cons(X1,nil),X0) ),
inference(cnf_transformation,[],[f198]) ).
fof(f497,plain,
ssList(sK55),
inference(cnf_transformation,[],[f295]) ).
fof(f508,plain,
! [X6,X4,X5] :
( ~ ssItem(X4)
| ~ ssList(X5)
| ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != sK53
| memberP(X5,sK57(X4,X5,X6)) ),
inference(cnf_transformation,[],[f295]) ).
fof(f509,plain,
! [X6,X4,X5] :
( ~ ssItem(X4)
| ~ ssList(X5)
| ~ ssList(X6)
| app(app(X5,cons(X4,nil)),X6) != sK53
| ssItem(sK57(X4,X5,X6)) ),
inference(cnf_transformation,[],[f295]) ).
fof(f510,plain,
nil != sK53,
inference(cnf_transformation,[],[f295]) ).
fof(f511,plain,
sK53 = sK55,
inference(cnf_transformation,[],[f295]) ).
fof(f514,plain,
nil != sK55,
inference(definition_unfolding,[],[f510,f511]) ).
fof(f515,plain,
! [X6,X4,X5] :
( app(app(X5,cons(X4,nil)),X6) != sK55
| ~ ssList(X5)
| ~ ssList(X6)
| ~ ssItem(X4)
| ssItem(sK57(X4,X5,X6)) ),
inference(definition_unfolding,[],[f509,f511]) ).
fof(f516,plain,
! [X6,X4,X5] :
( app(app(X5,cons(X4,nil)),X6) != sK55
| ~ ssList(X5)
| ~ ssList(X6)
| ~ ssItem(X4)
| memberP(X5,sK57(X4,X5,X6)) ),
inference(definition_unfolding,[],[f508,f511]) ).
fof(f10807,definition,
( spl60_284
<=> ssList(cons(hd(sK55),nil)) ),
introduced(definition,[new_symbols(definition,[spl60_284])],[avatar_definition]) ).
fof(f10808,plain,
( ssList(cons(hd(sK55),nil))
| ~ spl60_284 ),
inference(avatar_component_clause,[],[f10807]) ).
fof(f10809,plain,
( ~ ssList(cons(hd(sK55),nil))
| spl60_284 ),
inference(avatar_component_clause,[],[f10807]) ).
fof(f10811,definition,
( spl60_285
<=> ssItem(hd(sK55)) ),
introduced(definition,[new_symbols(definition,[spl60_285])],[avatar_definition]) ).
fof(f10812,plain,
( ~ ssItem(hd(sK55))
| spl60_285 ),
inference(avatar_component_clause,[],[f10811]) ).
fof(f10813,plain,
( ssItem(hd(sK55))
| ~ spl60_285 ),
inference(avatar_component_clause,[],[f10811]) ).
fof(f10815,plain,
( ~ ssItem(hd(sK55))
| ~ ssList(nil)
| spl60_284 ),
inference(resolution,[],[f10809,f387]) ).
fof(f10816,plain,
( ~ ssItem(hd(sK55))
| spl60_284 ),
inference(forward_subsumption_resolution,[],[f10815,f388]) ).
fof(f10817,plain,
( ~ spl60_285
| spl60_284 ),
inference(avatar_split_clause,[],[f10816,f10807,f10811]) ).
fof(f11127,plain,
( nil = sK55
| ~ ssList(sK55)
| spl60_285 ),
inference(resolution,[],[f10812,f396]) ).
fof(f11128,plain,
( ~ ssList(sK55)
| spl60_285 ),
inference(forward_subsumption_resolution,[],[f11127,f514]) ).
fof(f11129,plain,
( $false
| spl60_285 ),
inference(forward_subsumption_resolution,[],[f11128,f497]) ).
fof(f11130,plain,
spl60_285,
inference(avatar_contradiction_clause,[],[f11129]) ).
fof(f11142,plain,
( cons(hd(sK55),nil) = app(nil,cons(hd(sK55),nil))
| ~ spl60_284 ),
inference(resolution,[],[f10808,f402]) ).
fof(f17049,plain,
( sK55 = cons(sK50(sK55),sK49(sK55))
| nil = sK55 ),
inference(resolution,[],[f392,f497]) ).
fof(f17054,plain,
sK55 = cons(sK50(sK55),sK49(sK55)),
inference(forward_subsumption_resolution,[],[f17049,f514]) ).
fof(f17087,definition,
( spl60_357
<=> ssList(sK49(sK55)) ),
introduced(definition,[new_symbols(definition,[spl60_357])],[avatar_definition]) ).
fof(f17088,plain,
( ssList(sK49(sK55))
| ~ spl60_357 ),
inference(avatar_component_clause,[],[f17087]) ).
fof(f17089,plain,
( ~ ssList(sK49(sK55))
| spl60_357 ),
inference(avatar_component_clause,[],[f17087]) ).
fof(f17095,plain,
( nil = sK55
| ~ ssList(sK55)
| spl60_357 ),
inference(resolution,[],[f17089,f394]) ).
fof(f17096,plain,
( ~ ssList(sK55)
| spl60_357 ),
inference(forward_subsumption_resolution,[],[f17095,f514]) ).
fof(f17097,plain,
( $false
| spl60_357 ),
inference(forward_subsumption_resolution,[],[f17096,f497]) ).
fof(f17098,plain,
spl60_357,
inference(avatar_contradiction_clause,[],[f17097]) ).
fof(f17124,plain,
( ! [X0] :
( ~ ssItem(X0)
| hd(cons(X0,sK49(sK55))) = X0 )
| ~ spl60_357 ),
inference(resolution,[],[f17088,f397]) ).
fof(f17125,plain,
( ! [X0] :
( ~ ssItem(X0)
| sK49(sK55) = tl(cons(X0,sK49(sK55))) )
| ~ spl60_357 ),
inference(resolution,[],[f17088,f399]) ).
fof(f17885,definition,
( spl60_377
<=> ssList(tl(sK55)) ),
introduced(definition,[new_symbols(definition,[spl60_377])],[avatar_definition]) ).
fof(f17886,plain,
( ssList(tl(sK55))
| ~ spl60_377 ),
inference(avatar_component_clause,[],[f17885]) ).
fof(f17887,plain,
( ~ ssList(tl(sK55))
| spl60_377 ),
inference(avatar_component_clause,[],[f17885]) ).
fof(f17889,plain,
( nil = sK55
| ~ ssList(sK55)
| spl60_377 ),
inference(resolution,[],[f17887,f398]) ).
fof(f17890,plain,
( ~ ssList(sK55)
| spl60_377 ),
inference(forward_subsumption_resolution,[],[f17889,f514]) ).
fof(f17891,plain,
( $false
| spl60_377 ),
inference(forward_subsumption_resolution,[],[f17890,f497]) ).
fof(f17892,plain,
spl60_377,
inference(avatar_contradiction_clause,[],[f17891]) ).
fof(f18461,definition,
( spl60_382
<=> ssItem(sK50(sK55)) ),
introduced(definition,[new_symbols(definition,[spl60_382])],[avatar_definition]) ).
fof(f18462,plain,
( ssItem(sK50(sK55))
| ~ spl60_382 ),
inference(avatar_component_clause,[],[f18461]) ).
fof(f18463,plain,
( ~ ssItem(sK50(sK55))
| spl60_382 ),
inference(avatar_component_clause,[],[f18461]) ).
fof(f18469,plain,
( nil = sK55
| ~ ssList(sK55)
| spl60_382 ),
inference(resolution,[],[f18463,f393]) ).
fof(f18470,plain,
( ~ ssList(sK55)
| spl60_382 ),
inference(forward_subsumption_resolution,[],[f18469,f514]) ).
fof(f18471,plain,
( $false
| spl60_382 ),
inference(forward_subsumption_resolution,[],[f18470,f497]) ).
fof(f18472,plain,
spl60_382,
inference(avatar_contradiction_clause,[],[f18471]) ).
fof(f18481,plain,
( sK50(sK55) = hd(cons(sK50(sK55),sK49(sK55)))
| ~ spl60_357
| ~ spl60_382 ),
inference(resolution,[],[f18462,f17124]) ).
fof(f18482,plain,
( sK49(sK55) = tl(cons(sK50(sK55),sK49(sK55)))
| ~ spl60_357
| ~ spl60_382 ),
inference(resolution,[],[f18462,f17125]) ).
fof(f18484,plain,
( tl(sK55) = sK49(sK55)
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f18482,f17054]) ).
fof(f18485,plain,
( hd(sK55) = sK50(sK55)
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f18481,f17054]) ).
fof(f19374,plain,
( sK55 = cons(sK50(sK55),tl(sK55))
| ~ spl60_357
| ~ spl60_382 ),
inference(superposition,[],[f17054,f18484]) ).
fof(f19387,plain,
( sK55 = cons(hd(sK55),tl(sK55))
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f19374,f18485]) ).
fof(f22437,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(hd(sK55))
| ssItem(sK57(hd(sK55),nil,X0)) )
| ~ spl60_284 ),
inference(superposition,[],[f515,f11142]) ).
fof(f22438,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(X0)
| ~ ssItem(hd(sK55))
| ssItem(sK57(hd(sK55),nil,X0)) )
| ~ spl60_284 ),
inference(forward_subsumption_resolution,[],[f22437,f388]) ).
fof(f22441,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(X0)
| ssItem(sK57(hd(sK55),nil,X0)) )
| ~ spl60_284
| ~ spl60_285 ),
inference(forward_subsumption_resolution,[],[f22438,f10813]) ).
fof(f23221,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(hd(sK55))
| memberP(nil,sK57(hd(sK55),nil,X0)) )
| ~ spl60_284 ),
inference(superposition,[],[f516,f11142]) ).
fof(f23222,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(X0)
| ~ ssItem(hd(sK55))
| memberP(nil,sK57(hd(sK55),nil,X0)) )
| ~ spl60_284 ),
inference(forward_subsumption_resolution,[],[f23221,f388]) ).
fof(f23225,plain,
( ! [X0] :
( sK55 != app(cons(hd(sK55),nil),X0)
| ~ ssList(X0)
| memberP(nil,sK57(hd(sK55),nil,X0)) )
| ~ spl60_284
| ~ spl60_285 ),
inference(forward_subsumption_resolution,[],[f23222,f10813]) ).
fof(f49543,plain,
( ! [X0] :
( ~ ssItem(X0)
| cons(X0,sK49(sK55)) = app(cons(X0,nil),sK49(sK55)) )
| ~ spl60_357 ),
inference(resolution,[],[f476,f17088]) ).
fof(f49554,plain,
( ! [X0] :
( ~ ssItem(X0)
| cons(X0,tl(sK55)) = app(cons(X0,nil),tl(sK55)) )
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f49543,f18484]) ).
fof(f62863,plain,
( cons(sK50(sK55),tl(sK55)) = app(cons(sK50(sK55),nil),tl(sK55))
| ~ spl60_357
| ~ spl60_382 ),
inference(resolution,[],[f49554,f18462]) ).
fof(f62866,plain,
( cons(hd(sK55),tl(sK55)) = app(cons(hd(sK55),nil),tl(sK55))
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f62863,f18485]) ).
fof(f62879,plain,
( sK55 = app(cons(hd(sK55),nil),tl(sK55))
| ~ spl60_357
| ~ spl60_382 ),
inference(forward_demodulation,[],[f62866,f19387]) ).
fof(f105074,plain,
( sK55 != sK55
| ~ ssList(tl(sK55))
| memberP(nil,sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_382 ),
inference(superposition,[],[f23225,f62879]) ).
fof(f105078,plain,
( ~ ssList(tl(sK55))
| memberP(nil,sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_382 ),
inference(trivial_inequality_removal,[],[f105074]) ).
fof(f105082,plain,
( memberP(nil,sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(forward_subsumption_resolution,[],[f105078,f17886]) ).
fof(f105091,plain,
( ~ ssItem(sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(resolution,[],[f105082,f418]) ).
fof(f132092,plain,
( sK55 != sK55
| ~ ssList(tl(sK55))
| ssItem(sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_382 ),
inference(superposition,[],[f22441,f62879]) ).
fof(f132096,plain,
( ~ ssList(tl(sK55))
| ssItem(sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_382 ),
inference(trivial_inequality_removal,[],[f132092]) ).
fof(f132098,plain,
( ssItem(sK57(hd(sK55),nil,tl(sK55)))
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(forward_subsumption_resolution,[],[f132096,f17886]) ).
fof(f132100,plain,
( $false
| ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(forward_subsumption_resolution,[],[f132098,f105091]) ).
fof(f132101,plain,
( ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(avatar_contradiction_clause,[],[f132100]) ).
cnf(s5885,plain,
( spl60_284
| ~ spl60_285 ),
inference(sat_conversion,[],[f10817]) ).
cnf(s6063,plain,
spl60_285,
inference(sat_conversion,[],[f11130]) ).
cnf(s8607,plain,
spl60_357,
inference(sat_conversion,[],[f17098]) ).
cnf(s8949,plain,
spl60_377,
inference(sat_conversion,[],[f17892]) ).
cnf(s9156,plain,
spl60_382,
inference(sat_conversion,[],[f18472]) ).
cnf(s47432,plain,
( ~ spl60_284
| ~ spl60_285
| ~ spl60_357
| ~ spl60_377
| ~ spl60_382 ),
inference(sat_conversion,[],[f132101]) ).
cnf(s47459,plain,
~ spl60_284,
inference(rat,[],[s47432,s9156,s8949,s8607,s6063]) ).
cnf(s47466,plain,
$false,
inference(rat,[],[s5885,s6063,s47459]) ).
fof(f132104,plain,
$false,
inference(avatar_sat_refutation,[],[s47466]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC246+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n013.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 08:39:06 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 13.96/2.23 % (1028093)Will run a generic schedule for satisfiability detection.
% 13.96/2.23 % (1028103)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1425315432:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.96/2.23 % (1028099)% WARNING: option uhcvi not known.
% 13.96/2.23 % (1028098)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=96467661_2999 on theBenchmark for (2999ds/0Mi)
% 13.96/2.23 % (1028099)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4041080217:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.96/2.23 % (1028100)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=911326581:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.96/2.23 % (1028101)dis+10_1_sil=32000:sp=arity:random_seed=1941196179:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.96/2.23 % (1028102)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2436761305:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.96/2.23 % (1028104)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1741420408:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.96/2.23 % TRYING [1]
% 13.96/2.23 % TRYING [2]
% 13.96/2.23 % TRYING [3]
% 13.96/2.23 % (1028103)Instruction limit reached!
% 13.96/2.23 % (1028103)------------------------------
% 13.96/2.23 % (1028103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.23 % (1028103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.23 % (1028103)CaDiCaL version: 2.1.3
% 13.96/2.23 % (1028103)Termination reason: Instruction limit
% 13.96/2.23 % (1028103)Termination phase: Saturation
% 13.96/2.23 % (1028103)Time elapsed: 0.040 s
% 13.96/2.23 % (1028103)Peak memory usage: 14 MB
% 13.96/2.23 % (1028103)Instructions burned: 132 (million)
% 13.96/2.23 % TRYING [4]
% 13.96/2.23 % (1028112)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1687575955:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.96/2.23 % TRYING [1]
% 13.96/2.23 % TRYING [2]
% 13.96/2.23 % TRYING [3]
% 13.96/2.23 % (1028101)Instruction limit reached!
% 13.96/2.23 % (1028101)------------------------------
% 13.96/2.23 % (1028101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.23 % (1028101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.23 % (1028101)CaDiCaL version: 2.1.3
% 13.96/2.23 % (1028101)Termination reason: Instruction limit
% 13.96/2.23 % (1028101)Termination phase: Saturation
% 13.96/2.23 % (1028101)Time elapsed: 0.060 s
% 13.96/2.23 % (1028101)Peak memory usage: 13 MB
% 13.96/2.23 % (1028101)Instructions burned: 103 (million)
% 13.96/2.23 % TRYING [4]
% 13.96/2.23 % (1028102)Instruction limit reached!
% 13.96/2.23 % (1028102)------------------------------
% 13.96/2.23 % (1028102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.23 % (1028102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.23 % (1028102)CaDiCaL version: 2.1.3
% 13.96/2.23 % (1028102)Termination reason: Instruction limit
% 13.96/2.23 % (1028102)Termination phase: Saturation
% 13.96/2.23 % (1028102)Time elapsed: 0.066 s
% 13.96/2.23 % (1028102)Peak memory usage: 13 MB
% 13.96/2.23 % (1028102)Instructions burned: 117 (million)
% 13.96/2.23 % (1028114)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3987552306:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.96/2.23 % (1028115)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=4215557359:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.96/2.23 % TRYING [5]
% 13.96/2.23 % TRYING [5]
% 13.96/2.23 % (1028104)Instruction limit reached!
% 13.96/2.23 % (1028104)------------------------------
% 13.96/2.23 % (1028104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.96/2.23 % (1028104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.23 % (1028104)CaDiCaL version: 2.1.3
% 13.96/2.23 % (1028104)Termination reason: Instruction limit
% 13.96/2.23 % (1028104)Termination phase: Saturation
% 13.96/2.23 % (1028104)Time elapsed: 0.102 s
% 13.96/2.23 % (1028104)Peak memory usage: 15 MB
% 13.96/2.23 % (1028104)Instructions burned: 160 (million)
% 13.96/2.23 % (1028118)ott-21_1_sil=16000:fs=off:random_seed=2775610396:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.96/2.23 % (1028114)Instruction limit reached!
% 13.96/2.23 % (1028114)------------------------------
% 13.96/2.23 % (1028114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028114)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028114)Termination reason: Instruction limit
% 37.51/5.68 % (1028114)Termination phase: Saturation
% 37.51/5.68 % (1028114)Time elapsed: 0.072 s
% 37.51/5.68 % (1028114)Peak memory usage: 13 MB
% 37.51/5.68 % (1028114)Instructions burned: 132 (million)
% 37.51/5.68 % (1028120)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4066708822:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 37.51/5.68 % TRYING [6]
% 37.51/5.68 % (1028112)Instruction limit reached!
% 37.51/5.68 % (1028112)------------------------------
% 37.51/5.68 % (1028112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028112)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028112)Termination reason: Instruction limit
% 37.51/5.68 % (1028112)Termination phase: Finite model building constraint generation
% 37.51/5.68 % (1028112)Time elapsed: 0.159 s
% 37.51/5.68 % (1028112)Peak memory usage: 29 MB
% 37.51/5.68 % (1028112)Instructions burned: 719 (million)
% 37.51/5.68 % (1028118)Instruction limit reached!
% 37.51/5.68 % (1028118)------------------------------
% 37.51/5.68 % (1028118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028118)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028118)Termination reason: Instruction limit
% 37.51/5.68 % (1028118)Termination phase: Saturation
% 37.51/5.68 % (1028118)Time elapsed: 0.091 s
% 37.51/5.68 % (1028118)Peak memory usage: 13 MB
% 37.51/5.68 % (1028118)Instructions burned: 181 (million)
% 37.51/5.68 % (1028122)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=535462895:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.51/5.68 % TRYING [1]
% 37.51/5.68 % TRYING [2]
% 37.51/5.68 % TRYING [3]
% 37.51/5.68 % (1028123)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3424014308:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 37.51/5.68 % TRYING [6]
% 37.51/5.68 % TRYING [4]
% 37.51/5.68 % TRYING [5]
% 37.51/5.68 % (1028122)Instruction limit reached!
% 37.51/5.68 % (1028122)------------------------------
% 37.51/5.68 % (1028122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028122)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028122)Termination reason: Instruction limit
% 37.51/5.68 % (1028122)Termination phase: Finite model building SAT solving
% 37.51/5.68 % (1028122)Time elapsed: 0.182 s
% 37.51/5.68 % (1028122)Peak memory usage: 24 MB
% 37.51/5.68 % (1028122)Instructions burned: 869 (million)
% 37.51/5.68 % (1028126)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=832648310:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.51/5.68 % (1028115)Instruction limit reached!
% 37.51/5.68 % (1028115)------------------------------
% 37.51/5.68 % (1028115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028115)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028115)Termination reason: Instruction limit
% 37.51/5.68 % (1028115)Termination phase: Saturation
% 37.51/5.68 % (1028115)Time elapsed: 0.366 s
% 37.51/5.68 % (1028115)Peak memory usage: 24 MB
% 37.51/5.68 % (1028115)Instructions burned: 685 (million)
% 37.51/5.68 % (1028128)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=775458003:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 37.51/5.68 % TRYING [14]
% 37.51/5.68 % (1028120)Instruction limit reached!
% 37.51/5.68 % (1028120)------------------------------
% 37.51/5.68 % (1028120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.51/5.68 % (1028120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.51/5.68 % (1028120)CaDiCaL version: 2.1.3
% 37.51/5.68 % (1028120)Termination reason: Instruction limit
% 37.51/5.68 % (1028120)Termination phase: Saturation
% 37.51/5.68 % (1028120)Time elapsed: 0.318 s
% 37.51/5.68 % (1028120)Peak memory usage: 15 MB
% 37.51/5.68 % (1028120)Instructions burned: 477 (million)
% 37.51/5.68 % (1028130)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3302596589:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 37.51/5.68 % TRYING [7]
% 37.51/5.68 % (1028126)Instruction limit reached!
% 66.44/9.69 % (1028126)------------------------------
% 66.44/9.69 % (1028126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028126)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028126)Termination reason: Instruction limit
% 66.44/9.69 % (1028126)Termination phase: Finite model building constraint generation
% 66.44/9.69 % (1028126)Time elapsed: 0.185 s
% 66.44/9.69 % (1028126)Peak memory usage: 76 MB
% 66.44/9.69 % (1028126)Instructions burned: 894 (million)
% 66.44/9.69 % (1028132)fmb+10_1_sil=64000:random_seed=2669610580:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 66.44/9.69 % TRYING [1]
% 66.44/9.69 % TRYING [2]
% 66.44/9.69 % TRYING [3]
% 66.44/9.69 % TRYING [4]
% 66.44/9.69 % TRYING [5]
% 66.44/9.69 % (1028128)Instruction limit reached!
% 66.44/9.69 % (1028128)------------------------------
% 66.44/9.69 % (1028128)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028128)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028128)Termination reason: Instruction limit
% 66.44/9.69 % (1028128)Termination phase: Saturation
% 66.44/9.69 % (1028128)Time elapsed: 0.364 s
% 66.44/9.69 % (1028128)Peak memory usage: 23 MB
% 66.44/9.69 % (1028128)Instructions burned: 695 (million)
% 66.44/9.69 % (1028134)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2736714080:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 66.44/9.69 % TRYING [20]
% 66.44/9.69 % (1028123)Instruction limit reached!
% 66.44/9.69 % (1028123)------------------------------
% 66.44/9.69 % (1028123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028123)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028123)Termination reason: Instruction limit
% 66.44/9.69 % (1028123)Termination phase: Saturation
% 66.44/9.69 % (1028123)Time elapsed: 0.650 s
% 66.44/9.69 % (1028123)Peak memory usage: 26 MB
% 66.44/9.69 % (1028123)Instructions burned: 1180 (million)
% 66.44/9.69 % TRYING [6]
% 66.44/9.69 % (1028136)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1123894218:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 66.44/9.69 % TRYING [8]
% 66.44/9.69 % (1028130)Instruction limit reached!
% 66.44/9.69 % (1028130)------------------------------
% 66.44/9.69 % (1028130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028130)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028130)Termination reason: Instruction limit
% 66.44/9.69 % (1028130)Termination phase: Saturation
% 66.44/9.69 % (1028130)Time elapsed: 0.460 s
% 66.44/9.69 % (1028130)Peak memory usage: 20 MB
% 66.44/9.69 % (1028130)Instructions burned: 880 (million)
% 66.44/9.69 % (1028138)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2598280107:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 66.44/9.69 % (1028136)Instruction limit reached!
% 66.44/9.69 % (1028136)------------------------------
% 66.44/9.69 % (1028136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028136)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028136)Termination reason: Instruction limit
% 66.44/9.69 % (1028136)Termination phase: Finite model building constraint generation
% 66.44/9.69 % (1028136)Time elapsed: 0.342 s
% 66.44/9.69 % (1028136)Peak memory usage: 74 MB
% 66.44/9.69 % (1028136)Instructions burned: 922 (million)
% 66.44/9.69 % (1028140)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=239268703:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 66.44/9.69 % TRYING [7]
% 66.44/9.69 % TRYING [8]
% 66.44/9.69 % (1028140)Instruction limit reached!
% 66.44/9.69 % (1028140)------------------------------
% 66.44/9.69 % (1028140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.44/9.69 % (1028140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.44/9.69 % (1028140)CaDiCaL version: 2.1.3
% 66.44/9.69 % (1028140)Termination reason: Instruction limit
% 66.44/9.69 % (1028140)Termination phase: Saturation
% 66.44/9.69 % (1028140)Time elapsed: 0.667 s
% 66.44/9.69 % (1028140)Peak memory usage: 22 MB
% 66.44/9.69 % (1028140)Instructions burned: 1472 (million)
% 66.44/9.69 % (1028142)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4293101117:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 99.41/29.83 % TRYING [77]
% 99.41/29.83 % TRYING [8]
% 99.41/29.83 % TRYING [9]
% 99.41/29.83 % (1028138)Instruction limit reached!
% 99.41/29.83 % (1028138)------------------------------
% 99.41/29.83 % (1028138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028138)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028138)Termination reason: Instruction limit
% 99.41/29.83 % (1028138)Termination phase: Saturation
% 99.41/29.83 % (1028138)Time elapsed: 2.801 s
% 99.41/29.83 % (1028138)Peak memory usage: 50 MB
% 99.41/29.83 % (1028138)Instructions burned: 5132 (million)
% 99.41/29.83 % (1028144)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2805753174:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 99.41/29.83 % TRYING [16]
% 99.41/29.83 % TRYING [9]
% 99.41/29.83 % (1028134)Instruction limit reached!
% 99.41/29.83 % (1028134)------------------------------
% 99.41/29.83 % (1028134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028134)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028134)Termination reason: Instruction limit
% 99.41/29.83 % (1028134)Termination phase: Finite model building constraint generation
% 99.41/29.83 % (1028134)Time elapsed: 3.324 s
% 99.41/29.83 % (1028134)Peak memory usage: 562 MB
% 99.41/29.83 % (1028134)Instructions burned: 9516 (million)
% 99.41/29.83 % (1028146)ott-2_1_sil=16000:newcnf=on:random_seed=3180571042:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 99.41/29.83 % (1028142)Instruction limit reached!
% 99.41/29.83 % (1028142)------------------------------
% 99.41/29.83 % (1028142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028142)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028142)Termination reason: Instruction limit
% 99.41/29.83 % (1028142)Termination phase: Finite model building constraint generation
% 99.41/29.83 % (1028142)Time elapsed: 2.381 s
% 99.41/29.83 % (1028142)Peak memory usage: 524 MB
% 99.41/29.83 % (1028142)Instructions burned: 6325 (million)
% 99.41/29.83 % (1028148)ott+10_1_sil=32000:tgt=ground:random_seed=4086839888:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 99.41/29.83 % (1028144)Instruction limit reached!
% 99.41/29.83 % (1028144)------------------------------
% 99.41/29.83 % (1028144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028144)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028144)Termination reason: Instruction limit
% 99.41/29.83 % (1028144)Termination phase: Finite model building constraint generation
% 99.41/29.83 % (1028144)Time elapsed: 0.751 s
% 99.41/29.83 % (1028144)Peak memory usage: 138 MB
% 99.41/29.83 % (1028144)Instructions burned: 2176 (million)
% 99.41/29.83 % (1028150)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1758853935:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 99.41/29.83 % TRYING [1]
% 99.41/29.83 % TRYING [2]
% 99.41/29.83 % TRYING [3]
% 99.41/29.83 % TRYING [4]
% 99.41/29.83 % TRYING [5]
% 99.41/29.83 % (1028146)Instruction limit reached!
% 99.41/29.83 % (1028146)------------------------------
% 99.41/29.83 % (1028146)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028146)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028146)Termination reason: Instruction limit
% 99.41/29.83 % (1028146)Termination phase: Saturation
% 99.41/29.83 % (1028146)Time elapsed: 0.471 s
% 99.41/29.83 % (1028146)Peak memory usage: 20 MB
% 99.41/29.83 % (1028146)Instructions burned: 869 (million)
% 99.41/29.83 % (1028152)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1774032398:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 99.41/29.83 % TRYING [6]
% 99.41/29.83 % TRYING [7]
% 99.41/29.83 % (1028132)Instruction limit reached!
% 99.41/29.83 % (1028132)------------------------------
% 99.41/29.83 % (1028132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028132)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028132)Termination reason: Instruction limit
% 99.41/29.83 % (1028132)Termination phase: Finite model building SAT solving
% 99.41/29.83 % (1028132)Time elapsed: 4.802 s
% 99.41/29.83 % (1028132)Peak memory usage: 192 MB
% 99.41/29.83 % (1028132)Instructions burned: 22065 (million)
% 99.41/29.83 % (1028154)dis+21_1_sil=32000:sas=cadical:random_seed=711753356:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 99.41/29.83 % TRYING [8]
% 99.41/29.83 % TRYING [10]
% 99.41/29.83 % (1028154)Instruction limit reached!
% 99.41/29.83 % (1028154)------------------------------
% 99.41/29.83 % (1028154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028154)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028154)Termination reason: Instruction limit
% 99.41/29.83 % (1028154)Termination phase: Saturation
% 99.41/29.83 % (1028154)Time elapsed: 1.054 s
% 99.41/29.83 % (1028154)Peak memory usage: 53 MB
% 99.41/29.83 % (1028154)Instructions burned: 3775 (million)
% 99.41/29.83 % (1028156)ott+11_1_sil=16000:gs=on:random_seed=2121286300:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 99.41/29.83 % (1028152)Instruction limit reached!
% 99.41/29.83 % (1028152)------------------------------
% 99.41/29.83 % (1028152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028152)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028152)Termination reason: Instruction limit
% 99.41/29.83 % (1028152)Termination phase: Saturation
% 99.41/29.83 % (1028152)Time elapsed: 1.872 s
% 99.41/29.83 % (1028152)Peak memory usage: 40 MB
% 99.41/29.83 % (1028152)Instructions burned: 3512 (million)
% 99.41/29.83 % (1028158)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2471629158:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 99.41/29.83 % TRYING [7]
% 99.41/29.83 % (1028156)Instruction limit reached!
% 99.41/29.83 % (1028156)------------------------------
% 99.41/29.83 % (1028156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028156)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028156)Termination reason: Instruction limit
% 99.41/29.83 % (1028156)Termination phase: Saturation
% 99.41/29.83 % (1028156)Time elapsed: 0.507 s
% 99.41/29.83 % (1028156)Peak memory usage: 16 MB
% 99.41/29.83 % (1028156)Instructions burned: 2256 (million)
% 99.41/29.83 % (1028160)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3227178102:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 99.41/29.83 % (1028148)Instruction limit reached!
% 99.41/29.83 % (1028148)------------------------------
% 99.41/29.83 % (1028148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028148)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028148)Termination reason: Instruction limit
% 99.41/29.83 % (1028148)Termination phase: Saturation
% 99.41/29.83 % (1028148)Time elapsed: 2.790 s
% 99.41/29.83 % (1028148)Peak memory usage: 72 MB
% 99.41/29.83 % (1028148)Instructions burned: 5114 (million)
% 99.41/29.83 % (1028162)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=986614747:i=29340_2927 on theBenchmark for (2927ds/29340Mi)
% 99.41/29.83 % TRYING [9]
% 99.41/29.83 % (1028160)Instruction limit reached!
% 99.41/29.83 % (1028160)------------------------------
% 99.41/29.83 % (1028160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028160)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028160)Termination reason: Instruction limit
% 99.41/29.83 % (1028160)Termination phase: Saturation
% 99.41/29.83 % (1028160)Time elapsed: 1.057 s
% 99.41/29.83 % (1028160)Peak memory usage: 54 MB
% 99.41/29.83 % (1028160)Instructions burned: 4593 (million)
% 99.41/29.83 % (1028164)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3927428590:i=5211_2918 on theBenchmark for (2918ds/5211Mi)
% 99.41/29.83 % TRYING [8]
% 99.41/29.83 % (1028164)Instruction limit reached!
% 99.41/29.83 % (1028164)------------------------------
% 99.41/29.83 % (1028164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028164)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028164)Termination reason: Instruction limit
% 99.41/29.83 % (1028164)Termination phase: Saturation
% 99.41/29.83 % (1028164)Time elapsed: 1.306 s
% 99.41/29.83 % (1028164)Peak memory usage: 50 MB
% 99.41/29.83 % (1028164)Instructions burned: 5212 (million)
% 99.41/29.83 % (1028166)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4189474325:i=5497:nm=2_2905 on theBenchmark for (2905ds/5497Mi)
% 99.41/29.83 % TRYING [17]
% 99.41/29.83 % (1028166)Instruction limit reached!
% 99.41/29.83 % (1028166)------------------------------
% 99.41/29.83 % (1028166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028166)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028166)Termination reason: Instruction limit
% 99.41/29.83 % (1028166)Termination phase: Finite model building constraint generation
% 99.41/29.83 % (1028166)Time elapsed: 1.049 s
% 99.41/29.83 % (1028166)Peak memory usage: 322 MB
% 99.41/29.83 % (1028166)Instructions burned: 5501 (million)
% 99.41/29.83 % (1028168)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=656747592:fmbsr=2:i=46332_2894 on theBenchmark for (2894ds/46332Mi)
% 99.41/29.83 % TRYING [15]
% 99.41/29.83 % TRYING [10]
% 99.41/29.83 % TRYING [9]
% 99.41/29.83 % TRYING [11]
% 99.41/29.83 % TRYING [10]
% 99.41/29.83 % TRYING [11]
% 99.41/29.83 % (1028162)Instruction limit reached!
% 99.41/29.83 % (1028162)------------------------------
% 99.41/29.83 % (1028162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028162)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028162)Termination reason: Instruction limit
% 99.41/29.83 % (1028162)Termination phase: Saturation
% 99.41/29.83 % (1028162)Time elapsed: 14.207 s
% 99.41/29.83 % (1028162)Peak memory usage: 480 MB
% 99.41/29.83 % (1028162)Instructions burned: 29342 (million)
% 99.41/29.83 % (1028170)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3937572925:i=14071_2784 on theBenchmark for (2784ds/14071Mi)
% 99.41/29.83 % TRYING [12]
% 99.41/29.83 % (1028168)Instruction limit reached!
% 99.41/29.83 % (1028168)------------------------------
% 99.41/29.83 % (1028168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028168)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028168)Termination reason: Instruction limit
% 99.41/29.83 % (1028168)Termination phase: Finite model building SAT solving
% 99.41/29.83 % (1028168)Time elapsed: 14.939 s
% 99.41/29.83 % (1028168)Peak memory usage: 2707 MB
% 99.41/29.83 % (1028168)Instructions burned: 46335 (million)
% 99.41/29.83 % TRYING [11]
% 99.41/29.83 % (1028172)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=490551433:i=22565:add=on:rawr=on_2742 on theBenchmark for (2742ds/22565Mi)
% 99.41/29.83 % (1028170)Instruction limit reached!
% 99.41/29.83 % (1028170)------------------------------
% 99.41/29.83 % (1028170)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028170)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028170)Termination reason: Instruction limit
% 99.41/29.83 % (1028170)Termination phase: Finite model building constraint generation
% 99.41/29.83 % (1028170)Time elapsed: 5.795 s
% 99.41/29.83 % (1028170)Peak memory usage: 827 MB
% 99.41/29.83 % (1028170)Instructions burned: 14072 (million)
% 99.41/29.83 % (1028174)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3646562751:i=8173:av=off_2725 on theBenchmark for (2725ds/8173Mi)
% 99.41/29.83 % (1028172) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1028093-1028172"...
% 99.41/29.83 % (1028172)...printing done.
% 99.41/29.83 % (1028172)Refutation found. Thanks to Tanya!
% 99.41/29.83 % SZS status Theorem for theBenchmark
% 99.41/29.83 % SZS output start Proof for theBenchmark
% See solution above
% 99.41/29.83 % (1028172)------------------------------
% 99.41/29.83 % (1028172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.41/29.83 % (1028172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.41/29.83 % (1028172)CaDiCaL version: 2.1.3
% 99.41/29.83 % (1028172)Termination reason: Refutation
% 99.41/29.83 % (1028172)Time elapsed: 3.714 s
% 99.41/29.83 % (1028172)Peak memory usage: 78 MB
% 99.41/29.83 % (1028172)Instructions burned: 9112 (million)
% 99.41/29.83 % (1028093)Success in time 29.61 s
% 99.41/29.83 % Vampire exiting
%------------------------------------------------------------------------------