%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWC376-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 : n007.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:42 PM UTC 2026
% Result : Unsatisfiable 7.28s 1.53s
% Output : Refutation 8.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 46
% Syntax : Number of formulae : 227 ( 33 unt; 21 def)
% Number of atoms : 769 ( 77 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1002 ( 460 ~; 525 |; 0 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 18 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 72 ( 0 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
fof(f77,axiom,
! [X0] :
( ssList(tl(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
fof(f78,axiom,
! [X0] :
( ssItem(hd(X0))
| ~ ssList(X0)
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
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(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f102,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause104) ).
fof(f118,axiom,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f149,axiom,
! [X2,X0,X1] :
( X0 != X1
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0)
| memberP(cons(X1,X2),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause138) ).
fof(f150,axiom,
! [X2,X0,X1] :
( memberP(cons(X2,X0),X1)
| ~ ssList(X0)
| ~ ssItem(X2)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause139) ).
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(f152,axiom,
! [X2,X0,X1] :
( memberP(app(X2,X0),X1)
| ~ ssList(X0)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ memberP(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause141) ).
fof(f170,axiom,
! [X2,X0,X1] :
( ~ memberP(app(X0,X1),X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ ssItem(X2)
| memberP(X1,X2)
| memberP(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause158) ).
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(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_4) ).
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(f206,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
( memberP(sk2,sk5)
| memberP(sk1,sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
( ~ memberP(sk2,sk5)
| ~ memberP(sk1,sk5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_9) ).
fof(f209,negated_conjecture,
( nil = sk3
| nil != sk4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_10) ).
fof(f210,negated_conjecture,
( ~ neq(sk4,nil)
| neq(sk3,nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_11) ).
fof(f211,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ neq(sk4,nil)
| ~ ssList(X0)
| sk4 = X0
| ~ ssList(X1)
| ~ ssList(X2)
| tl(sk3) != X1
| app(X1,X2) != X0
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1_12) ).
fof(f214,plain,
( memberP(sk4,sk5)
| memberP(sk3,sk5) ),
inference(definition_unfolding,[],[f207,f204,f205]) ).
fof(f215,plain,
( ~ memberP(sk4,sk5)
| ~ memberP(sk3,sk5) ),
inference(definition_unfolding,[],[f208,f204,f205]) ).
fof(f222,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f118]) ).
fof(f225,plain,
! [X2,X1] :
( ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1)
| memberP(cons(X1,X2),X1) ),
inference(equality_resolution,[],[f149]) ).
fof(f240,plain,
! [X2,X3,X0] :
( ~ neq(sk4,nil)
| ~ ssList(X0)
| sk4 = X0
| ~ ssList(tl(sk3))
| ~ ssList(X2)
| app(tl(sk3),X2) != X0
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f211]) ).
fof(f241,plain,
! [X2,X3] :
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),X2))
| sk4 = app(tl(sk3),X2)
| ~ ssList(tl(sk3))
| ~ ssList(X2)
| ~ ssItem(X3)
| cons(X3,nil) != X2
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f240]) ).
fof(f242,plain,
! [X3] :
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),cons(X3,nil)))
| sk4 = app(tl(sk3),cons(X3,nil))
| ~ ssList(tl(sk3))
| ~ ssList(cons(X3,nil))
| ~ ssItem(X3)
| hd(sk3) != X3
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f241]) ).
fof(f243,plain,
( ~ neq(sk4,nil)
| ~ ssList(app(tl(sk3),cons(hd(sk3),nil)))
| sk4 = app(tl(sk3),cons(hd(sk3),nil))
| ~ ssList(tl(sk3))
| ~ ssList(cons(hd(sk3),nil))
| ~ ssItem(hd(sk3))
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(equality_resolution,[],[f242]) ).
fof(f244,definition,
sF0 = tl(sk3),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f245,plain,
tl(sk3) = sF0,
inference(reorient_equations,[],[f244]) ).
fof(f246,definition,
sF1 = hd(sk3),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f247,plain,
hd(sk3) = sF1,
inference(reorient_equations,[],[f246]) ).
fof(f248,definition,
sF2 = cons(sF1,nil),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f249,plain,
cons(sF1,nil) = sF2,
inference(reorient_equations,[],[f248]) ).
fof(f250,definition,
sF3 = app(sF0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f251,plain,
app(sF0,sF2) = sF3,
inference(reorient_equations,[],[f250]) ).
fof(f252,plain,
( ~ neq(sk4,nil)
| ~ ssList(sF3)
| sk4 = sF3
| ~ ssList(sF0)
| ~ ssList(sF2)
| ~ ssItem(sF1)
| ~ neq(nil,sk3)
| ~ neq(nil,sk3) ),
inference(definition_folding,[],[f243,f247,f249,f247,f245,f251,f249,f247,f245,f251,f249,f247,f245]) ).
fof(f253,plain,
( ~ neq(sk4,nil)
| ~ ssList(sF3)
| sk4 = sF3
| ~ ssList(sF0)
| ~ ssList(sF2)
| ~ ssItem(sF1)
| ~ neq(nil,sk3) ),
inference(duplicate_literal_removal,[],[f252]) ).
fof(f256,plain,
! [X2,X1] :
( memberP(cons(X1,X2),X1)
| ~ ssItem(X1)
| ~ ssList(X2) ),
inference(duplicate_literal_removal,[],[f225]) ).
fof(f258,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1) ),
inference(duplicate_literal_removal,[],[f222]) ).
fof(f261,definition,
( spl4_1
<=> neq(nil,sk3) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f263,plain,
( ~ neq(nil,sk3)
| spl4_1 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl4_2
<=> ssItem(sF1) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f266,plain,
( ssItem(sF1)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f267,plain,
( ~ ssItem(sF1)
| spl4_2 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f269,definition,
( spl4_3
<=> ssList(sF2) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
fof(f270,plain,
( ssList(sF2)
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f271,plain,
( ~ ssList(sF2)
| spl4_3 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl4_4
<=> ssList(sF0) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
fof(f274,plain,
( ssList(sF0)
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,definition,
( spl4_5
<=> sk4 = sF3 ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
fof(f279,plain,
( sk4 = sF3
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f281,definition,
( spl4_6
<=> ssList(sF3) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f285,definition,
( spl4_7
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl4_7])],[avatar_definition]) ).
fof(f287,plain,
( ~ neq(sk4,nil)
| spl4_7 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f288,plain,
( ~ spl4_1
| ~ spl4_2
| ~ spl4_3
| ~ spl4_4
| spl4_5
| ~ spl4_6
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f253,f285,f281,f277,f273,f269,f265,f261]) ).
fof(f290,definition,
( spl4_8
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f292,plain,
( neq(sk3,nil)
| ~ spl4_8 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,plain,
( spl4_8
| ~ spl4_7 ),
inference(avatar_split_clause,[],[f210,f285,f290]) ).
fof(f295,definition,
( spl4_9
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f296,plain,
( nil = sk4
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl4_10
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f300,plain,
( nil != sk3
| spl4_10 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( nil = sk3
| ~ spl4_10 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f302,plain,
( ~ spl4_9
| spl4_10 ),
inference(avatar_split_clause,[],[f209,f299,f295]) ).
fof(f304,definition,
( spl4_11
<=> memberP(sk3,sk5) ),
introduced(definition,[new_symbols(definition,[spl4_11])],[avatar_definition]) ).
fof(f305,plain,
( memberP(sk3,sk5)
| ~ spl4_11 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f306,plain,
( ~ memberP(sk3,sk5)
| spl4_11 ),
inference(avatar_component_clause,[],[f304]) ).
fof(f308,definition,
( spl4_12
<=> memberP(sk4,sk5) ),
introduced(definition,[new_symbols(definition,[spl4_12])],[avatar_definition]) ).
fof(f309,plain,
( memberP(sk4,sk5)
| ~ spl4_12 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( ~ memberP(sk4,sk5)
| spl4_12 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f311,plain,
( ~ spl4_11
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f215,f308,f304]) ).
fof(f312,plain,
( spl4_11
| spl4_12 ),
inference(avatar_split_clause,[],[f214,f308,f304]) ).
fof(f318,definition,
( spl4_14
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl4_14])],[avatar_definition]) ).
fof(f319,plain,
( ssList(nil)
| ~ spl4_14 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f354,plain,
spl4_14,
inference(avatar_split_clause,[],[f8,f318]) ).
fof(f355,plain,
! [X0] :
( memberP(sF3,X0)
| ~ ssList(sF2)
| ~ ssList(sF0)
| ~ ssItem(X0)
| ~ memberP(sF0,X0) ),
inference(superposition,[],[f151,f251]) ).
fof(f361,plain,
! [X0] :
( memberP(sF3,X0)
| ~ ssList(sF2)
| ~ ssList(sF0)
| ~ ssItem(X0)
| ~ memberP(sF2,X0) ),
inference(superposition,[],[f152,f251]) ).
fof(f362,plain,
! [X0] :
( ~ memberP(sF2,X0)
| ~ ssList(nil)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| memberP(nil,X0)
| sF1 = X0 ),
inference(superposition,[],[f174,f249]) ).
fof(f363,plain,
( ! [X0] :
( ~ memberP(sF2,X0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| memberP(nil,X0)
| sF1 = X0 )
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f362,f319]) ).
fof(f371,plain,
! [X0] :
( ~ memberP(sF3,X0)
| ~ ssList(sF2)
| ~ ssList(sF0)
| ~ ssItem(X0)
| memberP(sF2,X0)
| memberP(sF0,X0) ),
inference(superposition,[],[f170,f251]) ).
fof(f374,plain,
( ~ ssList(sk4)
| ~ ssList(nil)
| nil = sk4
| spl4_7 ),
inference(resolution,[],[f102,f287]) ).
fof(f375,plain,
( ~ ssList(nil)
| nil = sk4
| spl4_7 ),
inference(forward_subsumption_resolution,[],[f374,f203]) ).
fof(f376,plain,
( nil = sk4
| spl4_7
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f375,f319]) ).
fof(f379,plain,
( ssList(sF2)
| ~ ssList(nil)
| ~ ssItem(sF1) ),
inference(superposition,[],[f86,f249]) ).
fof(f380,plain,
( ~ ssList(nil)
| ~ ssItem(sF1)
| spl4_3 ),
inference(forward_subsumption_resolution,[],[f379,f271]) ).
fof(f381,plain,
( ~ ssItem(sF1)
| spl4_3
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f380,f319]) ).
fof(f384,plain,
( ! [X0] :
( ~ memberP(sF2,X0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| sF1 = X0 )
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f363,f71]) ).
fof(f385,plain,
( ~ spl4_2
| spl4_3
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f381,f318,f269,f265]) ).
fof(f387,definition,
( spl4_23
<=> ! [X0] :
( ~ memberP(sF2,X0)
| sF1 = X0
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_23])],[avatar_definition]) ).
fof(f388,plain,
( ! [X0] :
( ~ memberP(sF2,X0)
| sF1 = X0
| ~ ssItem(X0) )
| ~ spl4_23 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( ~ spl4_2
| spl4_23
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f384,f318,f387,f265]) ).
fof(f390,plain,
( ssList(sF0)
| ~ ssList(sk3)
| nil = sk3 ),
inference(superposition,[],[f77,f245]) ).
fof(f391,plain,
( ssList(sF0)
| nil = sk3 ),
inference(forward_subsumption_resolution,[],[f390,f202]) ).
fof(f392,plain,
( spl4_10
| spl4_4 ),
inference(avatar_split_clause,[],[f391,f273,f299]) ).
fof(f396,plain,
( memberP(nil,sk5)
| ~ spl4_10
| ~ spl4_11 ),
inference(superposition,[],[f305,f301]) ).
fof(f400,plain,
( ~ ssItem(sk5)
| ~ spl4_10
| ~ spl4_11 ),
inference(resolution,[],[f71,f396]) ).
fof(f401,plain,
( $false
| ~ spl4_10
| ~ spl4_11 ),
inference(forward_subsumption_resolution,[],[f400,f206]) ).
fof(f402,plain,
( ~ spl4_10
| ~ spl4_11 ),
inference(avatar_contradiction_clause,[],[f401]) ).
fof(f403,plain,
( ~ memberP(nil,sk5)
| ~ spl4_10
| spl4_11 ),
inference(forward_demodulation,[],[f306,f301]) ).
fof(f406,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| nil = sk3 ),
inference(resolution,[],[f107,f202]) ).
fof(f415,plain,
( neq(nil,nil)
| ~ spl4_8
| ~ spl4_10 ),
inference(superposition,[],[f292,f301]) ).
fof(f417,plain,
( ssList(sF3)
| ~ ssList(sF0)
| ~ ssList(sF2) ),
inference(superposition,[],[f85,f251]) ).
fof(f432,plain,
( ssItem(sF1)
| ~ ssList(sk3)
| nil = sk3 ),
inference(superposition,[],[f78,f247]) ).
fof(f435,plain,
( ~ ssList(nil)
| ~ spl4_8
| ~ spl4_10 ),
inference(resolution,[],[f258,f415]) ).
fof(f437,plain,
( $false
| ~ spl4_8
| ~ spl4_10
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f435,f319]) ).
fof(f438,plain,
( ~ spl4_8
| ~ spl4_10
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[],[f437]) ).
fof(f440,plain,
( ~ ssList(sk3)
| nil = sk3
| spl4_2 ),
inference(forward_subsumption_resolution,[],[f432,f267]) ).
fof(f442,plain,
( nil = sk3
| spl4_2 ),
inference(forward_subsumption_resolution,[],[f440,f202]) ).
fof(f444,plain,
( $false
| spl4_2
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f442,f300]) ).
fof(f445,plain,
( spl4_2
| spl4_10 ),
inference(avatar_contradiction_clause,[],[f444]) ).
fof(f446,plain,
( ! [X0] :
( memberP(sF3,X0)
| ~ ssList(sF0)
| ~ ssItem(X0)
| ~ memberP(sF2,X0) )
| ~ spl4_3 ),
inference(forward_subsumption_resolution,[],[f361,f270]) ).
fof(f447,plain,
( ! [X0] :
( ~ memberP(sF3,X0)
| ~ ssList(sF0)
| ~ ssItem(X0)
| memberP(sF2,X0)
| memberP(sF0,X0) )
| ~ spl4_3 ),
inference(forward_subsumption_resolution,[],[f371,f270]) ).
fof(f448,plain,
( ! [X0] :
( memberP(sF3,X0)
| ~ ssList(sF0)
| ~ ssItem(X0)
| ~ memberP(sF0,X0) )
| ~ spl4_3 ),
inference(forward_subsumption_resolution,[],[f355,f270]) ).
fof(f449,plain,
( ssList(sF3)
| ~ ssList(sF2)
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f417,f274]) ).
fof(f453,plain,
( ! [X0] :
( ~ memberP(sF2,X0)
| ~ ssItem(X0)
| memberP(sF3,X0) )
| ~ spl4_3
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f446,f274]) ).
fof(f454,plain,
( ! [X0] :
( ~ memberP(sF3,X0)
| ~ ssItem(X0)
| memberP(sF2,X0)
| memberP(sF0,X0) )
| ~ spl4_3
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f447,f274]) ).
fof(f455,plain,
( ! [X0] :
( ~ memberP(sF0,X0)
| ~ ssItem(X0)
| memberP(sF3,X0) )
| ~ spl4_3
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f448,f274]) ).
fof(f456,plain,
( ssList(sF3)
| ~ spl4_3
| ~ spl4_4 ),
inference(forward_subsumption_resolution,[],[f449,f270]) ).
fof(f460,plain,
( spl4_6
| ~ spl4_3
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f456,f273,f269,f281]) ).
fof(f461,plain,
( ~ ssList(nil)
| ~ ssList(sk3)
| nil = sk3
| spl4_1 ),
inference(resolution,[],[f263,f102]) ).
fof(f462,plain,
( ~ ssList(sk3)
| nil = sk3
| spl4_1
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f461,f319]) ).
fof(f463,plain,
( nil = sk3
| spl4_1
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f462,f202]) ).
fof(f464,plain,
( $false
| spl4_1
| spl4_10
| ~ spl4_14 ),
inference(forward_subsumption_resolution,[],[f463,f300]) ).
fof(f465,plain,
( spl4_1
| spl4_10
| ~ spl4_14 ),
inference(avatar_contradiction_clause,[],[f464]) ).
fof(f466,plain,
( spl4_9
| spl4_7
| ~ spl4_14 ),
inference(avatar_split_clause,[],[f376,f318,f285,f295]) ).
fof(f474,plain,
( memberP(nil,sk5)
| ~ spl4_9
| ~ spl4_12 ),
inference(superposition,[],[f309,f296]) ).
fof(f476,plain,
( $false
| ~ spl4_9
| ~ spl4_10
| spl4_11
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f474,f403]) ).
fof(f477,plain,
( ~ spl4_9
| ~ spl4_10
| spl4_11
| ~ spl4_12 ),
inference(avatar_contradiction_clause,[],[f476]) ).
fof(f478,plain,
( sk3 = cons(hd(sk3),tl(sk3))
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f406,f300]) ).
fof(f480,plain,
( sk3 = cons(hd(sk3),sF0)
| spl4_10 ),
inference(forward_demodulation,[],[f478,f245]) ).
fof(f481,plain,
( sk3 = cons(sF1,sF0)
| spl4_10 ),
inference(forward_demodulation,[],[f480,f247]) ).
fof(f484,plain,
( memberP(sk3,sF1)
| ~ ssItem(sF1)
| ~ ssList(sF0)
| spl4_10 ),
inference(superposition,[],[f256,f481]) ).
fof(f486,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssList(sF0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| ~ memberP(sF0,X0) )
| spl4_10 ),
inference(superposition,[],[f150,f481]) ).
fof(f487,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssList(sF0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| memberP(sF0,X0)
| sF1 = X0 )
| spl4_10 ),
inference(superposition,[],[f174,f481]) ).
fof(f488,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| memberP(sF0,X0)
| sF1 = X0 )
| ~ spl4_4
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f487,f274]) ).
fof(f489,plain,
( ! [X0] :
( memberP(sk3,X0)
| ~ ssItem(sF1)
| ~ ssItem(X0)
| ~ memberP(sF0,X0) )
| ~ spl4_4
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f486,f274]) ).
fof(f490,plain,
( memberP(sk3,sF1)
| ~ ssList(sF0)
| ~ spl4_2
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f484,f266]) ).
fof(f492,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ~ ssItem(X0)
| memberP(sF0,X0)
| sF1 = X0 )
| ~ spl4_2
| ~ spl4_4
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f488,f266]) ).
fof(f493,plain,
( ! [X0] :
( ~ memberP(sF0,X0)
| ~ ssItem(X0)
| memberP(sk3,X0) )
| ~ spl4_2
| ~ spl4_4
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f489,f266]) ).
fof(f494,plain,
( memberP(sk3,sF1)
| ~ spl4_2
| ~ spl4_4
| spl4_10 ),
inference(forward_subsumption_resolution,[],[f490,f274]) ).
fof(f513,plain,
( ! [X0] :
( ~ memberP(sk4,X0)
| ~ ssItem(X0)
| memberP(sF2,X0)
| memberP(sF0,X0) )
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5 ),
inference(superposition,[],[f454,f279]) ).
fof(f514,plain,
( ~ ssItem(sk5)
| memberP(sF2,sk5)
| memberP(sF0,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_12 ),
inference(resolution,[],[f513,f309]) ).
fof(f515,plain,
( memberP(sF2,sk5)
| memberP(sF0,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_12 ),
inference(forward_subsumption_resolution,[],[f514,f206]) ).
fof(f517,definition,
( spl4_26
<=> memberP(sF0,sk5) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f519,plain,
( memberP(sF0,sk5)
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f521,definition,
( spl4_27
<=> memberP(sF2,sk5) ),
introduced(definition,[new_symbols(definition,[spl4_27])],[avatar_definition]) ).
fof(f522,plain,
( ~ memberP(sF2,sk5)
| spl4_27 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( memberP(sF2,sk5)
| ~ spl4_27 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f524,plain,
( spl4_26
| spl4_27
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_12 ),
inference(avatar_split_clause,[],[f515,f308,f277,f273,f269,f521,f517]) ).
fof(f525,plain,
( sk5 = sF1
| ~ ssItem(sk5)
| ~ spl4_23
| ~ spl4_27 ),
inference(resolution,[],[f523,f388]) ).
fof(f526,plain,
( ~ ssItem(sk5)
| memberP(sF3,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_27 ),
inference(resolution,[],[f523,f453]) ).
fof(f527,plain,
( memberP(sF3,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f526,f206]) ).
fof(f528,plain,
( sk5 = sF1
| ~ spl4_23
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f525,f206]) ).
fof(f530,plain,
( memberP(sk3,sk5)
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_23
| ~ spl4_27 ),
inference(superposition,[],[f494,f528]) ).
fof(f534,plain,
( $false
| ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_23
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f530,f306]) ).
fof(f535,plain,
( ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_23
| ~ spl4_27 ),
inference(avatar_contradiction_clause,[],[f534]) ).
fof(f536,plain,
( ~ ssItem(sk5)
| memberP(sk3,sk5)
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_26 ),
inference(resolution,[],[f519,f493]) ).
fof(f537,plain,
( ~ ssItem(sk5)
| memberP(sF3,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_26 ),
inference(resolution,[],[f519,f455]) ).
fof(f538,plain,
( memberP(sF3,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f537,f206]) ).
fof(f539,plain,
( memberP(sk3,sk5)
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f536,f206]) ).
fof(f541,plain,
( $false
| ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f539,f306]) ).
fof(f542,plain,
( ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f541]) ).
fof(f543,plain,
( ~ ssItem(sk5)
| memberP(sF0,sk5)
| sk5 = sF1
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_11 ),
inference(resolution,[],[f305,f492]) ).
fof(f544,plain,
( memberP(sF0,sk5)
| sk5 = sF1
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_11 ),
inference(forward_subsumption_resolution,[],[f543,f206]) ).
fof(f546,definition,
( spl4_28
<=> sk5 = sF1 ),
introduced(definition,[new_symbols(definition,[spl4_28])],[avatar_definition]) ).
fof(f548,plain,
( sk5 = sF1
| ~ spl4_28 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f549,plain,
( spl4_28
| spl4_26
| ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_11 ),
inference(avatar_split_clause,[],[f544,f304,f299,f273,f265,f517,f546]) ).
fof(f553,plain,
( sF2 = cons(sk5,nil)
| ~ spl4_28 ),
inference(superposition,[],[f249,f548]) ).
fof(f556,plain,
( memberP(sF2,sk5)
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ spl4_28 ),
inference(superposition,[],[f256,f553]) ).
fof(f561,plain,
( ~ ssItem(sk5)
| ~ ssList(nil)
| spl4_27
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f556,f522]) ).
fof(f564,plain,
( ~ ssList(nil)
| spl4_27
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f561,f206]) ).
fof(f567,plain,
( $false
| ~ spl4_14
| spl4_27
| ~ spl4_28 ),
inference(forward_subsumption_resolution,[],[f564,f319]) ).
fof(f568,plain,
( ~ spl4_14
| spl4_27
| ~ spl4_28 ),
inference(avatar_contradiction_clause,[],[f567]) ).
fof(f569,plain,
( memberP(sk4,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_27 ),
inference(forward_demodulation,[],[f527,f279]) ).
fof(f572,plain,
( $false
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_27 ),
inference(forward_subsumption_resolution,[],[f569,f310]) ).
fof(f573,plain,
( ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_27 ),
inference(avatar_contradiction_clause,[],[f572]) ).
fof(f576,plain,
( memberP(sk4,sk5)
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_26 ),
inference(forward_demodulation,[],[f538,f279]) ).
fof(f577,plain,
( $false
| ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f576,f310]) ).
fof(f578,plain,
( ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_26 ),
inference(avatar_contradiction_clause,[],[f577]) ).
cnf(s1,plain,
( ~ spl4_1
| ~ spl4_2
| ~ spl4_3
| ~ spl4_4
| spl4_5
| ~ spl4_6
| ~ spl4_7 ),
inference(sat_conversion,[],[f288]) ).
cnf(s2,plain,
( ~ spl4_7
| spl4_8 ),
inference(sat_conversion,[],[f293]) ).
cnf(s3,plain,
( ~ spl4_9
| spl4_10 ),
inference(sat_conversion,[],[f302]) ).
cnf(s4,plain,
( ~ spl4_11
| ~ spl4_12 ),
inference(sat_conversion,[],[f311]) ).
cnf(s5,plain,
( spl4_11
| spl4_12 ),
inference(sat_conversion,[],[f312]) ).
cnf(s15,plain,
spl4_14,
inference(sat_conversion,[],[f354]) ).
cnf(s19,plain,
( ~ spl4_2
| spl4_3
| ~ spl4_14 ),
inference(sat_conversion,[],[f385]) ).
cnf(s20,plain,
( ~ spl4_2
| ~ spl4_14
| spl4_23 ),
inference(sat_conversion,[],[f389]) ).
cnf(s21,plain,
( spl4_4
| spl4_10 ),
inference(sat_conversion,[],[f392]) ).
cnf(s22,plain,
( ~ spl4_10
| ~ spl4_11 ),
inference(sat_conversion,[],[f402]) ).
cnf(s23,plain,
( ~ spl4_8
| ~ spl4_10
| ~ spl4_14 ),
inference(sat_conversion,[],[f438]) ).
cnf(s24,plain,
( spl4_2
| spl4_10 ),
inference(sat_conversion,[],[f445]) ).
cnf(s25,plain,
( ~ spl4_3
| ~ spl4_4
| spl4_6 ),
inference(sat_conversion,[],[f460]) ).
cnf(s26,plain,
( spl4_1
| spl4_10
| ~ spl4_14 ),
inference(sat_conversion,[],[f465]) ).
cnf(s27,plain,
( spl4_7
| spl4_9
| ~ spl4_14 ),
inference(sat_conversion,[],[f466]) ).
cnf(s28,plain,
( ~ spl4_9
| ~ spl4_10
| spl4_11
| ~ spl4_12 ),
inference(sat_conversion,[],[f477]) ).
cnf(s30,plain,
( ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| ~ spl4_12
| spl4_26
| spl4_27 ),
inference(sat_conversion,[],[f524]) ).
cnf(s31,plain,
( ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_23
| ~ spl4_27 ),
inference(sat_conversion,[],[f535]) ).
cnf(s32,plain,
( ~ spl4_2
| ~ spl4_4
| spl4_10
| spl4_11
| ~ spl4_26 ),
inference(sat_conversion,[],[f542]) ).
cnf(s33,plain,
( ~ spl4_2
| ~ spl4_4
| spl4_10
| ~ spl4_11
| spl4_26
| spl4_28 ),
inference(sat_conversion,[],[f549]) ).
cnf(s34,plain,
( ~ spl4_14
| spl4_27
| ~ spl4_28 ),
inference(sat_conversion,[],[f568]) ).
cnf(s36,plain,
( ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_27 ),
inference(sat_conversion,[],[f573]) ).
cnf(s38,plain,
( ~ spl4_3
| ~ spl4_4
| ~ spl4_5
| spl4_12
| ~ spl4_26 ),
inference(sat_conversion,[],[f578]) ).
cnf(s43,plain,
~ spl4_10,
inference(rat,[],[s28,s27,s5,s2,s22,s23,s15]) ).
cnf(s44,plain,
spl4_1,
inference(rat,[],[s26,s15,s43]) ).
cnf(s45,plain,
spl4_2,
inference(rat,[],[s24,s43]) ).
cnf(s46,plain,
spl4_4,
inference(rat,[],[s21,s43]) ).
cnf(s47,plain,
~ spl4_9,
inference(rat,[],[s3,s43]) ).
cnf(s48,plain,
spl4_23,
inference(rat,[],[s20,s15,s45]) ).
cnf(s49,plain,
spl4_3,
inference(rat,[],[s19,s15,s45]) ).
cnf(s50,plain,
spl4_6,
inference(rat,[],[s25,s49,s46]) ).
cnf(s51,plain,
spl4_7,
inference(rat,[],[s27,s15,s47]) ).
cnf(s53,plain,
spl4_5,
inference(rat,[],[s1,s46,s50,s49,s45,s44,s51]) ).
cnf(s54,plain,
spl4_11,
inference(rat,[],[s30,s32,s31,s5,s49,s46,s53,s43,s45,s48]) ).
cnf(s55,plain,
~ spl4_12,
inference(rat,[],[s4,s54]) ).
cnf(s56,plain,
~ spl4_26,
inference(rat,[],[s38,s53,s46,s49,s55]) ).
cnf(s57,plain,
~ spl4_27,
inference(rat,[],[s36,s53,s46,s49,s55]) ).
cnf(s58,plain,
spl4_28,
inference(rat,[],[s33,s54,s43,s46,s45,s56]) ).
cnf(s59,plain,
$false,
inference(rat,[],[s34,s15,s58,s57]) ).
fof(f579,plain,
$false,
inference(avatar_sat_refutation,[],[s59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC376-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.06/0.18 % Computer : n007.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 09:19:25 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/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
% 7.28/1.53 % (2260589)Input is clausal, will run a generic CNF schedule.
% 7.28/1.53 % (2260599)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1855891104:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 7.28/1.53 % (2260596)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=274905149:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 7.28/1.53 % (2260598)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4113641329:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 7.28/1.53 % (2260597)lrs+10_1_sil=8000:sp=occurrence:random_seed=1433255779:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 7.28/1.53 % (2260594)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=2194255283:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 7.28/1.53 % (2260600)dis-21_1_sil=8000:lcm=predicate:random_seed=1980448126: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)
% 7.28/1.53 % (2260595)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2067636408:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 7.28/1.53 % (2260599)Instruction limit reached!
% 7.28/1.53 % (2260599)------------------------------
% 7.28/1.53 % (2260599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260599)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260599)Termination reason: Instruction limit
% 7.28/1.53 % (2260599)Termination phase: Saturation
% 7.28/1.53 % (2260599)Time elapsed: 0.065 s
% 7.28/1.53 % (2260599)Peak memory usage: 90 MB
% 7.28/1.53 % (2260599)Instructions burned: 181 (million)
% 7.28/1.53 % (2260600)Instruction limit reached!
% 7.28/1.53 % (2260600)------------------------------
% 7.28/1.53 % (2260600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260600)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260600)Termination reason: Instruction limit
% 7.28/1.53 % (2260600)Termination phase: Saturation
% 7.28/1.53 % (2260600)Time elapsed: 0.065 s
% 7.28/1.53 % (2260600)Peak memory usage: 89 MB
% 7.28/1.53 % (2260600)Instructions burned: 118 (million)
% 7.28/1.53 % (2260598)Instruction limit reached!
% 7.28/1.53 % (2260598)------------------------------
% 7.28/1.53 % (2260598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260598)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260598)Termination reason: Instruction limit
% 7.28/1.53 % (2260598)Termination phase: Saturation
% 7.28/1.53 % (2260598)Time elapsed: 0.066 s
% 7.28/1.53 % (2260598)Peak memory usage: 89 MB
% 7.28/1.53 % (2260598)Instructions burned: 115 (million)
% 7.28/1.53 % (2260597)Instruction limit reached!
% 7.28/1.53 % (2260597)------------------------------
% 7.28/1.53 % (2260597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260597)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260597)Termination reason: Instruction limit
% 7.28/1.53 % (2260597)Termination phase: Saturation
% 7.28/1.53 % (2260597)Time elapsed: 0.067 s
% 7.28/1.53 % (2260597)Peak memory usage: 89 MB
% 7.28/1.53 % (2260597)Instructions burned: 108 (million)
% 7.28/1.53 % (2260608)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=2779448109:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 7.28/1.53 % (2260608)Instruction limit reached!
% 7.28/1.53 % (2260608)------------------------------
% 7.28/1.53 % (2260608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260608)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260608)Termination reason: Instruction limit
% 7.28/1.53 % (2260608)Termination phase: Saturation
% 7.28/1.53 % (2260608)Time elapsed: 0.050 s
% 7.28/1.53 % (2260608)Peak memory usage: 90 MB
% 7.28/1.53 % (2260608)Instructions burned: 145 (million)
% 7.28/1.53 % (2260609)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2075267960: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)
% 7.28/1.53 % (2260610)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=776960143:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 7.28/1.53 % (2260611)lrs+10_64_to=lpo:sil=8000:random_seed=1233937068:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 7.28/1.53 % (2260610)Refutation not found, incomplete strategy
% 7.28/1.53 % (2260610)------------------------------
% 7.28/1.53 % (2260610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260610)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260610)Termination reason: Refutation not found, incomplete strategy
% 7.28/1.53 % (2260610)Time elapsed: 0.007 s
% 7.28/1.53 % (2260610)Peak memory usage: 88 MB
% 7.28/1.53 % (2260610)Instructions burned: 9 (million)
% 7.28/1.53 % (2260611)Instruction limit reached!
% 7.28/1.53 % (2260611)------------------------------
% 7.28/1.53 % (2260611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260611)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260611)Termination reason: Instruction limit
% 7.28/1.53 % (2260611)Termination phase: Saturation
% 7.28/1.53 % (2260611)Time elapsed: 0.068 s
% 7.28/1.53 % (2260611)Peak memory usage: 90 MB
% 7.28/1.53 % (2260611)Instructions burned: 127 (million)
% 7.28/1.53 % (2260609)Instruction limit reached!
% 7.28/1.53 % (2260609)------------------------------
% 7.28/1.53 % (2260609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260609)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260609)Termination reason: Instruction limit
% 7.28/1.53 % (2260609)Termination phase: Saturation
% 7.28/1.53 % (2260609)Time elapsed: 0.101 s
% 7.28/1.53 % (2260609)Peak memory usage: 91 MB
% 7.28/1.53 % (2260609)Instructions burned: 189 (million)
% 7.28/1.53 % (2260613)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2335351308:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 7.28/1.53 % (2260613)Instruction limit reached!
% 7.28/1.53 % (2260613)------------------------------
% 7.28/1.53 % (2260613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260613)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260613)Termination reason: Instruction limit
% 7.28/1.53 % (2260613)Termination phase: Saturation
% 7.28/1.53 % (2260613)Time elapsed: 0.064 s
% 7.28/1.53 % (2260613)Peak memory usage: 90 MB
% 7.28/1.53 % (2260613)Instructions burned: 197 (million)
% 7.28/1.53 % (2260617)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4260712162:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 7.28/1.53 % (2260610)------------------------------
% 7.28/1.53 % (2260610)------------------------------
% 7.28/1.53 % (2260618)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3089583008:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 7.28/1.53 % (2260620)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1723438425:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 7.28/1.53 % (2260617)Instruction limit reached!
% 7.28/1.53 % (2260617)------------------------------
% 7.28/1.53 % (2260617)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260617)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260617)Termination reason: Instruction limit
% 7.28/1.53 % (2260617)Termination phase: Saturation
% 7.28/1.53 % (2260617)Time elapsed: 0.096 s
% 7.28/1.53 % (2260617)Peak memory usage: 91 MB
% 7.28/1.53 % (2260617)Instructions burned: 157 (million)
% 7.28/1.53 % (2260620)Instruction limit reached!
% 7.28/1.53 % (2260620)------------------------------
% 7.28/1.53 % (2260620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260620)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260620)Termination reason: Instruction limit
% 7.28/1.53 % (2260620)Termination phase: Saturation
% 7.28/1.53 % (2260620)Time elapsed: 0.033 s
% 7.28/1.53 % (2260620)Peak memory usage: 90 MB
% 7.28/1.53 % (2260620)Instructions burned: 113 (million)
% 7.28/1.53 % (2260622)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=832706042:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 7.28/1.53 % (2260594)First to succeed.
% 7.28/1.53 % (2260594)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2260589"
% 7.28/1.53 % (2260626)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3660503920:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 7.28/1.53 % (2260625)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3450140088:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 7.28/1.53 % (2260596)Also succeeded, but the first one will report.
% 7.28/1.53 % (2260622)Instruction limit reached!
% 7.28/1.53 % (2260622)------------------------------
% 7.28/1.53 % (2260622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260622)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260622)Termination reason: Instruction limit
% 7.28/1.53 % (2260622)Termination phase: Saturation
% 7.28/1.53 % (2260622)Time elapsed: 0.070 s
% 7.28/1.53 % (2260622)Peak memory usage: 90 MB
% 7.28/1.53 % (2260622)Instructions burned: 108 (million)
% 7.28/1.53 % (2260625)Instruction limit reached!
% 7.28/1.53 % (2260625)------------------------------
% 7.28/1.53 % (2260625)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.28/1.53 % (2260625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.28/1.53 % (2260625)CaDiCaL version: 2.1.3
% 7.28/1.53 % (2260625)Termination reason: Instruction limit
% 7.28/1.53 % (2260625)Termination phase: Saturation
% 7.28/1.53 % (2260625)Time elapsed: 0.156 s
% 7.28/1.53 % (2260625)Peak memory usage: 90 MB
% 7.28/1.53 % (2260625)Instructions burned: 243 (million)
% 7.28/1.53 % (2260630)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1971443810:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 7.28/1.53 % (2260594)Refutation found. Thanks to Tanya!
% 7.28/1.53 % SZS status Unsatisfiable for theBenchmark
% 7.28/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 8.28/1.72 % (2260594)------------------------------
% 8.28/1.72 % (2260594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.72 % (2260594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.72 % (2260594)CaDiCaL version: 2.1.3
% 8.28/1.72 % (2260594)Termination reason: Refutation
% 8.28/1.72 % (2260594)Time elapsed: 0.673 s
% 8.28/1.72 % (2260594)Peak memory usage: 130 MB
% 8.28/1.72 % (2260594)Instructions burned: 1003 (million)
% 8.28/1.72 % (2260594)------------------------------
% 8.28/1.72 % (2260594)------------------------------
% 8.28/1.72 % (2260589)Success in time 1.115 s
% 8.28/1.72 % Vampire exiting
%------------------------------------------------------------------------------