%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC298-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:03:21 PM UTC 2026
% Result : Unsatisfiable 4.63s 1.35s
% Output : Refutation 5.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 39
% Syntax : Number of formulae : 183 ( 36 unt; 19 def)
% Number of atoms : 520 ( 37 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 646 ( 309 ~; 318 |; 0 &)
% ( 19 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 25 ( 23 usr; 20 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 49 ( 0 sgn 49 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f63,axiom,
! [X0] :
( ~ lt(X0,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ssList(cons(X0,X1))
| ~ ssList(X1)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f126,plain,
! [X0,X1] :
( cons(X0,X1) = app(cons(X0,nil),X1)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(reorient_equations,[],[f125]) ).
fof(f151,axiom,
! [X2,X0,X1] :
( memberP(app(X0,X2),X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause140) ).
fof(f161,axiom,
! [X2,X0,X1] :
( app(app(X2,X1),X0) = app(X2,app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X2)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f173,axiom,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X2 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ memberP(cons(X0,X1),X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| X0 = X2 ),
inference(reorient_equations,[],[f173]) ).
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/theBenchmark.p',clause175) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
ssItem(sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
ssList(sk7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
ssList(sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
ssList(sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9) = sk1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f212,plain,
sk1 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(reorient_equations,[],[f211]) ).
fof(f213,negated_conjecture,
lt(sk6,sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_13) ).
fof(f215,negated_conjecture,
( ssItem(sk10)
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_15) ).
fof(f220,negated_conjecture,
( cons(sk10,nil) = sk3
| nil = sk3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_19) ).
fof(f221,plain,
( sk3 = cons(sk10,nil)
| nil = sk3 ),
inference(reorient_equations,[],[f220]) ).
fof(f227,plain,
! [X2,X0,X1] :
( memberP(app(X0,cons(X1,X2)),X1)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| ~ ssList(X2) ),
inference(equality_resolution,[],[f189]) ).
fof(f233,definition,
( spl0_1
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f234,plain,
( nil = sk3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f244,definition,
( spl0_4
<=> sk3 = cons(sk10,nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f245,plain,
( sk3 = cons(sk10,nil)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f246,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f221,f244,f233]) ).
fof(f254,definition,
( spl0_6
<=> ssItem(sk10) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f255,plain,
( ssItem(sk10)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f256,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f215,f254,f233]) ).
fof(f292,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ~ ssItem(sk10)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f174,f245]) ).
fof(f305,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(sk10)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f292,f8]) ).
fof(f315,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f305,f255]) ).
fof(f318,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| sk10 = X0 )
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f315,f71]) ).
fof(f323,plain,
sk3 = app(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),sk9),
inference(forward_demodulation,[],[f212,f205]) ).
fof(f408,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9))
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(sk9) ),
inference(superposition,[],[f323,f161]) ).
fof(f413,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(sk9)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(superposition,[],[f151,f323]) ).
fof(f430,plain,
! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssItem(X0)
| ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0) ),
inference(forward_subsumption_resolution,[],[f413,f210]) ).
fof(f432,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9))
| ~ ssList(cons(sk6,nil))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
inference(forward_subsumption_resolution,[],[f408,f210]) ).
fof(f436,definition,
( spl0_9
<=> ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f437,plain,
( ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| spl0_9 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f465,definition,
( spl0_16
<=> ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f466,plain,
( ! [X0] :
( ~ memberP(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f465]) ).
fof(f467,plain,
( ~ spl0_9
| spl0_16 ),
inference(avatar_split_clause,[],[f430,f465,f436]) ).
fof(f469,definition,
( spl0_17
<=> ssList(app(app(sk7,cons(sk5,nil)),sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f470,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| spl0_17 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f472,definition,
( spl0_18
<=> ssList(cons(sk6,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f473,plain,
( ~ ssList(cons(sk6,nil))
| spl0_18 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f475,definition,
( spl0_19
<=> sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f476,plain,
( sk3 = app(app(app(sk7,cons(sk5,nil)),sk8),app(cons(sk6,nil),sk9))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f478,plain,
( ~ spl0_17
| ~ spl0_18
| spl0_19 ),
inference(avatar_split_clause,[],[f432,f475,f472,f469]) ).
fof(f480,definition,
( spl0_20
<=> ssList(app(sk7,cons(sk5,nil))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f481,plain,
( ~ ssList(app(sk7,cons(sk5,nil)))
| spl0_20 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f488,definition,
( spl0_22
<=> ssList(cons(sk5,nil)) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f489,plain,
( ~ ssList(cons(sk5,nil))
| spl0_22 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f494,plain,
( ~ ssList(nil)
| ~ ssItem(sk6)
| spl0_18 ),
inference(resolution,[],[f473,f86]) ).
fof(f495,plain,
( ~ ssItem(sk6)
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f494,f8]) ).
fof(f496,plain,
( $false
| spl0_18 ),
inference(forward_subsumption_resolution,[],[f495,f207]) ).
fof(f497,plain,
spl0_18,
inference(avatar_contradiction_clause,[],[f496]) ).
fof(f498,plain,
( ~ ssList(nil)
| ~ ssItem(sk5)
| spl0_22 ),
inference(resolution,[],[f489,f86]) ).
fof(f499,plain,
( ~ ssItem(sk5)
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f498,f8]) ).
fof(f500,plain,
( $false
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f499,f206]) ).
fof(f501,plain,
spl0_22,
inference(avatar_contradiction_clause,[],[f500]) ).
fof(f502,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,nil))
| spl0_20 ),
inference(resolution,[],[f481,f85]) ).
fof(f503,plain,
( ~ ssList(cons(sk5,nil))
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f502,f208]) ).
fof(f504,plain,
( ~ spl0_22
| spl0_20 ),
inference(avatar_split_clause,[],[f503,f480,f488]) ).
fof(f516,plain,
( ~ ssList(app(sk7,app(cons(sk5,nil),sk8)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk7)
| ~ ssList(sk8)
| spl0_17 ),
inference(superposition,[],[f470,f161]) ).
fof(f517,plain,
( ~ ssList(app(sk7,app(cons(sk5,nil),sk8)))
| ~ ssList(cons(sk5,nil))
| ~ ssList(sk8)
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f516,f208]) ).
fof(f519,plain,
( ~ ssList(app(sk7,app(cons(sk5,nil),sk8)))
| ~ ssList(cons(sk5,nil))
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f517,f209]) ).
fof(f522,definition,
( spl0_24
<=> ssList(app(sk7,app(cons(sk5,nil),sk8))) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f523,plain,
( ~ ssList(app(sk7,app(cons(sk5,nil),sk8)))
| spl0_24 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f524,plain,
( ~ spl0_22
| ~ spl0_24
| spl0_17 ),
inference(avatar_split_clause,[],[f519,f469,f522,f488]) ).
fof(f658,plain,
( ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(cons(sk6,nil))
| spl0_9 ),
inference(resolution,[],[f437,f85]) ).
fof(f663,plain,
( ~ spl0_18
| ~ spl0_17
| spl0_9 ),
inference(avatar_split_clause,[],[f658,f436,f469,f472]) ).
fof(f735,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(app(cons(sk6,nil),sk9))
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssItem(X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0) )
| ~ spl0_19 ),
inference(superposition,[],[f151,f476]) ).
fof(f745,definition,
( spl0_40
<=> ssList(app(cons(sk6,nil),sk9)) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f746,plain,
( ~ ssList(app(cons(sk6,nil),sk9))
| spl0_40 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f774,definition,
( spl0_47
<=> ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f775,plain,
( ! [X0] :
( ~ memberP(app(app(sk7,cons(sk5,nil)),sk8),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f776,plain,
( ~ spl0_17
| ~ spl0_40
| spl0_47
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f735,f475,f774,f745,f469]) ).
fof(f812,plain,
( ~ ssList(cons(sk6,sk9))
| ~ ssList(sk9)
| ~ ssItem(sk6)
| spl0_40 ),
inference(superposition,[],[f746,f126]) ).
fof(f813,plain,
( ~ ssList(sk9)
| ~ ssItem(sk6)
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f812,f86]) ).
fof(f815,plain,
( ~ ssItem(sk6)
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f813,f210]) ).
fof(f817,plain,
( $false
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f815,f207]) ).
fof(f818,plain,
spl0_40,
inference(avatar_contradiction_clause,[],[f817]) ).
fof(f909,definition,
( spl0_60
<=> ssList(app(sk7,cons(sk5,sk8))) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f910,plain,
( ~ ssList(app(sk7,cons(sk5,sk8)))
| spl0_60 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f916,definition,
( spl0_62
<=> ssList(cons(sk5,sk8)) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f917,plain,
( ~ ssList(cons(sk5,sk8))
| spl0_62 ),
inference(avatar_component_clause,[],[f916]) ).
fof(f922,plain,
( ~ ssList(sk8)
| ~ ssItem(sk5)
| spl0_62 ),
inference(resolution,[],[f917,f86]) ).
fof(f923,plain,
( ~ ssItem(sk5)
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f922,f209]) ).
fof(f924,plain,
( $false
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f923,f206]) ).
fof(f925,plain,
spl0_62,
inference(avatar_contradiction_clause,[],[f924]) ).
fof(f982,plain,
( ~ ssList(sk7)
| ~ ssList(cons(sk5,sk8))
| spl0_60 ),
inference(resolution,[],[f910,f85]) ).
fof(f983,plain,
( ~ ssList(cons(sk5,sk8))
| spl0_60 ),
inference(forward_subsumption_resolution,[],[f982,f208]) ).
fof(f984,plain,
( ~ spl0_62
| spl0_60 ),
inference(avatar_split_clause,[],[f983,f909,f916]) ).
fof(f986,plain,
( ~ ssList(app(sk7,cons(sk5,sk8)))
| ~ ssList(sk8)
| ~ ssItem(sk5)
| spl0_24 ),
inference(superposition,[],[f523,f126]) ).
fof(f987,plain,
( ~ ssList(app(sk7,cons(sk5,sk8)))
| ~ ssItem(sk5)
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f986,f209]) ).
fof(f989,plain,
( ~ ssList(app(sk7,cons(sk5,sk8)))
| spl0_24 ),
inference(forward_subsumption_resolution,[],[f987,f206]) ).
fof(f991,plain,
( ~ spl0_60
| spl0_24 ),
inference(avatar_split_clause,[],[f989,f522,f909]) ).
fof(f1015,plain,
( memberP(sk3,sk6)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssItem(sk6)
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(nil)
| ~ spl0_16 ),
inference(resolution,[],[f466,f227]) ).
fof(f1022,plain,
( memberP(sk3,sk6)
| ~ ssItem(sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(nil)
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1015]) ).
fof(f1031,plain,
( memberP(sk3,sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ ssList(nil)
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1022,f207]) ).
fof(f1034,plain,
( memberP(sk3,sk6)
| ~ ssList(app(app(sk7,cons(sk5,nil)),sk8))
| ~ ssList(app(app(app(sk7,cons(sk5,nil)),sk8),cons(sk6,nil)))
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1031,f8]) ).
fof(f1037,definition,
( spl0_74
<=> memberP(sk3,sk6) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f1038,plain,
( memberP(sk3,sk6)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f1037]) ).
fof(f1039,plain,
( ~ spl0_9
| ~ spl0_17
| spl0_74
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1034,f465,f1037,f469,f436]) ).
fof(f1040,plain,
( ~ ssItem(sk6)
| sk6 = sk10
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74 ),
inference(resolution,[],[f1038,f318]) ).
fof(f1041,plain,
( sk6 = sk10
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1040,f207]) ).
fof(f1053,plain,
( lt(sk10,sk5)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74 ),
inference(superposition,[],[f213,f1041]) ).
fof(f1142,plain,
( memberP(nil,sk6)
| ~ spl0_1
| ~ spl0_74 ),
inference(superposition,[],[f1038,f234]) ).
fof(f1160,plain,
( ~ ssItem(sk6)
| ~ spl0_1
| ~ spl0_74 ),
inference(resolution,[],[f1142,f71]) ).
fof(f1161,plain,
( $false
| ~ spl0_1
| ~ spl0_74 ),
inference(forward_subsumption_resolution,[],[f1160,f207]) ).
fof(f1162,plain,
( ~ spl0_1
| ~ spl0_74 ),
inference(avatar_contradiction_clause,[],[f1161]) ).
fof(f1198,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(nil)
| ~ ssItem(sk10)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4 ),
inference(superposition,[],[f174,f245]) ).
fof(f1211,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(sk10)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1198,f8]) ).
fof(f1221,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(nil,X0)
| sk10 = X0 )
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1211,f255]) ).
fof(f1224,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| sk10 = X0 )
| ~ spl0_4
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f1221,f71]) ).
fof(f1354,definition,
( spl0_88
<=> sk5 = sk10 ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1355,plain,
( sk5 = sk10
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f2762,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk8)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssItem(X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_47 ),
inference(resolution,[],[f775,f151]) ).
fof(f2766,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(sk8)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_47 ),
inference(duplicate_literal_removal,[],[f2762]) ).
fof(f2771,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(X0)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ memberP(app(sk7,cons(sk5,nil)),X0) )
| ~ spl0_47 ),
inference(forward_subsumption_resolution,[],[f2766,f209]) ).
fof(f2778,definition,
( spl0_215
<=> ! [X0] :
( memberP(sk3,X0)
| ~ memberP(app(sk7,cons(sk5,nil)),X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f2779,plain,
( ! [X0] :
( ~ memberP(app(sk7,cons(sk5,nil)),X0)
| memberP(sk3,X0)
| ~ ssItem(X0) )
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f2778]) ).
fof(f2780,plain,
( ~ spl0_20
| spl0_215
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f2771,f774,f2778,f480]) ).
fof(f2863,plain,
( memberP(sk3,sk5)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ~ ssItem(sk5)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_215 ),
inference(resolution,[],[f2779,f227]) ).
fof(f2868,plain,
( memberP(sk3,sk5)
| ~ ssItem(sk5)
| ~ ssList(sk7)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_215 ),
inference(duplicate_literal_removal,[],[f2863]) ).
fof(f2870,plain,
( memberP(sk3,sk5)
| ~ ssList(sk7)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_215 ),
inference(forward_subsumption_resolution,[],[f2868,f206]) ).
fof(f2875,plain,
( memberP(sk3,sk5)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ ssList(nil)
| ~ spl0_215 ),
inference(forward_subsumption_resolution,[],[f2870,f208]) ).
fof(f2876,plain,
( memberP(sk3,sk5)
| ~ ssList(app(sk7,cons(sk5,nil)))
| ~ spl0_215 ),
inference(forward_subsumption_resolution,[],[f2875,f8]) ).
fof(f2878,definition,
( spl0_227
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f2879,plain,
( memberP(sk3,sk5)
| ~ spl0_227 ),
inference(avatar_component_clause,[],[f2878]) ).
fof(f2880,plain,
( ~ spl0_20
| spl0_227
| ~ spl0_215 ),
inference(avatar_split_clause,[],[f2876,f2778,f2878,f480]) ).
fof(f2881,plain,
( ~ ssItem(sk5)
| sk5 = sk10
| ~ spl0_4
| ~ spl0_6
| ~ spl0_227 ),
inference(resolution,[],[f2879,f1224]) ).
fof(f2882,plain,
( sk5 = sk10
| ~ spl0_4
| ~ spl0_6
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2881,f206]) ).
fof(f2883,plain,
( spl0_88
| ~ spl0_4
| ~ spl0_6
| ~ spl0_227 ),
inference(avatar_split_clause,[],[f2882,f2878,f254,f244,f1354]) ).
fof(f2902,plain,
( lt(sk10,sk10)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74
| ~ spl0_88 ),
inference(superposition,[],[f1053,f1355]) ).
fof(f3006,plain,
( ~ ssItem(sk10)
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74
| ~ spl0_88 ),
inference(resolution,[],[f2902,f63]) ).
fof(f3019,plain,
( $false
| ~ spl0_4
| ~ spl0_6
| ~ spl0_74
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f3006,f255]) ).
fof(f3020,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_74
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f3019]) ).
cnf(s3,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f246]) ).
cnf(s7,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f256]) ).
cnf(s18,plain,
( ~ spl0_9
| spl0_16 ),
inference(sat_conversion,[],[f467]) ).
cnf(s20,plain,
( ~ spl0_17
| ~ spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f478]) ).
cnf(s23,plain,
spl0_18,
inference(sat_conversion,[],[f497]) ).
cnf(s24,plain,
spl0_22,
inference(sat_conversion,[],[f501]) ).
cnf(s25,plain,
( spl0_20
| ~ spl0_22 ),
inference(sat_conversion,[],[f504]) ).
cnf(s27,plain,
( spl0_17
| ~ spl0_22
| ~ spl0_24 ),
inference(sat_conversion,[],[f524]) ).
cnf(s36,plain,
( spl0_9
| ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f663]) ).
cnf(s54,plain,
( ~ spl0_17
| ~ spl0_19
| ~ spl0_40
| spl0_47 ),
inference(sat_conversion,[],[f776]) ).
cnf(s63,plain,
spl0_40,
inference(sat_conversion,[],[f818]) ).
cnf(s81,plain,
spl0_62,
inference(sat_conversion,[],[f925]) ).
cnf(s92,plain,
( spl0_60
| ~ spl0_62 ),
inference(sat_conversion,[],[f984]) ).
cnf(s94,plain,
( spl0_24
| ~ spl0_60 ),
inference(sat_conversion,[],[f991]) ).
cnf(s103,plain,
( ~ spl0_9
| ~ spl0_16
| ~ spl0_17
| spl0_74 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s118,plain,
( ~ spl0_1
| ~ spl0_74 ),
inference(sat_conversion,[],[f1162]) ).
cnf(s327,plain,
( ~ spl0_20
| ~ spl0_47
| spl0_215 ),
inference(sat_conversion,[],[f2780]) ).
cnf(s342,plain,
( ~ spl0_20
| ~ spl0_215
| spl0_227 ),
inference(sat_conversion,[],[f2880]) ).
cnf(s343,plain,
( ~ spl0_4
| ~ spl0_6
| spl0_88
| ~ spl0_227 ),
inference(sat_conversion,[],[f2883]) ).
cnf(s345,plain,
( ~ spl0_4
| ~ spl0_6
| ~ spl0_74
| ~ spl0_88 ),
inference(sat_conversion,[],[f3020]) ).
cnf(s362,plain,
spl0_60,
inference(rat,[],[s92,s81]) ).
cnf(s367,plain,
spl0_24,
inference(rat,[],[s94,s362]) ).
cnf(s375,plain,
( ~ spl0_17
| ~ spl0_19
| spl0_47 ),
inference(rat,[],[s54,s63]) ).
cnf(s392,plain,
( spl0_17
| ~ spl0_22 ),
inference(rat,[],[s27,s367]) ).
cnf(s394,plain,
spl0_17,
inference(rat,[],[s392,s24]) ).
cnf(s395,plain,
spl0_20,
inference(rat,[],[s25,s24]) ).
cnf(s398,plain,
spl0_9,
inference(rat,[],[s36,s394,s23]) ).
cnf(s411,plain,
spl0_19,
inference(rat,[],[s20,s23,s394]) ).
cnf(s413,plain,
spl0_47,
inference(rat,[],[s375,s394,s411]) ).
cnf(s421,plain,
spl0_215,
inference(rat,[],[s327,s395,s413]) ).
cnf(s425,plain,
spl0_227,
inference(rat,[],[s342,s395,s421]) ).
cnf(s427,plain,
spl0_16,
inference(rat,[],[s18,s398]) ).
cnf(s428,plain,
spl0_74,
inference(rat,[],[s103,s398,s394,s427]) ).
cnf(s431,plain,
~ spl0_1,
inference(rat,[],[s118,s428]) ).
cnf(s448,plain,
spl0_6,
inference(rat,[],[s7,s431]) ).
cnf(s450,plain,
spl0_4,
inference(rat,[],[s3,s431]) ).
cnf(s451,plain,
~ spl0_88,
inference(rat,[],[s345,s448,s428,s450]) ).
cnf(s452,plain,
$false,
inference(rat,[],[s343,s425,s448,s451,s450]) ).
fof(f3021,plain,
$false,
inference(avatar_sat_refutation,[],[s452]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC298-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n018.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 08:59:12 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.21 Running first-order theorem proving
% 0.07/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.63/1.35 % (3237689)Input is clausal, will run a generic CNF schedule.
% 4.63/1.35 % (3237694)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=516110666:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.63/1.35 % (3237696)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3198539274:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.63/1.35 % (3237698)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=115994126:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.63/1.35 % (3237700)dis-21_1_sil=8000:lcm=predicate:random_seed=379726339: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.35 % (3237695)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2248454140:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.63/1.35 % (3237697)lrs+10_1_sil=8000:sp=occurrence:random_seed=1572022013:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.63/1.35 % (3237699)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2242925428:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.63/1.35 % (3237700)Instruction limit reached!
% 4.63/1.35 % (3237700)------------------------------
% 4.63/1.35 % (3237700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237700)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237700)Termination reason: Instruction limit
% 4.63/1.35 % (3237700)Termination phase: Saturation
% 4.63/1.35 % (3237700)Time elapsed: 0.054 s
% 4.63/1.35 % (3237700)Peak memory usage: 89 MB
% 4.63/1.35 % (3237700)Instructions burned: 118 (million)
% 4.63/1.35 % (3237697)Instruction limit reached!
% 4.63/1.35 % (3237697)------------------------------
% 4.63/1.35 % (3237697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237697)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237697)Termination reason: Instruction limit
% 4.63/1.35 % (3237697)Termination phase: Saturation
% 4.63/1.35 % (3237697)Time elapsed: 0.064 s
% 4.63/1.35 % (3237697)Peak memory usage: 90 MB
% 4.63/1.35 % (3237697)Instructions burned: 109 (million)
% 4.63/1.35 % (3237698)Instruction limit reached!
% 4.63/1.35 % (3237698)------------------------------
% 4.63/1.35 % (3237698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237698)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237698)Termination reason: Instruction limit
% 4.63/1.35 % (3237698)Termination phase: Saturation
% 4.63/1.35 % (3237698)Time elapsed: 0.069 s
% 4.63/1.35 % (3237698)Peak memory usage: 89 MB
% 4.63/1.35 % (3237698)Instructions burned: 115 (million)
% 4.63/1.35 % (3237699)Instruction limit reached!
% 4.63/1.35 % (3237699)------------------------------
% 4.63/1.35 % (3237699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237699)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237699)Termination reason: Instruction limit
% 4.63/1.35 % (3237699)Termination phase: Saturation
% 4.63/1.35 % (3237699)Time elapsed: 0.119 s
% 4.63/1.35 % (3237699)Peak memory usage: 90 MB
% 4.63/1.35 % (3237699)Instructions burned: 181 (million)
% 4.63/1.35 % (3237708)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=1355129958:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 4.63/1.35 % (3237710)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4111781610:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.63/1.35 % (3237709)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=541040010: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.35 % (3237708)First to succeed.
% 4.63/1.35 % (3237708)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3237689"
% 4.63/1.35 % (3237711)lrs+10_64_to=lpo:sil=8000:random_seed=3353532475:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 4.63/1.35 % (3237709)Instruction limit reached!
% 4.63/1.35 % (3237709)------------------------------
% 4.63/1.35 % (3237709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237709)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237709)Termination reason: Instruction limit
% 4.63/1.35 % (3237709)Termination phase: Saturation
% 4.63/1.35 % (3237709)Time elapsed: 0.098 s
% 4.63/1.35 % (3237709)Peak memory usage: 92 MB
% 4.63/1.35 % (3237709)Instructions burned: 190 (million)
% 4.63/1.35 % (3237711)Instruction limit reached!
% 4.63/1.35 % (3237711)------------------------------
% 4.63/1.35 % (3237711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237711)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237711)Termination reason: Instruction limit
% 4.63/1.35 % (3237711)Termination phase: Saturation
% 4.63/1.35 % (3237711)Time elapsed: 0.065 s
% 4.63/1.35 % (3237711)Peak memory usage: 90 MB
% 4.63/1.35 % (3237711)Instructions burned: 126 (million)
% 4.63/1.35 % (3237710)Instruction limit reached!
% 4.63/1.35 % (3237710)------------------------------
% 4.63/1.35 % (3237710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.63/1.35 % (3237710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.63/1.35 % (3237710)CaDiCaL version: 2.1.3
% 4.63/1.35 % (3237710)Termination reason: Instruction limit
% 4.63/1.35 % (3237710)Termination phase: Saturation
% 4.63/1.35 % (3237710)Time elapsed: 0.128 s
% 4.63/1.35 % (3237710)Peak memory usage: 90 MB
% 4.63/1.35 % (3237710)Instructions burned: 220 (million)
% 4.63/1.35 % (3237716)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=62663600:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 4.63/1.35 % (3237694)Also succeeded, but the first one will report.
% 4.63/1.35 % (3237717)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2694915947:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 4.63/1.35 % (3237708)Refutation found. Thanks to Tanya!
% 4.63/1.35 % SZS status Unsatisfiable for theBenchmark
% 4.63/1.35 % SZS output start Proof for theBenchmark
% See solution above
% 5.41/1.44 % (3237708)------------------------------
% 5.41/1.44 % (3237708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.44 % (3237708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.44 % (3237708)CaDiCaL version: 2.1.3
% 5.41/1.44 % (3237708)Termination reason: Refutation
% 5.41/1.44 % (3237708)Time elapsed: 0.062 s
% 5.41/1.44 % (3237708)Peak memory usage: 91 MB
% 5.41/1.44 % (3237708)Instructions burned: 93 (million)
% 5.41/1.44 % (3237708)------------------------------
% 5.41/1.44 % (3237708)------------------------------
% 5.41/1.44 % (3237689)Success in time 0.696 s
% 5.41/1.44 % Vampire exiting
%------------------------------------------------------------------------------