%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC409-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:55 PM UTC 2026
% Result : Unsatisfiable 95.99s 18.17s
% Output : Refutation 95.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 41
% Syntax : Number of formulae : 187 ( 38 unt; 14 def)
% Number of atoms : 535 ( 81 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 583 ( 235 ~; 334 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 15 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-2 aty)
% Number of variables : 147 ( 0 sgn 147 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
fof(f13,axiom,
! [X0] : ssList(skaf82(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause13) ).
fof(f52,axiom,
! [X0,X1] : ssList(skaf43(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause52) ).
fof(f53,axiom,
! [X0,X1] : ssList(skaf42(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause53) ).
fof(f72,axiom,
! [X0,X1] :
( ~ ssList(X0)
| duplicatefreeP(X0)
| ssItem(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause72) ).
fof(f75,axiom,
! [X0] :
( ~ ssList(X0)
| ssList(tl(X0))
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause75) ).
fof(f85,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| ssList(app(X1,X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f86,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| ssList(cons(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause86) ).
fof(f96,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| tl(cons(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause96) ).
fof(f97,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| hd(cons(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause97) ).
fof(f107,axiom,
! [X0] :
( ~ ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause104) ).
fof(f112,axiom,
! [X0] :
( ~ ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause109) ).
fof(f125,axiom,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(cons(X0,nil),X1) = cons(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause120) ).
fof(f126,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(reorient_equations,[],[f125]) ).
fof(f151,axiom,
! [X2,X0,X1] :
( ~ memberP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| memberP(app(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause140) ).
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/sandbox2/benchmark/Axioms/SWC001-0.ax',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(f182,axiom,
! [X0,X1] :
( ~ memberP(X0,X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause169) ).
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/sandbox2/benchmark/Axioms/SWC001-0.ax',clause175) ).
fof(f193,axiom,
! [X2,X3,X0,X1,X4] :
( app(app(X0,cons(X1,X2)),cons(X1,X3)) != X4
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(X4)
| ~ ssList(X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause179) ).
fof(f200,negated_conjecture,
ssList(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_1) ).
fof(f201,negated_conjecture,
ssList(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_2) ).
fof(f204,negated_conjecture,
sk2 = sk4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_5) ).
fof(f205,negated_conjecture,
sk1 = sk3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_6) ).
fof(f206,negated_conjecture,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| app(X1,cons(X0,nil)) = sk3
| app(cons(X0,nil),X1) != sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,plain,
! [X0,X1] :
( ~ ssItem(X0)
| ~ ssList(X1)
| sk3 = app(X1,cons(X0,nil))
| app(cons(X0,nil),X1) != sk4 ),
inference(reorient_equations,[],[f206]) ).
fof(f208,negated_conjecture,
ssItem(sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f209,negated_conjecture,
memberP(sk2,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f210,negated_conjecture,
~ memberP(sk1,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f211,negated_conjecture,
( nil = sk3
| nil != sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f212,plain,
ssList(sk3),
inference(definition_unfolding,[],[f200,f205]) ).
fof(f213,plain,
ssList(sk4),
inference(definition_unfolding,[],[f201,f204]) ).
fof(f214,plain,
memberP(sk4,sk5),
inference(definition_unfolding,[],[f209,f204]) ).
fof(f215,plain,
~ memberP(sk3,sk5),
inference(definition_unfolding,[],[f210,f205]) ).
fof(f231,plain,
! [X2,X0,X1] :
( ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ ssList(app(X0,cons(X1,X2)))
| memberP(app(X0,cons(X1,X2)),X1) ),
inference(equality_resolution,[],[f189]) ).
fof(f233,plain,
! [X2,X3,X0,X1] :
( ~ ssList(X3)
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ~ ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(equality_resolution,[],[f193]) ).
fof(f242,plain,
~ ssList(nil),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f247,plain,
! [X0] : ~ ssList(skaf82(X0)),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f286,plain,
! [X0,X1] : ~ ssList(skaf43(X0,X1)),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f287,plain,
! [X0,X1] : ~ ssList(skaf42(X0,X1)),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f305,plain,
! [X0,X1] :
( ssList(X0)
| duplicatefreeP(X0)
| ~ ssItem(X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f308,plain,
! [X0] :
( ~ ssList(tl(X0))
| ssList(X0)
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f318,plain,
! [X0,X1] :
( ~ ssList(app(X1,X0))
| ssList(X1)
| ssList(X0) ),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f319,plain,
! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1)
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f329,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| tl(cons(X0,X1)) = X1 ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f330,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| hd(cons(X0,X1)) = X0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f337,plain,
! [X0] :
( ssList(X0)
| cons(hd(X0),tl(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f342,plain,
! [X0] :
( ssList(X0)
| cons(skaf83(X0),skaf82(X0)) = X0
| nil = X0 ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f353,plain,
! [X0,X1] :
( ssItem(X0)
| ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f373,plain,
! [X2,X0,X1] :
( ~ memberP(app(X0,X2),X1)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| memberP(X0,X1) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f394,plain,
! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X0)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f402,plain,
! [X0,X1] :
( memberP(X0,X1)
| ssItem(X1)
| ssList(X0)
| app(skaf42(X0,X1),cons(X1,skaf43(X1,X0))) = X0 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f408,plain,
! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssItem(X1)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f412,plain,
! [X2,X3,X0,X1] :
( ssList(X3)
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ~ duplicatefreeP(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(app(app(X0,cons(X1,X2)),cons(X1,X3))) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f419,plain,
~ ssList(sk3),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f420,plain,
~ ssList(sk4),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f423,plain,
! [X0,X1] :
( app(cons(X0,nil),X1) != sk4
| ssList(X1)
| sk3 = app(X1,cons(X0,nil))
| ssItem(X0) ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f424,plain,
~ ssItem(sk5),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f425,plain,
~ memberP(sk4,sk5),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f426,plain,
memberP(sk3,sk5),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f434,definition,
( spl0_1
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f435,plain,
( nil = sk4
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f436,plain,
( nil != sk4
| spl0_1 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,definition,
( spl0_2
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f440,plain,
( nil = sk3
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f211,f438,f434]) ).
fof(f447,definition,
( spl0_4
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f448,plain,
( ~ ssList(nil)
| spl0_4 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f475,definition,
( spl0_10
<=> ! [X1] : ~ ssItem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f476,plain,
( ! [X1] : ~ ssItem(X1)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f478,definition,
( spl0_11
<=> ! [X0] :
( ssList(X0)
| duplicatefreeP(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f479,plain,
( ! [X0] :
( duplicatefreeP(X0)
| ssList(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( spl0_10
| spl0_11 ),
inference(avatar_split_clause,[],[f305,f478,f475]) ).
fof(f483,plain,
~ spl0_4,
inference(avatar_split_clause,[],[f242,f447]) ).
fof(f484,plain,
( ! [X0,X1] :
( app(cons(X0,nil),X1) != sk4
| ssList(X1)
| sk3 = app(X1,cons(X0,nil)) )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f423,f476]) ).
fof(f582,plain,
( ! [X0,X1] :
( ~ ssList(cons(X0,X1))
| ssList(X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f319,f476]) ).
fof(f595,plain,
( ! [X0,X1] :
( ssList(X1)
| tl(cons(X0,X1)) = X1 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f329,f476]) ).
fof(f598,plain,
( ! [X0,X1] : skaf82(X1) = tl(cons(X0,skaf82(X1)))
| ~ spl0_10 ),
inference(resolution,[],[f595,f247]) ).
fof(f632,plain,
( ! [X0,X1] :
( ssList(X1)
| hd(cons(X0,X1)) = X0 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f330,f476]) ).
fof(f636,plain,
( ! [X0,X1] : hd(cons(X0,skaf82(X1))) = X0
| ~ spl0_10 ),
inference(resolution,[],[f632,f247]) ).
fof(f734,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| nil = sk4 ),
inference(resolution,[],[f337,f420]) ).
fof(f735,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f734,f436]) ).
fof(f774,plain,
( sk4 = cons(skaf83(sk4),skaf82(sk4))
| nil = sk4 ),
inference(resolution,[],[f342,f420]) ).
fof(f775,plain,
( sk4 = cons(skaf83(sk4),skaf82(sk4))
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f774,f436]) ).
fof(f783,plain,
( memberP(nil,sk5)
| ~ spl0_2 ),
inference(superposition,[],[f426,f440]) ).
fof(f808,definition,
( spl0_14
<=> ssList(tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f809,plain,
( ~ ssList(tl(sk4))
| spl0_14 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f810,plain,
( ssList(tl(sk4))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f823,plain,
( ! [X0,X1] :
( ssList(X1)
| cons(X0,X1) = app(cons(X0,nil),X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f353,f476]) ).
fof(f825,plain,
( ! [X0,X1] : cons(X0,skaf82(X1)) = app(cons(X0,nil),skaf82(X1))
| ~ spl0_10 ),
inference(resolution,[],[f823,f247]) ).
fof(f1122,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X0,X2),X1)
| ssList(X2)
| ssList(X0)
| memberP(X0,X1) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f373,f476]) ).
fof(f1166,plain,
( ssList(sk4)
| nil = sk4
| ~ spl0_14 ),
inference(resolution,[],[f810,f308]) ).
fof(f1167,plain,
( nil = sk4
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f1166,f420]) ).
fof(f1204,plain,
( spl0_1
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1167,f808,f434]) ).
fof(f1206,definition,
( spl0_28
<=> sk4 = cons(hd(sk4),tl(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f1208,plain,
( sk4 = cons(hd(sk4),tl(sk4))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1211,definition,
( spl0_29
<=> sk4 = cons(skaf83(sk4),skaf82(sk4)) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f1213,plain,
( sk4 = cons(skaf83(sk4),skaf82(sk4))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1220,plain,
( ~ memberP(nil,sk5)
| ~ spl0_1 ),
inference(superposition,[],[f425,f435]) ).
fof(f1231,plain,
( $false
| ~ spl0_1
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f1220,f783]) ).
fof(f1232,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(avatar_contradiction_clause,[],[f1231]) ).
fof(f1233,plain,
( spl0_28
| spl0_1 ),
inference(avatar_split_clause,[],[f735,f434,f1206]) ).
fof(f1234,plain,
( spl0_29
| spl0_1 ),
inference(avatar_split_clause,[],[f775,f434,f1211]) ).
fof(f2511,plain,
( ssItem(sk5)
| ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4))) ),
inference(resolution,[],[f402,f425]) ).
fof(f2522,plain,
( ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4))) ),
inference(forward_subsumption_resolution,[],[f2511,f424]) ).
fof(f2529,plain,
sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4))),
inference(forward_subsumption_resolution,[],[f2522,f420]) ).
fof(f2715,plain,
( ! [X2,X3,X0,X1] :
( ssList(app(app(X0,cons(X1,X2)),cons(X1,X3)))
| ssList(X2)
| ssList(X0)
| ssItem(X1)
| ssList(X3) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f412,f479]) ).
fof(f2733,definition,
( spl0_60
<=> ! [X3] : ssList(X3) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f2734,plain,
( ! [X3] : ssList(X3)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f2733]) ).
fof(f2916,plain,
( ! [X0] :
( ssList(app(sk4,cons(sk5,X0)))
| ssList(skaf43(sk5,sk4))
| ssList(skaf42(sk4,sk5))
| ssItem(sk5)
| ssList(X0) )
| ~ spl0_11 ),
inference(superposition,[],[f2715,f2529]) ).
fof(f2941,plain,
( ! [X0] :
( ssList(app(sk4,cons(sk5,X0)))
| ssList(skaf42(sk4,sk5))
| ssItem(sk5)
| ssList(X0) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2916,f286]) ).
fof(f2986,plain,
( ! [X0] :
( ssList(app(sk4,cons(sk5,X0)))
| ssItem(sk5)
| ssList(X0) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2941,f287]) ).
fof(f2991,plain,
( ! [X0] :
( ssList(app(sk4,cons(sk5,X0)))
| ssList(X0) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f2986,f424]) ).
fof(f3828,plain,
( $false
| ~ spl0_60 ),
inference(backward_subsumption_resolution,[],[f420,f2734]) ).
fof(f3860,plain,
~ spl0_60,
inference(avatar_contradiction_clause,[],[f3828]) ).
fof(f9067,plain,
( ! [X0] :
( ssList(X0)
| ssList(sk4)
| ssList(cons(sk5,X0)) )
| ~ spl0_11 ),
inference(resolution,[],[f2991,f318]) ).
fof(f9068,plain,
( ! [X0] :
( ssList(cons(sk5,X0))
| ssList(X0) )
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f9067,f420]) ).
fof(f9106,plain,
( ! [X0] :
( ssList(X0)
| ssList(X0)
| ssItem(sk5) )
| ~ spl0_11 ),
inference(resolution,[],[f9068,f319]) ).
fof(f9107,plain,
( ! [X0] :
( ssList(X0)
| ssItem(sk5) )
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f9106]) ).
fof(f9108,plain,
( ! [X0] : ssList(X0)
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f9107,f424]) ).
fof(f9111,plain,
( spl0_60
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f9108,f478,f2733]) ).
fof(f9174,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| ssItem(X2)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f394,f476]) ).
fof(f9179,plain,
( ! [X2,X0,X1] :
( ~ memberP(app(X0,cons(X1,X2)),X1)
| ssList(X0)
| ssList(app(X0,cons(X1,X2)))
| ssList(X2) )
| ~ spl0_10 ),
inference(backward_subsumption_resolution,[],[f408,f476]) ).
fof(f9256,plain,
( ! [X2,X0,X1] :
( ~ memberP(X1,X2)
| ssList(X1)
| memberP(cons(X0,X1),X2)
| X0 = X2 )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f9174,f476]) ).
fof(f10262,plain,
( hd(sk4) = skaf83(sk4)
| ~ spl0_10
| ~ spl0_29 ),
inference(superposition,[],[f636,f1213]) ).
fof(f10571,plain,
( tl(sk4) = skaf82(sk4)
| ~ spl0_10
| ~ spl0_29 ),
inference(superposition,[],[f598,f1213]) ).
fof(f17129,definition,
( spl0_247
<=> memberP(tl(sk4),sk5) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f17130,plain,
( ~ memberP(tl(sk4),sk5)
| spl0_247 ),
inference(avatar_component_clause,[],[f17129]) ).
fof(f17131,plain,
( memberP(tl(sk4),sk5)
| ~ spl0_247 ),
inference(avatar_component_clause,[],[f17129]) ).
fof(f17262,plain,
( ! [X0] :
( ssList(tl(sk4))
| memberP(cons(X0,tl(sk4)),sk5)
| sk5 = X0 )
| ~ spl0_10
| ~ spl0_247 ),
inference(resolution,[],[f17131,f9256]) ).
fof(f17263,plain,
( ! [X0] :
( memberP(cons(X0,tl(sk4)),sk5)
| sk5 = X0 )
| ~ spl0_10
| spl0_14
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f17262,f809]) ).
fof(f19894,definition,
( spl0_258
<=> sk5 = hd(sk4) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f19896,plain,
( sk5 = hd(sk4)
| ~ spl0_258 ),
inference(avatar_component_clause,[],[f19894]) ).
fof(f33388,plain,
( memberP(sk4,sk5)
| sk5 = hd(sk4)
| ~ spl0_10
| spl0_14
| ~ spl0_28
| ~ spl0_247 ),
inference(superposition,[],[f17263,f1208]) ).
fof(f33389,plain,
( sk5 = hd(sk4)
| ~ spl0_10
| spl0_14
| ~ spl0_28
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f33388,f425]) ).
fof(f33390,plain,
( spl0_258
| ~ spl0_10
| spl0_14
| ~ spl0_28
| ~ spl0_247 ),
inference(avatar_split_clause,[],[f33389,f17129,f1206,f808,f475,f19894]) ).
fof(f101516,definition,
( spl0_2539
<=> ssList(cons(hd(sk4),nil)) ),
introduced(definition,[new_symbols(definition,[spl0_2539])],[avatar_definition]) ).
fof(f101518,plain,
( ssList(cons(hd(sk4),nil))
| ~ spl0_2539 ),
inference(avatar_component_clause,[],[f101516]) ).
fof(f101643,definition,
( spl0_2562
<=> ssList(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_2562])],[avatar_definition]) ).
fof(f101644,plain,
( ~ ssList(sk3)
| spl0_2562 ),
inference(avatar_component_clause,[],[f101643]) ).
fof(f101883,plain,
~ spl0_2562,
inference(avatar_split_clause,[],[f419,f101643]) ).
fof(f101884,plain,
( ! [X0,X1] :
( sk4 != cons(X0,skaf82(X1))
| ssList(skaf82(X1))
| sk3 = app(skaf82(X1),cons(X0,nil)) )
| ~ spl0_10 ),
inference(superposition,[],[f484,f825]) ).
fof(f101940,plain,
( ! [X0,X1] :
( sk4 != cons(X0,skaf82(X1))
| sk3 = app(skaf82(X1),cons(X0,nil)) )
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f101884,f247]) ).
fof(f175413,plain,
( sk4 != sk4
| sk3 = app(skaf82(sk4),cons(skaf83(sk4),nil))
| ~ spl0_10
| ~ spl0_29 ),
inference(superposition,[],[f101940,f1213]) ).
fof(f175417,plain,
( sk3 = app(skaf82(sk4),cons(skaf83(sk4),nil))
| ~ spl0_10
| ~ spl0_29 ),
inference(trivial_inequality_removal,[],[f175413]) ).
fof(f175420,plain,
( sk3 = app(skaf82(sk4),cons(hd(sk4),nil))
| ~ spl0_10
| ~ spl0_29 ),
inference(forward_demodulation,[],[f175417,f10262]) ).
fof(f190400,plain,
( sk3 = app(tl(sk4),cons(hd(sk4),nil))
| ~ spl0_10
| ~ spl0_29 ),
inference(forward_demodulation,[],[f175420,f10571]) ).
fof(f519587,plain,
( ~ memberP(sk3,hd(sk4))
| ssList(tl(sk4))
| ssList(sk3)
| ssList(nil)
| ~ spl0_10
| ~ spl0_29 ),
inference(superposition,[],[f9179,f190400]) ).
fof(f519628,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(cons(hd(sk4),nil))
| ssList(tl(sk4))
| memberP(tl(sk4),X0) )
| ~ spl0_10
| ~ spl0_29 ),
inference(superposition,[],[f1122,f190400]) ).
fof(f519647,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| ssList(cons(hd(sk4),nil))
| memberP(tl(sk4),X0) )
| ~ spl0_10
| spl0_14
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f519628,f809]) ).
fof(f519671,plain,
( ~ memberP(sk3,hd(sk4))
| ssList(sk3)
| ssList(nil)
| ~ spl0_10
| spl0_14
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f519587,f809]) ).
fof(f519710,definition,
( spl0_7792
<=> ! [X0] :
( ~ memberP(sk3,X0)
| memberP(tl(sk4),X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7792])],[avatar_definition]) ).
fof(f519711,plain,
( ! [X0] :
( ~ memberP(sk3,X0)
| memberP(tl(sk4),X0) )
| ~ spl0_7792 ),
inference(avatar_component_clause,[],[f519710]) ).
fof(f519712,plain,
( spl0_2539
| spl0_7792
| ~ spl0_10
| spl0_14
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f519647,f1211,f808,f475,f519710,f101516]) ).
fof(f519766,plain,
( ~ memberP(sk3,hd(sk4))
| ssList(nil)
| ~ spl0_10
| spl0_14
| ~ spl0_29
| spl0_2562 ),
inference(forward_subsumption_resolution,[],[f519671,f101644]) ).
fof(f519773,plain,
( ~ memberP(sk3,hd(sk4))
| spl0_4
| ~ spl0_10
| spl0_14
| ~ spl0_29
| spl0_2562 ),
inference(forward_subsumption_resolution,[],[f519766,f448]) ).
fof(f533587,plain,
( ssList(nil)
| ~ spl0_10
| ~ spl0_2539 ),
inference(resolution,[],[f101518,f582]) ).
fof(f533588,plain,
( $false
| spl0_4
| ~ spl0_10
| ~ spl0_2539 ),
inference(forward_subsumption_resolution,[],[f533587,f448]) ).
fof(f533589,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_2539 ),
inference(avatar_contradiction_clause,[],[f533588]) ).
fof(f541971,plain,
( ~ memberP(sk3,sk5)
| spl0_4
| ~ spl0_10
| spl0_14
| ~ spl0_29
| ~ spl0_258
| spl0_2562 ),
inference(superposition,[],[f519773,f19896]) ).
fof(f541981,plain,
( $false
| spl0_4
| ~ spl0_10
| spl0_14
| ~ spl0_29
| ~ spl0_258
| spl0_2562 ),
inference(forward_subsumption_resolution,[],[f541971,f426]) ).
fof(f541982,plain,
( spl0_4
| ~ spl0_10
| spl0_14
| ~ spl0_29
| ~ spl0_258
| spl0_2562 ),
inference(avatar_contradiction_clause,[],[f541981]) ).
fof(f583564,plain,
( memberP(tl(sk4),sk5)
| ~ spl0_7792 ),
inference(resolution,[],[f519711,f426]) ).
fof(f583565,plain,
( $false
| spl0_247
| ~ spl0_7792 ),
inference(forward_subsumption_resolution,[],[f583564,f17130]) ).
fof(f583566,plain,
( spl0_247
| ~ spl0_7792 ),
inference(avatar_contradiction_clause,[],[f583565]) ).
cnf(s1,plain,
( ~ spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f441]) ).
cnf(s8,plain,
( spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f480]) ).
cnf(s11,plain,
~ spl0_4,
inference(sat_conversion,[],[f483]) ).
cnf(s24,plain,
( spl0_1
| ~ spl0_14 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s30,plain,
( ~ spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s31,plain,
( spl0_1
| spl0_28 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s32,plain,
( spl0_1
| spl0_29 ),
inference(sat_conversion,[],[f1234]) ).
cnf(s119,plain,
~ spl0_60,
inference(sat_conversion,[],[f3860]) ).
cnf(s189,plain,
( ~ spl0_11
| spl0_60 ),
inference(sat_conversion,[],[f9111]) ).
cnf(s368,plain,
( ~ spl0_10
| spl0_14
| ~ spl0_28
| ~ spl0_247
| spl0_258 ),
inference(sat_conversion,[],[f33390]) ).
cnf(s3062,plain,
~ spl0_2562,
inference(sat_conversion,[],[f101883]) ).
cnf(s13731,plain,
( ~ spl0_10
| spl0_14
| ~ spl0_29
| spl0_2539
| spl0_7792 ),
inference(sat_conversion,[],[f519712]) ).
cnf(s15310,plain,
( spl0_4
| ~ spl0_10
| ~ spl0_2539 ),
inference(sat_conversion,[],[f533589]) ).
cnf(s16097,plain,
( spl0_4
| ~ spl0_10
| spl0_14
| ~ spl0_29
| ~ spl0_258
| spl0_2562 ),
inference(sat_conversion,[],[f541982]) ).
cnf(s17115,plain,
( spl0_247
| ~ spl0_7792 ),
inference(sat_conversion,[],[f583566]) ).
cnf(s17296,plain,
~ spl0_11,
inference(rat,[],[s189,s119]) ).
cnf(s17383,plain,
spl0_10,
inference(rat,[],[s8,s17296]) ).
cnf(s17385,plain,
~ spl0_2539,
inference(rat,[],[s15310,s11,s17383]) ).
cnf(s18173,plain,
spl0_1,
inference(rat,[],[s368,s17115,s16097,s13731,s24,s31,s32,s17383,s11,s3062,s17385]) ).
cnf(s18174,plain,
~ spl0_2,
inference(rat,[],[s30,s18173]) ).
cnf(s18177,plain,
$false,
inference(rat,[],[s1,s18174,s18173]) ).
fof(f583571,plain,
$false,
inference(avatar_sat_refutation,[],[s18177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC409-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 09:31:31 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.67/2.38 % (1660332)Will run a generic schedule for satisfiability detection.
% 14.67/2.38 % (1660337)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3973446743_2999 on theBenchmark for (2999ds/0Mi)
% 14.67/2.38 % (1660338)% WARNING: option uhcvi not known.
% 14.67/2.38 % TRYING [1]
% 14.67/2.38 % TRYING [2]
% 14.67/2.38 % (1660338)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4046159020:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.67/2.38 % (1660339)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1338119903:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.67/2.38 % (1660340)dis+10_1_sil=32000:sp=arity:random_seed=1894431678:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.67/2.38 % (1660341)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1611287127:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.67/2.38 % (1660342)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1221119497:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.67/2.38 % (1660343)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3023932950:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.67/2.38 % TRYING [3]
% 14.67/2.38 % TRYING [4]
% 14.67/2.38 % TRYING [5]
% 14.67/2.38 % (1660341)Instruction limit reached!
% 14.67/2.38 % (1660341)------------------------------
% 14.67/2.38 % (1660341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.38 % (1660341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.38 % (1660341)CaDiCaL version: 2.1.3
% 14.67/2.38 % (1660341)Termination reason: Instruction limit
% 14.67/2.38 % (1660341)Termination phase: Saturation
% 14.67/2.38 % (1660341)Time elapsed: 0.059 s
% 14.67/2.38 % (1660341)Peak memory usage: 13 MB
% 14.67/2.38 % (1660341)Instructions burned: 117 (million)
% 14.67/2.38 % (1660340)Instruction limit reached!
% 14.67/2.38 % (1660340)------------------------------
% 14.67/2.38 % (1660340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.38 % (1660340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.38 % (1660340)CaDiCaL version: 2.1.3
% 14.67/2.38 % (1660340)Termination reason: Instruction limit
% 14.67/2.38 % (1660340)Termination phase: Saturation
% 14.67/2.38 % (1660340)Time elapsed: 0.060 s
% 14.67/2.38 % (1660340)Peak memory usage: 13 MB
% 14.67/2.38 % (1660340)Instructions burned: 105 (million)
% 14.67/2.38 % (1660342)Instruction limit reached!
% 14.67/2.38 % (1660342)------------------------------
% 14.67/2.38 % (1660342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.38 % (1660342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.38 % (1660342)CaDiCaL version: 2.1.3
% 14.67/2.38 % (1660342)Termination reason: Instruction limit
% 14.67/2.38 % (1660342)Termination phase: Saturation
% 14.67/2.38 % (1660342)Time elapsed: 0.068 s
% 14.67/2.38 % (1660342)Peak memory usage: 14 MB
% 14.67/2.38 % (1660342)Instructions burned: 134 (million)
% 14.67/2.38 % (1660352)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1889690931:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.67/2.38 % (1660351)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2157437054:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.67/2.38 % (1660353)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=3260771953:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.67/2.38 % TRYING [1]
% 14.67/2.38 % TRYING [2]
% 14.67/2.38 % (1660343)Instruction limit reached!
% 14.67/2.38 % (1660343)------------------------------
% 14.67/2.38 % (1660343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.67/2.38 % (1660343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.67/2.38 % (1660343)CaDiCaL version: 2.1.3
% 14.67/2.38 % (1660343)Termination reason: Instruction limit
% 14.67/2.38 % (1660343)Termination phase: Saturation
% 14.67/2.38 % (1660343)Time elapsed: 0.092 s
% 14.67/2.38 % (1660343)Peak memory usage: 14 MB
% 14.67/2.38 % (1660343)Instructions burned: 160 (million)
% 14.67/2.38 % TRYING [3]
% 14.67/2.38 % (1660357)ott-21_1_sil=16000:fs=off:random_seed=2569196041:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.67/2.38 % TRYING [4]
% 14.67/2.38 % TRYING [6]
% 14.67/2.38 % (1660352)Instruction limit reached!
% 14.67/2.38 % (1660352)------------------------------
% 14.67/2.38 % (1660352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660352)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660352)Termination reason: Instruction limit
% 46.57/6.87 % (1660352)Termination phase: Saturation
% 46.57/6.87 % (1660352)Time elapsed: 0.073 s
% 46.57/6.87 % (1660352)Peak memory usage: 14 MB
% 46.57/6.87 % (1660352)Instructions burned: 132 (million)
% 46.57/6.87 % (1660359)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=391279969:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 46.57/6.87 % TRYING [5]
% 46.57/6.87 % (1660357)Instruction limit reached!
% 46.57/6.87 % (1660357)------------------------------
% 46.57/6.87 % (1660357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660357)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660357)Termination reason: Instruction limit
% 46.57/6.87 % (1660357)Termination phase: Saturation
% 46.57/6.87 % (1660357)Time elapsed: 0.091 s
% 46.57/6.87 % (1660357)Peak memory usage: 13 MB
% 46.57/6.87 % (1660357)Instructions burned: 181 (million)
% 46.57/6.87 % (1660361)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2682986547:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 46.57/6.87 % TRYING [1]
% 46.57/6.87 % TRYING [2]
% 46.57/6.87 % TRYING [3]
% 46.57/6.87 % TRYING [4]
% 46.57/6.87 % TRYING [6]
% 46.57/6.87 % (1660351)Instruction limit reached!
% 46.57/6.87 % (1660351)------------------------------
% 46.57/6.87 % (1660351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660351)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660351)Termination reason: Instruction limit
% 46.57/6.87 % (1660351)Termination phase: Finite model building constraint generation
% 46.57/6.87 % (1660351)Time elapsed: 0.287 s
% 46.57/6.87 % (1660351)Peak memory usage: 36 MB
% 46.57/6.87 % (1660351)Instructions burned: 714 (million)
% 46.57/6.87 % TRYING [7]
% 46.57/6.87 % TRYING [5]
% 46.57/6.87 % (1660363)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3404789711:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 46.57/6.87 % (1660353)Instruction limit reached!
% 46.57/6.87 % (1660353)------------------------------
% 46.57/6.87 % (1660353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660353)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660353)Termination reason: Instruction limit
% 46.57/6.87 % (1660353)Termination phase: Saturation
% 46.57/6.87 % (1660353)Time elapsed: 0.377 s
% 46.57/6.87 % (1660353)Peak memory usage: 20 MB
% 46.57/6.87 % (1660353)Instructions burned: 686 (million)
% 46.57/6.87 % (1660365)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1016588741:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 46.57/6.87 % (1660359)Instruction limit reached!
% 46.57/6.87 % (1660359)------------------------------
% 46.57/6.87 % (1660359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660359)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660359)Termination reason: Instruction limit
% 46.57/6.87 % (1660359)Termination phase: Saturation
% 46.57/6.87 % (1660359)Time elapsed: 0.319 s
% 46.57/6.87 % (1660359)Peak memory usage: 14 MB
% 46.57/6.87 % (1660359)Instructions burned: 477 (million)
% 46.57/6.87 % (1660367)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=254327695:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 46.57/6.87 % (1660361)Instruction limit reached!
% 46.57/6.87 % (1660361)------------------------------
% 46.57/6.87 % (1660361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.57/6.87 % (1660361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.57/6.87 % (1660361)CaDiCaL version: 2.1.3
% 46.57/6.87 % (1660361)Termination reason: Instruction limit
% 46.57/6.87 % (1660361)Termination phase: Finite model building SAT solving
% 46.57/6.87 % (1660361)Time elapsed: 0.340 s
% 46.57/6.87 % (1660361)Peak memory usage: 23 MB
% 46.57/6.87 % (1660361)Instructions burned: 866 (million)
% 46.57/6.87 % (1660369)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2772086610:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 46.57/6.87 % TRYING [14]
% 93.38/13.46 % (1660365)Instruction limit reached!
% 93.38/13.46 % (1660365)------------------------------
% 93.38/13.46 % (1660365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660365)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660365)Termination reason: Instruction limit
% 93.38/13.46 % (1660365)Termination phase: Finite model building constraint generation
% 93.38/13.46 % (1660365)Time elapsed: 0.327 s
% 93.38/13.46 % (1660365)Peak memory usage: 72 MB
% 93.38/13.46 % (1660365)Instructions burned: 891 (million)
% 93.38/13.46 % (1660371)fmb+10_1_sil=64000:random_seed=287893360:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 93.38/13.46 % TRYING [1]
% 93.38/13.46 % TRYING [2]
% 93.38/13.46 % TRYING [3]
% 93.38/13.46 % TRYING [8]
% 93.38/13.46 % (1660367)Instruction limit reached!
% 93.38/13.46 % (1660367)------------------------------
% 93.38/13.46 % (1660367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660367)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660367)Termination reason: Instruction limit
% 93.38/13.46 % (1660367)Termination phase: Saturation
% 93.38/13.46 % (1660367)Time elapsed: 0.381 s
% 93.38/13.46 % (1660367)Peak memory usage: 21 MB
% 93.38/13.46 % (1660367)Instructions burned: 694 (million)
% 93.38/13.46 % (1660373)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=387828035:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 93.38/13.46 % TRYING [4]
% 93.38/13.46 % TRYING [20]
% 93.38/13.46 % (1660363)Instruction limit reached!
% 93.38/13.46 % (1660363)------------------------------
% 93.38/13.46 % (1660363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660363)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660363)Termination reason: Instruction limit
% 93.38/13.46 % (1660363)Termination phase: Saturation
% 93.38/13.46 % (1660363)Time elapsed: 0.656 s
% 93.38/13.46 % (1660363)Peak memory usage: 27 MB
% 93.38/13.46 % (1660363)Instructions burned: 1181 (million)
% 93.38/13.46 % (1660369)Instruction limit reached!
% 93.38/13.46 % (1660369)------------------------------
% 93.38/13.46 % (1660369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660369)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660369)Termination reason: Instruction limit
% 93.38/13.46 % (1660369)Termination phase: Saturation
% 93.38/13.46 % (1660369)Time elapsed: 0.463 s
% 93.38/13.46 % (1660369)Peak memory usage: 21 MB
% 93.38/13.46 % (1660369)Instructions burned: 881 (million)
% 93.38/13.46 % (1660375)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1840939595:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 93.38/13.46 % (1660376)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2531028122:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 93.38/13.46 % TRYING [5]
% 93.38/13.46 % TRYING [8]
% 93.38/13.46 % (1660375)Instruction limit reached!
% 93.38/13.46 % (1660375)------------------------------
% 93.38/13.46 % (1660375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660375)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660375)Termination reason: Instruction limit
% 93.38/13.46 % (1660375)Termination phase: Finite model building constraint generation
% 93.38/13.46 % (1660375)Time elapsed: 0.331 s
% 93.38/13.46 % (1660375)Peak memory usage: 79 MB
% 93.38/13.46 % (1660375)Instructions burned: 922 (million)
% 93.38/13.46 % (1660379)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4203270652:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 93.38/13.46 % TRYING [6]
% 93.38/13.46 % (1660379)Instruction limit reached!
% 93.38/13.46 % (1660379)------------------------------
% 93.38/13.46 % (1660379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 93.38/13.46 % (1660379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 93.38/13.46 % (1660379)CaDiCaL version: 2.1.3
% 93.38/13.46 % (1660379)Termination reason: Instruction limit
% 93.38/13.46 % (1660379)Termination phase: Saturation
% 93.38/13.46 % (1660379)Time elapsed: 0.664 s
% 93.38/13.46 % (1660379)Peak memory usage: 15 MB
% 93.38/13.46 % (1660379)Instructions burned: 1474 (million)
% 93.38/13.46 % (1660381)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1159118578:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 95.99/18.17 % TRYING [77]
% 95.99/18.17 % TRYING [9]
% 95.99/18.17 % TRYING [7]
% 95.99/18.17 % (1660376)Instruction limit reached!
% 95.99/18.17 % (1660376)------------------------------
% 95.99/18.17 % (1660376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660376)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660376)Termination reason: Instruction limit
% 95.99/18.17 % (1660376)Termination phase: Saturation
% 95.99/18.17 % (1660376)Time elapsed: 2.700 s
% 95.99/18.17 % (1660376)Peak memory usage: 56 MB
% 95.99/18.17 % (1660376)Instructions burned: 5131 (million)
% 95.99/18.17 % (1660383)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1899977827:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 95.99/18.17 % TRYING [16]
% 95.99/18.17 % TRYING [10]
% 95.99/18.17 % (1660373)Instruction limit reached!
% 95.99/18.17 % (1660373)------------------------------
% 95.99/18.17 % (1660373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660373)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660373)Termination reason: Instruction limit
% 95.99/18.17 % (1660373)Termination phase: Finite model building constraint generation
% 95.99/18.17 % (1660373)Time elapsed: 3.260 s
% 95.99/18.17 % (1660373)Peak memory usage: 589 MB
% 95.99/18.17 % (1660373)Instructions burned: 9518 (million)
% 95.99/18.17 % TRYING [8]
% 95.99/18.17 % (1660385)ott-2_1_sil=16000:newcnf=on:random_seed=1779205957:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 95.99/18.17 % (1660381)Instruction limit reached!
% 95.99/18.17 % (1660381)------------------------------
% 95.99/18.17 % (1660381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660381)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660381)Termination reason: Instruction limit
% 95.99/18.17 % (1660381)Termination phase: Finite model building constraint generation
% 95.99/18.17 % (1660381)Time elapsed: 2.225 s
% 95.99/18.17 % (1660381)Peak memory usage: 431 MB
% 95.99/18.17 % (1660381)Instructions burned: 6325 (million)
% 95.99/18.17 % (1660387)ott+10_1_sil=32000:tgt=ground:random_seed=2287308179:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 95.99/18.17 % (1660383)Instruction limit reached!
% 95.99/18.17 % (1660383)------------------------------
% 95.99/18.17 % (1660383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660383)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660383)Termination reason: Instruction limit
% 95.99/18.17 % (1660383)Termination phase: Finite model building constraint generation
% 95.99/18.17 % (1660383)Time elapsed: 0.752 s
% 95.99/18.17 % (1660383)Peak memory usage: 138 MB
% 95.99/18.17 % (1660383)Instructions burned: 2178 (million)
% 95.99/18.17 % (1660389)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1204538648:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 95.99/18.17 % TRYING [1]
% 95.99/18.17 % TRYING [2]
% 95.99/18.17 % TRYING [3]
% 95.99/18.17 % TRYING [4]
% 95.99/18.17 % TRYING [5]
% 95.99/18.17 % (1660385)Instruction limit reached!
% 95.99/18.17 % (1660385)------------------------------
% 95.99/18.17 % (1660385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660385)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660385)Termination reason: Instruction limit
% 95.99/18.17 % (1660385)Termination phase: Saturation
% 95.99/18.17 % (1660385)Time elapsed: 0.469 s
% 95.99/18.17 % (1660385)Peak memory usage: 23 MB
% 95.99/18.17 % (1660385)Instructions burned: 869 (million)
% 95.99/18.17 % (1660391)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3045182209:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 95.99/18.17 % TRYING [6]
% 95.99/18.17 % TRYING [7]
% 95.99/18.17 % TRYING [8]
% 95.99/18.17 % (1660391)Instruction limit reached!
% 95.99/18.17 % (1660391)------------------------------
% 95.99/18.17 % (1660391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660391)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660391)Termination reason: Instruction limit
% 95.99/18.17 % (1660391)Termination phase: Saturation
% 95.99/18.17 % (1660391)Time elapsed: 1.839 s
% 95.99/18.17 % (1660391)Peak memory usage: 46 MB
% 95.99/18.17 % (1660391)Instructions burned: 3514 (million)
% 95.99/18.17 % (1660393)dis+21_1_sil=32000:sas=cadical:random_seed=3950091633:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 95.99/18.17 % (1660387)Instruction limit reached!
% 95.99/18.17 % (1660387)------------------------------
% 95.99/18.17 % (1660387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660387)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660387)Termination reason: Instruction limit
% 95.99/18.17 % (1660387)Termination phase: Saturation
% 95.99/18.17 % (1660387)Time elapsed: 2.715 s
% 95.99/18.17 % (1660387)Peak memory usage: 70 MB
% 95.99/18.17 % (1660387)Instructions burned: 5114 (million)
% 95.99/18.17 % (1660395)ott+11_1_sil=16000:gs=on:random_seed=786120202:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2928 on theBenchmark for (2928ds/2251Mi)
% 95.99/18.17 % TRYING [9]
% 95.99/18.17 % (1660395)Instruction limit reached!
% 95.99/18.17 % (1660395)------------------------------
% 95.99/18.17 % (1660395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660395)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660395)Termination reason: Instruction limit
% 95.99/18.17 % (1660395)Termination phase: Saturation
% 95.99/18.17 % (1660395)Time elapsed: 0.883 s
% 95.99/18.17 % (1660395)Peak memory usage: 13 MB
% 95.99/18.17 % (1660395)Instructions burned: 2252 (million)
% 95.99/18.17 % (1660397)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=785202386:fmbsr=1.6:i=67534_2919 on theBenchmark for (2919ds/67534Mi)
% 95.99/18.17 % TRYING [7]
% 95.99/18.17 % TRYING [9]
% 95.99/18.17 % TRYING [11]
% 95.99/18.17 % (1660393)Instruction limit reached!
% 95.99/18.17 % (1660393)------------------------------
% 95.99/18.17 % (1660393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660393)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660393)Termination reason: Instruction limit
% 95.99/18.17 % (1660393)Termination phase: Saturation
% 95.99/18.17 % (1660393)Time elapsed: 1.963 s
% 95.99/18.17 % (1660393)Peak memory usage: 49 MB
% 95.99/18.17 % (1660393)Instructions burned: 3774 (million)
% 95.99/18.17 % (1660399)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4118507219:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2913 on theBenchmark for (2913ds/4591Mi)
% 95.99/18.17 % (1660371)Instruction limit reached!
% 95.99/18.17 % (1660371)------------------------------
% 95.99/18.17 % (1660371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660371)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660371)Termination reason: Instruction limit
% 95.99/18.17 % (1660371)Termination phase: Finite model building constraint generation
% 95.99/18.17 % (1660371)Time elapsed: 8.585 s
% 95.99/18.17 % (1660371)Peak memory usage: 248 MB
% 95.99/18.17 % (1660371)Instructions burned: 22062 (million)
% 95.99/18.17 % (1660401)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3827654967:i=29340_2905 on theBenchmark for (2905ds/29340Mi)
% 95.99/18.17 % TRYING [8]
% 95.99/18.17 % (1660399)Instruction limit reached!
% 95.99/18.17 % (1660399)------------------------------
% 95.99/18.17 % (1660399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660399)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660399)Termination reason: Instruction limit
% 95.99/18.17 % (1660399)Termination phase: Saturation
% 95.99/18.17 % (1660399)Time elapsed: 2.037 s
% 95.99/18.17 % (1660399)Peak memory usage: 50 MB
% 95.99/18.17 % (1660399)Instructions burned: 4591 (million)
% 95.99/18.17 % (1660403)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3498138757:i=5211_2893 on theBenchmark for (2893ds/5211Mi)
% 95.99/18.17 % (1660403)Instruction limit reached!
% 95.99/18.17 % (1660403)------------------------------
% 95.99/18.17 % (1660403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660403)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660403)Termination reason: Instruction limit
% 95.99/18.17 % (1660403)Termination phase: Saturation
% 95.99/18.17 % (1660403)Time elapsed: 2.508 s
% 95.99/18.17 % (1660403)Peak memory usage: 47 MB
% 95.99/18.17 % (1660403)Instructions burned: 5212 (million)
% 95.99/18.17 % (1660405)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2468406691:i=5497:nm=2_2867 on theBenchmark for (2867ds/5497Mi)
% 95.99/18.17 % TRYING [17]
% 95.99/18.17 % TRYING [9]
% 95.99/18.17 % TRYING [10]
% 95.99/18.17 % (1660405)Instruction limit reached!
% 95.99/18.17 % (1660405)------------------------------
% 95.99/18.17 % (1660405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.17 % (1660405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.17 % (1660405)CaDiCaL version: 2.1.3
% 95.99/18.17 % (1660405)Termination reason: Instruction limit
% 95.99/18.17 % (1660405)Termination phase: Finite model building constraint generation
% 95.99/18.17 % (1660405)Time elapsed: 1.859 s
% 95.99/18.17 % (1660405)Peak memory usage: 345 MB
% 95.99/18.17 % (1660405)Instructions burned: 5500 (million)
% 95.99/18.17 % (1660407)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=972043913:fmbsr=2:i=46332_2848 on theBenchmark for (2848ds/46332Mi)
% 95.99/18.17 % TRYING [15]
% 95.99/18.17 % (1660338) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1660332-1660338"...
% 95.99/18.17 % (1660338)...printing done.
% 95.99/18.17 % (1660338)Refutation found. Thanks to Tanya!
% 95.99/18.17 % SZS status Unsatisfiable for theBenchmark
% 95.99/18.17 % SZS output start Proof for theBenchmark
% See solution above
% 95.99/18.18 % (1660338)------------------------------
% 95.99/18.18 % (1660338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/18.18 % (1660338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/18.18 % (1660338)CaDiCaL version: 2.1.3
% 95.99/18.18 % (1660338)Termination reason: Refutation
% 95.99/18.18 % (1660338)Time elapsed: 17.716 s
% 95.99/18.18 % (1660338)Peak memory usage: 256 MB
% 95.99/18.18 % (1660338)Instructions burned: 33108 (million)
% 95.99/18.18 % (1660332)Success in time 17.941 s
% 95.99/18.18 % Vampire exiting
%------------------------------------------------------------------------------