%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC383-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 : n004.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:48 PM UTC 2026
% Result : Unsatisfiable 203.22s 41.18s
% Output : Refutation 203.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 29
% Syntax : Number of formulae : 108 ( 22 unt; 8 def)
% Number of atoms : 300 ( 28 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 374 ( 182 ~; 184 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 9 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause8) ).
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(f73,axiom,
! [X0] :
( ~ ssList(X0)
| app(X0,nil) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause73) ).
fof(f74,axiom,
! [X0] :
( ~ ssList(X0)
| app(nil,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause74) ).
fof(f85,axiom,
! [X0,X1] :
( ssList(app(X1,X0))
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause85) ).
fof(f118,axiom,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause115) ).
fof(f119,axiom,
! [X0,X1] :
( cons(X0,nil) != X1
| ~ ssItem(X0)
| ~ ssList(X1)
| singletonP(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause116) ).
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(f164,axiom,
! [X2,X0,X1] :
( segmentP(X0,X2)
| ~ segmentP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0)
| ~ segmentP(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause152) ).
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(f187,axiom,
! [X2,X3,X0,X1] :
( app(app(X0,X1),X2) != X3
| ~ ssList(X2)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X3)
| segmentP(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause173) ).
fof(f202,negated_conjecture,
ssList(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_3) ).
fof(f203,negated_conjecture,
ssList(sk4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_4) ).
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,
neq(sk2,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
( ssItem(sk5)
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f209,negated_conjecture,
( cons(sk5,nil) = sk3
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f210,plain,
( sk3 = cons(sk5,nil)
| nil = sk4 ),
inference(reorient_equations,[],[f209]) ).
fof(f211,negated_conjecture,
( memberP(sk4,sk5)
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_11) ).
fof(f217,negated_conjecture,
( ~ singletonP(sk1)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_16) ).
fof(f220,plain,
neq(sk4,nil),
inference(definition_unfolding,[],[f206,f204]) ).
fof(f221,plain,
( ~ singletonP(sk3)
| ~ segmentP(sk4,sk3) ),
inference(definition_unfolding,[],[f217,f205,f204,f205]) ).
fof(f228,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(equality_resolution,[],[f118]) ).
fof(f229,plain,
! [X0] :
( singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil))
| ~ ssItem(X0) ),
inference(equality_resolution,[],[f119]) ).
fof(f236,plain,
! [X2,X0,X1] :
( segmentP(app(app(X0,X1),X2),X1)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(app(app(X0,X1),X2))
| ~ ssList(X2) ),
inference(equality_resolution,[],[f187]) ).
fof(f250,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1) ),
inference(duplicate_literal_removal,[],[f228]) ).
fof(f253,definition,
( spl0_1
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f255,plain,
( nil = sk4
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f257,definition,
( spl0_2
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f259,plain,
( ssItem(sk5)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f260,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f207,f257,f253]) ).
fof(f267,definition,
( spl0_4
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f269,plain,
( ~ segmentP(sk4,sk3)
| spl0_4 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl0_5
<=> singletonP(sk3) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f273,plain,
( ~ singletonP(sk3)
| spl0_5 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
( ~ spl0_4
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f221,f271,f267]) ).
fof(f276,definition,
( spl0_6
<=> memberP(sk4,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f278,plain,
( memberP(sk4,sk5)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f276]) ).
fof(f279,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f211,f276,f253]) ).
fof(f281,plain,
( neq(nil,nil)
| ~ spl0_1 ),
inference(superposition,[],[f220,f255]) ).
fof(f286,definition,
( spl0_7
<=> sk3 = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f288,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f289,plain,
( spl0_1
| spl0_7 ),
inference(avatar_split_clause,[],[f210,f286,f253]) ).
fof(f331,plain,
( ~ ssList(nil)
| ~ spl0_1 ),
inference(resolution,[],[f250,f281]) ).
fof(f332,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f331,f8]) ).
fof(f333,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f332]) ).
fof(f379,plain,
sk4 = app(sk4,nil),
inference(resolution,[],[f73,f203]) ).
fof(f409,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f761,plain,
( singletonP(sk3)
| ~ ssList(sk3)
| ~ ssItem(sk5)
| ~ spl0_7 ),
inference(superposition,[],[f229,f288]) ).
fof(f763,plain,
( ~ ssList(sk3)
| ~ ssItem(sk5)
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f761,f273]) ).
fof(f765,plain,
( ~ ssItem(sk5)
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f763,f202]) ).
fof(f766,plain,
( $false
| ~ spl0_2
| spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f765,f259]) ).
fof(f767,plain,
( ~ spl0_2
| spl0_5
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f766]) ).
fof(f905,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(cons(sk5,nil),X0) )
| ~ spl0_2 ),
inference(resolution,[],[f126,f259]) ).
fof(f966,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(sk3,X0) )
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_demodulation,[],[f905,f288]) ).
fof(f1631,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ segmentP(sk4,X0) )
| spl0_4 ),
inference(resolution,[],[f164,f269]) ).
fof(f1637,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ segmentP(sk4,X0) )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1631,f202]) ).
fof(f1639,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ segmentP(sk4,X0)
| ~ ssList(X0) )
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1637,f203]) ).
fof(f2491,plain,
( ~ ssItem(sk5)
| ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_6 ),
inference(resolution,[],[f182,f278]) ).
fof(f2502,plain,
( ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2491,f259]) ).
fof(f2515,plain,
( sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2502,f203]) ).
fof(f2778,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ),
inference(superposition,[],[f236,f409]) ).
fof(f2829,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2778,f85]) ).
fof(f2855,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2829,f8]) ).
fof(f2881,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2855,f202]) ).
fof(f3243,plain,
( ! [X0,X1] : cons(sk5,skaf43(X0,X1)) = app(sk3,skaf43(X0,X1))
| ~ spl0_2
| ~ spl0_7 ),
inference(resolution,[],[f966,f52]) ).
fof(f3596,plain,
( ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(skaf42(sk4,sk5))
| ~ ssList(cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[],[f236,f2515]) ).
fof(f3597,plain,
( ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(app(sk4,X0))
| ~ ssList(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f3596,f53]) ).
fof(f88606,plain,
( ! [X0,X1] :
( segmentP(cons(sk5,skaf43(X0,X1)),sk3)
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_7 ),
inference(superposition,[],[f2881,f3243]) ).
fof(f88608,plain,
( ! [X0,X1] :
( ssList(cons(sk5,skaf43(X0,X1)))
| ~ ssList(sk3)
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_7 ),
inference(superposition,[],[f85,f3243]) ).
fof(f88651,plain,
( ! [X0,X1] :
( ssList(cons(sk5,skaf43(X0,X1)))
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f88608,f202]) ).
fof(f88653,plain,
( ! [X0,X1] : segmentP(cons(sk5,skaf43(X0,X1)),sk3)
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f88606,f52]) ).
fof(f88678,plain,
( ! [X0,X1] : ssList(cons(sk5,skaf43(X0,X1)))
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f88651,f52]) ).
fof(f95105,plain,
( ! [X0,X1] :
( ~ segmentP(sk4,cons(sk5,skaf43(X0,X1)))
| ~ ssList(cons(sk5,skaf43(X0,X1))) )
| ~ spl0_2
| spl0_4
| ~ spl0_7 ),
inference(resolution,[],[f88653,f1639]) ).
fof(f95123,plain,
( ! [X0,X1] : ~ segmentP(sk4,cons(sk5,skaf43(X0,X1)))
| ~ spl0_2
| spl0_4
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f95105,f88678]) ).
fof(f95158,definition,
( spl0_62
<=> ssList(cons(sk5,skaf43(sk5,sk4))) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f95160,plain,
( ~ ssList(cons(sk5,skaf43(sk5,sk4)))
| spl0_62 ),
inference(avatar_component_clause,[],[f95158]) ).
fof(f95166,plain,
( $false
| ~ spl0_2
| ~ spl0_7
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f95160,f88678]) ).
fof(f95167,plain,
( ~ spl0_2
| ~ spl0_7
| spl0_62 ),
inference(avatar_contradiction_clause,[],[f95166]) ).
fof(f221713,definition,
( spl0_129
<=> ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f221714,plain,
( ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) )
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f221713]) ).
fof(f221715,plain,
( ~ spl0_62
| spl0_129
| ~ spl0_2
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f3597,f276,f257,f221713,f95158]) ).
fof(f221738,plain,
( segmentP(sk4,cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ spl0_129 ),
inference(superposition,[],[f221714,f379]) ).
fof(f221752,plain,
( ~ ssList(nil)
| ~ ssList(sk4)
| ~ spl0_2
| spl0_4
| ~ spl0_7
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f221738,f95123]) ).
fof(f221759,plain,
( ~ ssList(sk4)
| ~ spl0_2
| spl0_4
| ~ spl0_7
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f221752,f8]) ).
fof(f221763,plain,
( $false
| ~ spl0_2
| spl0_4
| ~ spl0_7
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f221759,f203]) ).
fof(f221764,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_7
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f221763]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f260]) ).
cnf(s3,plain,
( ~ spl0_4
| ~ spl0_5 ),
inference(sat_conversion,[],[f274]) ).
cnf(s4,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f279]) ).
cnf(s6,plain,
( spl0_1
| spl0_7 ),
inference(sat_conversion,[],[f289]) ).
cnf(s16,plain,
~ spl0_1,
inference(sat_conversion,[],[f333]) ).
cnf(s23,plain,
( ~ spl0_2
| spl0_5
| ~ spl0_7 ),
inference(sat_conversion,[],[f767]) ).
cnf(s73,plain,
( ~ spl0_2
| ~ spl0_7
| spl0_62 ),
inference(sat_conversion,[],[f95167]) ).
cnf(s191,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_62
| spl0_129 ),
inference(sat_conversion,[],[f221715]) ).
cnf(s193,plain,
( ~ spl0_2
| spl0_4
| ~ spl0_7
| ~ spl0_129 ),
inference(sat_conversion,[],[f221764]) ).
cnf(s222,plain,
spl0_7,
inference(rat,[],[s6,s16]) ).
cnf(s223,plain,
spl0_6,
inference(rat,[],[s4,s16]) ).
cnf(s224,plain,
spl0_2,
inference(rat,[],[s1,s16]) ).
cnf(s226,plain,
spl0_62,
inference(rat,[],[s73,s222,s224]) ).
cnf(s232,plain,
spl0_5,
inference(rat,[],[s23,s222,s224]) ).
cnf(s235,plain,
spl0_129,
inference(rat,[],[s191,s224,s223,s226]) ).
cnf(s246,plain,
~ spl0_4,
inference(rat,[],[s3,s232]) ).
cnf(s253,plain,
$false,
inference(rat,[],[s193,s224,s222,s235,s246]) ).
fof(f221765,plain,
$false,
inference(avatar_sat_refutation,[],[s253]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC383-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.07/0.17 % Computer : n004.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 09:23:07 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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
% 25.37/3.87 % (228379)Will run a generic schedule for satisfiability detection.
% 25.37/3.87 % (228388)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=349058719:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 25.37/3.87 % (228385)% WARNING: option uhcvi not known.
% 25.37/3.87 % (228384)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1512718041_2999 on theBenchmark for (2999ds/0Mi)
% 25.37/3.87 % (228385)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2936145065:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 25.37/3.87 % (228386)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1328061376:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 25.37/3.87 % (228387)dis+10_1_sil=32000:sp=arity:random_seed=1517915036:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 25.37/3.87 % (228389)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3169935410:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 25.37/3.87 % (228390)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1811339605:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 25.37/3.87 % TRYING [1]
% 25.37/3.87 % TRYING [2]
% 25.37/3.87 % TRYING [3]
% 25.37/3.87 % (228388)Instruction limit reached!
% 25.37/3.87 % (228388)------------------------------
% 25.37/3.87 % (228388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.37/3.87 % (228388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/3.87 % (228388)CaDiCaL version: 2.1.3
% 25.37/3.87 % (228388)Termination reason: Instruction limit
% 25.37/3.87 % (228388)Termination phase: Saturation
% 25.37/3.87 % (228388)Time elapsed: 0.033 s
% 25.37/3.87 % (228388)Peak memory usage: 13 MB
% 25.37/3.87 % (228388)Instructions burned: 116 (million)
% 25.37/3.87 % (228398)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2804123871:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 25.37/3.87 % TRYING [4]
% 25.37/3.87 % TRYING [1]
% 25.37/3.87 % TRYING [2]
% 25.37/3.87 % TRYING [3]
% 25.37/3.87 % TRYING [4]
% 25.37/3.87 % (228387)Instruction limit reached!
% 25.37/3.87 % (228387)------------------------------
% 25.37/3.87 % (228387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.37/3.87 % (228387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/3.87 % (228387)CaDiCaL version: 2.1.3
% 25.37/3.87 % (228387)Termination reason: Instruction limit
% 25.37/3.87 % (228387)Termination phase: Saturation
% 25.37/3.87 % (228387)Time elapsed: 0.061 s
% 25.37/3.87 % (228387)Peak memory usage: 13 MB
% 25.37/3.87 % (228387)Instructions burned: 105 (million)
% 25.37/3.87 % (228389)Instruction limit reached!
% 25.37/3.87 % (228389)------------------------------
% 25.37/3.87 % (228389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.37/3.87 % (228389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/3.87 % (228389)CaDiCaL version: 2.1.3
% 25.37/3.87 % (228389)Termination reason: Instruction limit
% 25.37/3.87 % (228389)Termination phase: Saturation
% 25.37/3.87 % (228389)Time elapsed: 0.065 s
% 25.37/3.87 % (228389)Peak memory usage: 14 MB
% 25.37/3.87 % (228389)Instructions burned: 137 (million)
% 25.37/3.87 % (228400)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=575207043:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 25.37/3.87 % (228401)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=4215920266:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 25.37/3.87 % TRYING [5]
% 25.37/3.87 % (228390)Instruction limit reached!
% 25.37/3.87 % (228390)------------------------------
% 25.37/3.87 % (228390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.37/3.87 % (228390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.37/3.87 % (228390)CaDiCaL version: 2.1.3
% 25.37/3.87 % (228390)Termination reason: Instruction limit
% 25.37/3.87 % (228390)Termination phase: Saturation
% 25.37/3.87 % (228390)Time elapsed: 0.092 s
% 25.37/3.87 % (228390)Peak memory usage: 14 MB
% 25.37/3.87 % (228390)Instructions burned: 160 (million)
% 25.37/3.87 % TRYING [5]
% 25.37/3.87 % (228404)ott-21_1_sil=16000:fs=off:random_seed=4071856109:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 25.37/3.87 % (228400)Instruction limit reached!
% 25.37/3.87 % (228400)------------------------------
% 25.37/3.87 % (228400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.37/3.87 % (228400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228400)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228400)Termination reason: Instruction limit
% 45.98/6.75 % (228400)Termination phase: Saturation
% 45.98/6.75 % (228400)Time elapsed: 0.067 s
% 45.98/6.75 % (228400)Peak memory usage: 13 MB
% 45.98/6.75 % (228400)Instructions burned: 132 (million)
% 45.98/6.75 % (228406)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4005172948:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 45.98/6.75 % TRYING [6]
% 45.98/6.75 % (228398)Instruction limit reached!
% 45.98/6.75 % (228398)------------------------------
% 45.98/6.75 % (228398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.98/6.75 % (228398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228398)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228398)Termination reason: Instruction limit
% 45.98/6.75 % (228398)Termination phase: Finite model building constraint generation
% 45.98/6.75 % (228398)Time elapsed: 0.151 s
% 45.98/6.75 % (228398)Peak memory usage: 36 MB
% 45.98/6.75 % (228398)Instructions burned: 716 (million)
% 45.98/6.75 % (228404)Instruction limit reached!
% 45.98/6.75 % (228404)------------------------------
% 45.98/6.75 % (228404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.98/6.75 % (228404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228404)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228404)Termination reason: Instruction limit
% 45.98/6.75 % (228404)Termination phase: Saturation
% 45.98/6.75 % (228404)Time elapsed: 0.085 s
% 45.98/6.75 % (228404)Peak memory usage: 13 MB
% 45.98/6.75 % (228404)Instructions burned: 181 (million)
% 45.98/6.75 % (228408)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=134643265:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.98/6.75 % TRYING [1]
% 45.98/6.75 % TRYING [2]
% 45.98/6.75 % TRYING [3]
% 45.98/6.75 % (228409)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1932622345:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 45.98/6.75 % TRYING [4]
% 45.98/6.75 % TRYING [6]
% 45.98/6.75 % TRYING [5]
% 45.98/6.75 % (228408)Instruction limit reached!
% 45.98/6.75 % (228408)------------------------------
% 45.98/6.75 % (228408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.98/6.75 % (228408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228408)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228408)Termination reason: Instruction limit
% 45.98/6.75 % (228408)Termination phase: Finite model building SAT solving
% 45.98/6.75 % (228408)Time elapsed: 0.176 s
% 45.98/6.75 % (228408)Peak memory usage: 22 MB
% 45.98/6.75 % (228408)Instructions burned: 867 (million)
% 45.98/6.75 % (228412)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2367667960:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 45.98/6.75 % TRYING [14]
% 45.98/6.75 % (228401)Instruction limit reached!
% 45.98/6.75 % (228401)------------------------------
% 45.98/6.75 % (228401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.98/6.75 % (228401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228401)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228401)Termination reason: Instruction limit
% 45.98/6.75 % (228401)Termination phase: Saturation
% 45.98/6.75 % (228401)Time elapsed: 0.406 s
% 45.98/6.75 % (228401)Peak memory usage: 19 MB
% 45.98/6.75 % (228401)Instructions burned: 685 (million)
% 45.98/6.75 % (228406)Instruction limit reached!
% 45.98/6.75 % (228406)------------------------------
% 45.98/6.75 % (228406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.98/6.75 % (228406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.98/6.75 % (228406)CaDiCaL version: 2.1.3
% 45.98/6.75 % (228406)Termination reason: Instruction limit
% 45.98/6.75 % (228406)Termination phase: Saturation
% 45.98/6.75 % (228406)Time elapsed: 0.326 s
% 45.98/6.75 % (228406)Peak memory usage: 14 MB
% 45.98/6.75 % (228406)Instructions burned: 477 (million)
% 45.98/6.75 % (228414)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=3005837233: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)
% 45.98/6.75 % (228415)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3515527642:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 45.98/6.75 % (228412)Instruction limit reached!
% 45.98/6.75 % (228412)------------------------------
% 45.98/6.75 % (228412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228412)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228412)Termination reason: Instruction limit
% 94.90/13.69 % (228412)Termination phase: Finite model building constraint generation
% 94.90/13.69 % (228412)Time elapsed: 0.178 s
% 94.90/13.69 % (228412)Peak memory usage: 73 MB
% 94.90/13.69 % (228412)Instructions burned: 891 (million)
% 94.90/13.69 % (228418)fmb+10_1_sil=64000:random_seed=774073172:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 94.90/13.69 % TRYING [1]
% 94.90/13.69 % TRYING [2]
% 94.90/13.69 % TRYING [3]
% 94.90/13.69 % TRYING [4]
% 94.90/13.69 % TRYING [5]
% 94.90/13.69 % TRYING [7]
% 94.90/13.69 % (228409)Instruction limit reached!
% 94.90/13.69 % (228409)------------------------------
% 94.90/13.69 % (228409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228409)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228409)Termination reason: Instruction limit
% 94.90/13.69 % (228409)Termination phase: Saturation
% 94.90/13.69 % (228409)Time elapsed: 0.668 s
% 94.90/13.69 % (228409)Peak memory usage: 28 MB
% 94.90/13.69 % (228409)Instructions burned: 1181 (million)
% 94.90/13.69 % (228414)Instruction limit reached!
% 94.90/13.69 % (228414)------------------------------
% 94.90/13.69 % (228414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228414)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228414)Termination reason: Instruction limit
% 94.90/13.69 % (228414)Termination phase: Saturation
% 94.90/13.69 % (228414)Time elapsed: 0.382 s
% 94.90/13.69 % (228414)Peak memory usage: 21 MB
% 94.90/13.69 % (228414)Instructions burned: 693 (million)
% 94.90/13.69 % (228420)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=884827248:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 94.90/13.69 % TRYING [6]
% 94.90/13.69 % (228421)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1511102367:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 94.90/13.69 % TRYING [20]
% 94.90/13.69 % TRYING [8]
% 94.90/13.69 % (228415)Instruction limit reached!
% 94.90/13.69 % (228415)------------------------------
% 94.90/13.69 % (228415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228415)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228415)Termination reason: Instruction limit
% 94.90/13.69 % (228415)Termination phase: Saturation
% 94.90/13.69 % (228415)Time elapsed: 0.456 s
% 94.90/13.69 % (228415)Peak memory usage: 20 MB
% 94.90/13.69 % (228415)Instructions burned: 880 (million)
% 94.90/13.69 % (228424)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1080252125:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 94.90/13.69 % (228421)Instruction limit reached!
% 94.90/13.69 % (228421)------------------------------
% 94.90/13.69 % (228421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228421)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228421)Termination reason: Instruction limit
% 94.90/13.69 % (228421)Termination phase: Finite model building constraint generation
% 94.90/13.69 % (228421)Time elapsed: 0.333 s
% 94.90/13.69 % (228421)Peak memory usage: 79 MB
% 94.90/13.69 % (228421)Instructions burned: 922 (million)
% 94.90/13.69 % (228426)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1801606431:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 94.90/13.69 % TRYING [7]
% 94.90/13.69 % TRYING [8]
% 94.90/13.69 % (228426)Instruction limit reached!
% 94.90/13.69 % (228426)------------------------------
% 94.90/13.69 % (228426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.90/13.69 % (228426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.90/13.69 % (228426)CaDiCaL version: 2.1.3
% 94.90/13.69 % (228426)Termination reason: Instruction limit
% 94.90/13.69 % (228426)Termination phase: Saturation
% 94.90/13.69 % (228426)Time elapsed: 0.645 s
% 94.90/13.69 % (228426)Peak memory usage: 15 MB
% 94.90/13.69 % (228426)Instructions burned: 1473 (million)
% 94.90/13.69 % (228428)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1550265277:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 94.90/13.69 % TRYING [77]
% 94.90/13.69 % TRYING [8]
% 94.90/13.69 % (228424)Instruction limit reached!
% 94.90/13.69 % (228424)------------------------------
% 94.90/13.69 % (228424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228424)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228424)Termination reason: Instruction limit
% 223.99/31.81 % (228424)Termination phase: Saturation
% 223.99/31.81 % (228424)Time elapsed: 2.625 s
% 223.99/31.81 % (228424)Peak memory usage: 58 MB
% 223.99/31.81 % (228424)Instructions burned: 5132 (million)
% 223.99/31.81 % (228430)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3063145884:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 223.99/31.81 % TRYING [16]
% 223.99/31.81 % (228420)Instruction limit reached!
% 223.99/31.81 % (228420)------------------------------
% 223.99/31.81 % (228420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228420)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228420)Termination reason: Instruction limit
% 223.99/31.81 % (228420)Termination phase: Finite model building constraint generation
% 223.99/31.81 % (228420)Time elapsed: 3.240 s
% 223.99/31.81 % (228420)Peak memory usage: 588 MB
% 223.99/31.81 % (228420)Instructions burned: 9520 (million)
% 223.99/31.81 % (228428)Instruction limit reached!
% 223.99/31.81 % (228428)------------------------------
% 223.99/31.81 % (228428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228428)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228428)Termination reason: Instruction limit
% 223.99/31.81 % (228428)Termination phase: Finite model building constraint generation
% 223.99/31.81 % (228428)Time elapsed: 2.209 s
% 223.99/31.81 % (228428)Peak memory usage: 411 MB
% 223.99/31.81 % (228428)Instructions burned: 6326 (million)
% 223.99/31.81 % (228433)ott-2_1_sil=16000:newcnf=on:random_seed=3573682501:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 223.99/31.81 % (228434)ott+10_1_sil=32000:tgt=ground:random_seed=3475547521:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 223.99/31.81 % (228430)Instruction limit reached!
% 223.99/31.81 % (228430)------------------------------
% 223.99/31.81 % (228430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228430)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228430)Termination reason: Instruction limit
% 223.99/31.81 % (228430)Termination phase: Finite model building constraint generation
% 223.99/31.81 % (228430)Time elapsed: 0.750 s
% 223.99/31.81 % (228430)Peak memory usage: 138 MB
% 223.99/31.81 % (228430)Instructions burned: 2176 (million)
% 223.99/31.81 % (228437)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3701394236:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 223.99/31.81 % TRYING [1]
% 223.99/31.81 % TRYING [2]
% 223.99/31.81 % TRYING [3]
% 223.99/31.81 % TRYING [4]
% 223.99/31.81 % TRYING [9]
% 223.99/31.81 % TRYING [5]
% 223.99/31.81 % TRYING [9]
% 223.99/31.81 % (228433)Instruction limit reached!
% 223.99/31.81 % (228433)------------------------------
% 223.99/31.81 % (228433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228433)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228433)Termination reason: Instruction limit
% 223.99/31.81 % (228433)Termination phase: Saturation
% 223.99/31.81 % (228433)Time elapsed: 0.454 s
% 223.99/31.81 % (228433)Peak memory usage: 26 MB
% 223.99/31.81 % (228433)Instructions burned: 871 (million)
% 223.99/31.81 % TRYING [6]
% 223.99/31.81 % (228439)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1426764861:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 223.99/31.81 % TRYING [7]
% 223.99/31.81 % (228418)Instruction limit reached!
% 223.99/31.81 % (228418)------------------------------
% 223.99/31.81 % (228418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.99/31.81 % (228418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.99/31.81 % (228418)CaDiCaL version: 2.1.3
% 223.99/31.81 % (228418)Termination reason: Instruction limit
% 223.99/31.81 % (228418)Termination phase: Finite model building constraint generation
% 223.99/31.81 % (228418)Time elapsed: 4.819 s
% 223.99/31.81 % (228418)Peak memory usage: 247 MB
% 223.99/31.81 % (228418)Instructions burned: 22065 (million)
% 223.99/31.81 % (228441)dis+21_1_sil=32000:sas=cadical:random_seed=1065664269:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 223.99/31.81 % TRYING [8]
% 223.99/31.81 % (228441)Instruction limit reached!
% 223.99/31.81 % (228441)------------------------------
% 203.22/41.18 % (228441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228441)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228441)Termination reason: Instruction limit
% 203.22/41.18 % (228441)Termination phase: Saturation
% 203.22/41.18 % (228441)Time elapsed: 1.066 s
% 203.22/41.18 % (228441)Peak memory usage: 40 MB
% 203.22/41.18 % (228441)Instructions burned: 3774 (million)
% 203.22/41.18 % (228443)ott+11_1_sil=16000:gs=on:random_seed=3771427388:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 203.22/41.18 % (228439)Instruction limit reached!
% 203.22/41.18 % (228439)------------------------------
% 203.22/41.18 % (228439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228439)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228439)Termination reason: Instruction limit
% 203.22/41.18 % (228439)Termination phase: Saturation
% 203.22/41.18 % (228439)Time elapsed: 1.807 s
% 203.22/41.18 % (228439)Peak memory usage: 43 MB
% 203.22/41.18 % (228439)Instructions burned: 3513 (million)
% 203.22/41.18 % (228445)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4171056658:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi)
% 203.22/41.18 % TRYING [7]
% 203.22/41.18 % (228434)Instruction limit reached!
% 203.22/41.18 % (228434)------------------------------
% 203.22/41.18 % (228434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228434)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228434)Termination reason: Instruction limit
% 203.22/41.18 % (228434)Termination phase: Saturation
% 203.22/41.18 % (228434)Time elapsed: 2.738 s
% 203.22/41.18 % (228434)Peak memory usage: 54 MB
% 203.22/41.18 % (228434)Instructions burned: 5116 (million)
% 203.22/41.18 % (228447)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2897689703:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 203.22/41.18 % (228443)Instruction limit reached!
% 203.22/41.18 % (228443)------------------------------
% 203.22/41.18 % (228443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228443)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228443)Termination reason: Instruction limit
% 203.22/41.18 % (228443)Termination phase: Saturation
% 203.22/41.18 % (228443)Time elapsed: 0.533 s
% 203.22/41.18 % (228443)Peak memory usage: 19 MB
% 203.22/41.18 % (228443)Instructions burned: 2256 (million)
% 203.22/41.18 % (228449)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1653429223:i=29340_2929 on theBenchmark for (2929ds/29340Mi)
% 203.22/41.18 % TRYING [8]
% 203.22/41.18 % TRYING [9]
% 203.22/41.18 % (228447)Instruction limit reached!
% 203.22/41.18 % (228447)------------------------------
% 203.22/41.18 % (228447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228447)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228447)Termination reason: Instruction limit
% 203.22/41.18 % (228447)Termination phase: Saturation
% 203.22/41.18 % (228447)Time elapsed: 2.131 s
% 203.22/41.18 % (228447)Peak memory usage: 54 MB
% 203.22/41.18 % (228447)Instructions burned: 4592 (million)
% 203.22/41.18 % (228451)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3270056704:i=5211_2908 on theBenchmark for (2908ds/5211Mi)
% 203.22/41.18 % TRYING [10]
% 203.22/41.18 % (228451)Instruction limit reached!
% 203.22/41.18 % (228451)------------------------------
% 203.22/41.18 % (228451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228451)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228451)Termination reason: Instruction limit
% 203.22/41.18 % (228451)Termination phase: Saturation
% 203.22/41.18 % (228451)Time elapsed: 2.383 s
% 203.22/41.18 % (228451)Peak memory usage: 51 MB
% 203.22/41.18 % (228451)Instructions burned: 5213 (million)
% 203.22/41.18 % (228453)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2765711539:i=5497:nm=2_2884 on theBenchmark for (2884ds/5497Mi)
% 203.22/41.18 % TRYING [17]
% 203.22/41.18 % TRYING [9]
% 203.22/41.18 % TRYING [10]
% 203.22/41.18 % (228453)Instruction limit reached!
% 203.22/41.18 % (228453)------------------------------
% 203.22/41.18 % (228453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228453)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228453)Termination reason: Instruction limit
% 203.22/41.18 % (228453)Termination phase: Finite model building constraint generation
% 203.22/41.18 % (228453)Time elapsed: 1.864 s
% 203.22/41.18 % (228453)Peak memory usage: 344 MB
% 203.22/41.18 % (228453)Instructions burned: 5501 (million)
% 203.22/41.18 % (228455)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3627549411:fmbsr=2:i=46332_2864 on theBenchmark for (2864ds/46332Mi)
% 203.22/41.18 % TRYING [15]
% 203.22/41.18 % (228449)Instruction limit reached!
% 203.22/41.18 % (228449)------------------------------
% 203.22/41.18 % (228449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228449)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228449)Termination reason: Instruction limit
% 203.22/41.18 % (228449)Termination phase: Saturation
% 203.22/41.18 % (228449)Time elapsed: 7.582 s
% 203.22/41.18 % (228449)Peak memory usage: 413 MB
% 203.22/41.18 % (228449)Instructions burned: 29340 (million)
% 203.22/41.18 % (228457)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3993233588:i=14071_2852 on theBenchmark for (2852ds/14071Mi)
% 203.22/41.18 % TRYING [12]
% 203.22/41.18 % (228457)Instruction limit reached!
% 203.22/41.18 % (228457)------------------------------
% 203.22/41.18 % (228457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228457)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228457)Termination reason: Instruction limit
% 203.22/41.18 % (228457)Termination phase: Finite model building constraint generation
% 203.22/41.18 % (228457)Time elapsed: 3.087 s
% 203.22/41.18 % (228457)Peak memory usage: 819 MB
% 203.22/41.18 % (228457)Instructions burned: 14072 (million)
% 203.22/41.18 % (228459)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=171759754:i=22565:add=on:rawr=on_2821 on theBenchmark for (2821ds/22565Mi)
% 203.22/41.18 % TRYING [11]
% 203.22/41.18 % TRYING [10]
% 203.22/41.18 % TRYING [11]
% 203.22/41.18 % (228459)Instruction limit reached!
% 203.22/41.18 % (228459)------------------------------
% 203.22/41.18 % (228459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228459)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228459)Termination reason: Instruction limit
% 203.22/41.18 % (228459)Termination phase: Saturation
% 203.22/41.18 % (228459)Time elapsed: 7.185 s
% 203.22/41.18 % (228459)Peak memory usage: 200 MB
% 203.22/41.18 % (228459)Instructions burned: 22569 (million)
% 203.22/41.18 % (228461)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2219671910:i=8173:av=off_2749 on theBenchmark for (2749ds/8173Mi)
% 203.22/41.18 % (228461)Instruction limit reached!
% 203.22/41.18 % (228461)------------------------------
% 203.22/41.18 % (228461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228461)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228461)Termination reason: Instruction limit
% 203.22/41.18 % (228461)Termination phase: Saturation
% 203.22/41.18 % (228461)Time elapsed: 2.099 s
% 203.22/41.18 % (228461)Peak memory usage: 77 MB
% 203.22/41.18 % (228461)Instructions burned: 8175 (million)
% 203.22/41.18 % (228463)dis+10_16:1_sil=16000:random_seed=1795038206:i=9155:fsr=off_2728 on theBenchmark for (2728ds/9155Mi)
% 203.22/41.18 % (228463)Instruction limit reached!
% 203.22/41.18 % (228463)------------------------------
% 203.22/41.18 % (228463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228463)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228463)Termination reason: Instruction limit
% 203.22/41.18 % (228463)Termination phase: Saturation
% 203.22/41.18 % (228463)Time elapsed: 2.469 s
% 203.22/41.18 % (228463)Peak memory usage: 83 MB
% 203.22/41.18 % (228463)Instructions burned: 9158 (million)
% 203.22/41.18 % (228465)ott-3_8_sil=64000:random_seed=1058351199:i=20139:bs=on_2703 on theBenchmark for (2703ds/20139Mi)
% 203.22/41.18 % (228455)Instruction limit reached!
% 203.22/41.18 % (228455)------------------------------
% 203.22/41.18 % (228455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228455)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228455)Termination reason: Instruction limit
% 203.22/41.18 % (228455)Termination phase: Finite model building constraint generation
% 203.22/41.18 % (228455)Time elapsed: 18.051 s
% 203.22/41.18 % (228455)Peak memory usage: 2485 MB
% 203.22/41.18 % (228455)Instructions burned: 46332 (million)
% 203.22/41.18 % (228437)Instruction limit reached!
% 203.22/41.18 % (228437)------------------------------
% 203.22/41.18 % (228437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228437)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228437)Termination reason: Instruction limit
% 203.22/41.18 % (228437)Termination phase: Finite model building SAT solving
% 203.22/41.18 % (228437)Time elapsed: 27.384 s
% 203.22/41.18 % (228437)Peak memory usage: 1090 MB
% 203.22/41.18 % (228437)Instructions burned: 54282 (million)
% 203.22/41.18 % (228467)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3203260326:fmbsr=2:i=32576_2680 on theBenchmark for (2680ds/32576Mi)
% 203.22/41.18 % TRYING [9]
% 203.22/41.18 % (228469)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=980080987:i=11404_2680 on theBenchmark for (2680ds/11404Mi)
% 203.22/41.18 % TRYING [11]
% 203.22/41.18 % (228445)Instruction limit reached!
% 203.22/41.18 % (228445)------------------------------
% 203.22/41.18 % (228445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228445)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228445)Termination reason: Instruction limit
% 203.22/41.18 % (228445)Termination phase: Finite model building constraint generation
% 203.22/41.18 % (228445)Time elapsed: 27.773 s
% 203.22/41.18 % (228445)Peak memory usage: 402 MB
% 203.22/41.18 % (228445)Instructions burned: 67534 (million)
% 203.22/41.18 % (228471)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1169900541:i=14134_2656 on theBenchmark for (2656ds/14134Mi)
% 203.22/41.18 % (228465)Instruction limit reached!
% 203.22/41.18 % (228465)------------------------------
% 203.22/41.18 % (228465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228465)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228465)Termination reason: Instruction limit
% 203.22/41.18 % (228465)Termination phase: Saturation
% 203.22/41.18 % (228465)Time elapsed: 6.588 s
% 203.22/41.18 % (228465)Peak memory usage: 176 MB
% 203.22/41.18 % (228465)Instructions burned: 20143 (million)
% 203.22/41.18 % (228473)dis+33_16_sil=32000:sac=on:random_seed=2757475986:i=15851:nm=0_2636 on theBenchmark for (2636ds/15851Mi)
% 203.22/41.18 % (228469)Instruction limit reached!
% 203.22/41.18 % (228469)------------------------------
% 203.22/41.18 % (228469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.18 % (228469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.18 % (228469)CaDiCaL version: 2.1.3
% 203.22/41.18 % (228469)Termination reason: Instruction limit
% 203.22/41.18 % (228469)Termination phase: Saturation
% 203.22/41.18 % (228469)Time elapsed: 4.809 s
% 203.22/41.18 % (228469)Peak memory usage: 84 MB
% 203.22/41.18 % (228469)Instructions burned: 11404 (million)
% 203.22/41.18 % (228475)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1944359281:avsq=on:i=17627:add=on:amm=off_2631 on theBenchmark for (2631ds/17627Mi)
% 203.22/41.18 % (228471) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-228379-228471"...
% 203.22/41.18 % (228471)...printing done.
% 203.22/41.18 % (228471)Refutation found. Thanks to Tanya!
% 203.22/41.18 % SZS status Unsatisfiable for theBenchmark
% 203.22/41.18 % SZS output start Proof for theBenchmark
% See solution above
% 203.22/41.19 % (228471)------------------------------
% 203.22/41.19 % (228471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 203.22/41.19 % (228471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.22/41.19 % (228471)CaDiCaL version: 2.1.3
% 203.22/41.19 % (228471)Termination reason: Refutation
% 203.22/41.19 % (228471)Time elapsed: 6.407 s
% 203.22/41.19 % (228471)Peak memory usage: 147 MB
% 203.22/41.19 % (228471)Instructions burned: 11705 (million)
% 203.22/41.19 % (228379)Success in time 40.966 s
% 203.22/41.19 % Vampire exiting
%------------------------------------------------------------------------------