%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC113-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 : n019.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:04:43 PM UTC 2026
% Result : Unsatisfiable 250.12s 41.60s
% Output : Refutation 250.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 36
% Syntax : Number of formulae : 139 ( 15 unt; 10 def)
% Number of atoms : 403 ( 47 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 505 ( 241 ~; 254 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 11 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 63 ( 0 sgn 63 !; 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(f56,axiom,
! [X0] :
( segmentP(X0,nil)
| ~ ssList(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause56) ).
fof(f71,axiom,
! [X0] :
( ~ memberP(nil,X0)
| ~ ssItem(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause71) ).
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(f98,axiom,
! [X0,X1] :
( cons(X0,X1) != nil
| ~ ssItem(X0)
| ~ ssList(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause98) ).
fof(f99,plain,
! [X0,X1] :
( nil != cons(X0,X1)
| ~ ssItem(X0)
| ~ ssList(X1) ),
inference(reorient_equations,[],[f98]) ).
fof(f101,axiom,
! [X0,X1] :
( ~ ssList(X0)
| ~ ssList(X1)
| neq(X1,X0)
| X1 = X0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWC001-0.ax',clause100) ).
fof(f102,plain,
! [X0,X1] :
( neq(X1,X0)
| ~ ssList(X1)
| ~ ssList(X0)
| X0 = X1 ),
inference(reorient_equations,[],[f101]) ).
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,
( ssItem(sk5)
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_7) ).
fof(f207,negated_conjecture,
( ssItem(sk5)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_8) ).
fof(f208,negated_conjecture,
( cons(sk5,nil) = sk3
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_9) ).
fof(f209,plain,
( sk3 = cons(sk5,nil)
| nil = sk4 ),
inference(reorient_equations,[],[f208]) ).
fof(f210,negated_conjecture,
( memberP(sk4,sk5)
| nil = sk4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_10) ).
fof(f213,negated_conjecture,
( memberP(sk4,sk5)
| nil = sk3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_12) ).
fof(f215,negated_conjecture,
( nil = sk2
| ~ neq(sk1,nil)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_14) ).
fof(f216,negated_conjecture,
( nil != sk1
| neq(sk2,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_15) ).
fof(f217,negated_conjecture,
( nil != sk1
| ~ neq(sk1,nil)
| ~ segmentP(sk2,sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1_16) ).
fof(f221,plain,
( nil = sk4
| ~ neq(sk3,nil)
| ~ segmentP(sk4,sk3) ),
inference(definition_unfolding,[],[f215,f204,f205,f204,f205]) ).
fof(f222,plain,
( nil != sk3
| neq(sk4,nil) ),
inference(definition_unfolding,[],[f216,f205,f204]) ).
fof(f223,plain,
( nil != sk3
| ~ neq(sk3,nil)
| ~ segmentP(sk4,sk3) ),
inference(definition_unfolding,[],[f217,f205,f205,f204,f205]) ).
fof(f238,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(f255,definition,
( spl0_1
<=> nil = sk4 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f257,plain,
( nil = sk4
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f259,definition,
( spl0_2
<=> ssItem(sk5) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f261,plain,
( ssItem(sk5)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f206,f259,f255]) ).
fof(f264,definition,
( spl0_3
<=> nil = sk3 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f265,plain,
( nil != sk3
| spl0_3 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f266,plain,
( nil = sk3
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f264]) ).
fof(f267,plain,
( spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f207,f259,f264]) ).
fof(f269,definition,
( spl0_4
<=> memberP(sk4,sk5) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f271,plain,
( memberP(sk4,sk5)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f272,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f210,f269,f255]) ).
fof(f273,plain,
( spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f213,f269,f264]) ).
fof(f275,definition,
( spl0_5
<=> neq(sk4,nil) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f277,plain,
( neq(sk4,nil)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,plain,
( spl0_5
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f222,f264,f275]) ).
fof(f281,definition,
( spl0_6
<=> sk3 = cons(sk5,nil) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f283,plain,
( sk3 = cons(sk5,nil)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f284,plain,
( spl0_1
| spl0_6 ),
inference(avatar_split_clause,[],[f209,f281,f255]) ).
fof(f285,plain,
( neq(nil,nil)
| ~ spl0_1
| ~ spl0_5 ),
inference(superposition,[],[f277,f257]) ).
fof(f286,plain,
( memberP(nil,sk5)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f271,f257]) ).
fof(f291,definition,
( spl0_7
<=> segmentP(sk4,sk3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f293,plain,
( ~ segmentP(sk4,sk3)
| spl0_7 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl0_8
<=> neq(sk3,nil) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f297,plain,
( ~ neq(sk3,nil)
| spl0_8 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f298,plain,
( ~ spl0_7
| ~ spl0_8
| spl0_1 ),
inference(avatar_split_clause,[],[f221,f255,f295,f291]) ).
fof(f299,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f223,f264,f295,f291]) ).
fof(f300,plain,
( ~ segmentP(sk4,nil)
| ~ spl0_3
| spl0_7 ),
inference(forward_demodulation,[],[f293,f266]) ).
fof(f301,plain,
( ~ segmentP(nil,nil)
| ~ spl0_1
| ~ spl0_3
| spl0_7 ),
inference(forward_demodulation,[],[f300,f257]) ).
fof(f302,plain,
( ~ ssList(nil)
| ~ spl0_1
| ~ spl0_3
| spl0_7 ),
inference(resolution,[],[f56,f301]) ).
fof(f303,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f302,f8]) ).
fof(f304,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_contradiction_clause,[],[f303]) ).
fof(f306,plain,
( ~ neq(nil,nil)
| ~ spl0_3
| spl0_8 ),
inference(forward_demodulation,[],[f297,f266]) ).
fof(f308,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f306,f285]) ).
fof(f309,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| spl0_8 ),
inference(avatar_contradiction_clause,[],[f308]) ).
fof(f311,plain,
( ~ ssItem(sk5)
| ~ spl0_1
| ~ spl0_4 ),
inference(resolution,[],[f71,f286]) ).
fof(f312,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f311,f261]) ).
fof(f313,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f385,plain,
sk4 = app(sk4,nil),
inference(resolution,[],[f73,f203]) ).
fof(f414,plain,
sk3 = app(nil,sk3),
inference(resolution,[],[f74,f202]) ).
fof(f476,plain,
( nil != sk3
| ~ ssItem(sk5)
| ~ ssList(nil)
| ~ spl0_6 ),
inference(superposition,[],[f99,f283]) ).
fof(f477,plain,
( nil != sk3
| ~ ssList(nil)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f476,f261]) ).
fof(f478,plain,
( nil != sk3
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f477,f8]) ).
fof(f479,plain,
( ~ spl0_3
| ~ spl0_2
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f478,f281,f259,f264]) ).
fof(f683,plain,
( ~ ssList(sk3)
| ~ ssList(nil)
| nil = sk3
| spl0_8 ),
inference(resolution,[],[f102,f297]) ).
fof(f688,plain,
( ~ ssList(nil)
| nil = sk3
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f683,f202]) ).
fof(f689,plain,
( nil = sk3
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f688,f8]) ).
fof(f690,plain,
( $false
| spl0_3
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f689,f265]) ).
fof(f691,plain,
( spl0_3
| spl0_8 ),
inference(avatar_contradiction_clause,[],[f690]) ).
fof(f914,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(cons(sk5,nil),X0) )
| ~ spl0_2 ),
inference(resolution,[],[f126,f261]) ).
fof(f975,plain,
( ! [X0] :
( ~ ssList(X0)
| cons(sk5,X0) = app(sk3,X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_demodulation,[],[f914,f283]) ).
fof(f1643,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ ssList(sk3)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ segmentP(sk4,X0) )
| spl0_7 ),
inference(resolution,[],[f164,f293]) ).
fof(f1649,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ ssList(X0)
| ~ ssList(sk4)
| ~ segmentP(sk4,X0) )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1643,f202]) ).
fof(f1651,plain,
( ! [X0] :
( ~ segmentP(X0,sk3)
| ~ segmentP(sk4,X0)
| ~ ssList(X0) )
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f1649,f203]) ).
fof(f2493,plain,
( ~ ssItem(sk5)
| ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_4 ),
inference(resolution,[],[f182,f271]) ).
fof(f2504,plain,
( ~ ssList(sk4)
| sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2493,f261]) ).
fof(f2516,plain,
( sk4 = app(skaf42(sk4,sk5),cons(sk5,skaf43(sk5,sk4)))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2504,f203]) ).
fof(f2825,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(app(sk3,X0))
| ~ ssList(X0) ),
inference(superposition,[],[f238,f414]) ).
fof(f2833,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(nil)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2825,f85]) ).
fof(f2861,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2833,f8]) ).
fof(f2888,plain,
! [X0] :
( segmentP(app(sk3,X0),sk3)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[],[f2861,f202]) ).
fof(f3255,plain,
( ! [X0,X1] : cons(sk5,skaf43(X0,X1)) = app(sk3,skaf43(X0,X1))
| ~ spl0_2
| ~ spl0_6 ),
inference(resolution,[],[f975,f52]) ).
fof(f3608,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_4 ),
inference(superposition,[],[f238,f2516]) ).
fof(f3609,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_4 ),
inference(forward_subsumption_resolution,[],[f3608,f53]) ).
fof(f86427,plain,
( ! [X0,X1] :
( segmentP(cons(sk5,skaf43(X0,X1)),sk3)
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[],[f2888,f3255]) ).
fof(f86428,plain,
( ! [X0,X1] :
( ssList(cons(sk5,skaf43(X0,X1)))
| ~ ssList(sk3)
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_6 ),
inference(superposition,[],[f85,f3255]) ).
fof(f86471,plain,
( ! [X0,X1] :
( ssList(cons(sk5,skaf43(X0,X1)))
| ~ ssList(skaf43(X0,X1)) )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f86428,f202]) ).
fof(f86472,plain,
( ! [X0,X1] : segmentP(cons(sk5,skaf43(X0,X1)),sk3)
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f86427,f52]) ).
fof(f86496,plain,
( ! [X0,X1] : ssList(cons(sk5,skaf43(X0,X1)))
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f86471,f52]) ).
fof(f96318,definition,
( spl0_66
<=> ssList(cons(sk5,skaf43(sk5,sk4))) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f96320,plain,
( ~ ssList(cons(sk5,skaf43(sk5,sk4)))
| spl0_66 ),
inference(avatar_component_clause,[],[f96318]) ).
fof(f96326,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f96320,f86496]) ).
fof(f96327,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f96326]) ).
fof(f97417,plain,
( ! [X0,X1] :
( ~ segmentP(sk4,cons(sk5,skaf43(X0,X1)))
| ~ ssList(cons(sk5,skaf43(X0,X1))) )
| ~ spl0_2
| ~ spl0_6
| spl0_7 ),
inference(resolution,[],[f86472,f1651]) ).
fof(f97435,plain,
( ! [X0,X1] : ~ segmentP(sk4,cons(sk5,skaf43(X0,X1)))
| ~ spl0_2
| ~ spl0_6
| spl0_7 ),
inference(forward_subsumption_resolution,[],[f97417,f86496]) ).
fof(f221729,definition,
( spl0_130
<=> ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f221730,plain,
( ! [X0] :
( segmentP(app(sk4,X0),cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(X0)
| ~ ssList(app(sk4,X0)) )
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f221729]) ).
fof(f221731,plain,
( ~ spl0_66
| spl0_130
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f3609,f269,f259,f221729,f96318]) ).
fof(f221746,plain,
( segmentP(sk4,cons(sk5,skaf43(sk5,sk4)))
| ~ ssList(nil)
| ~ ssList(sk4)
| ~ spl0_130 ),
inference(superposition,[],[f221730,f385]) ).
fof(f221760,plain,
( ~ ssList(nil)
| ~ ssList(sk4)
| ~ spl0_2
| ~ spl0_6
| spl0_7
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f221746,f97435]) ).
fof(f221767,plain,
( ~ ssList(sk4)
| ~ spl0_2
| ~ spl0_6
| spl0_7
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f221760,f8]) ).
fof(f221771,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| spl0_7
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f221767,f203]) ).
fof(f221772,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_7
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f221771]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f262]) ).
cnf(s2,plain,
( spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f267]) ).
cnf(s3,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f272]) ).
cnf(s4,plain,
( spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f273]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f279]) ).
cnf(s7,plain,
( spl0_1
| spl0_6 ),
inference(sat_conversion,[],[f284]) ).
cnf(s9,plain,
( spl0_1
| ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f298]) ).
cnf(s10,plain,
( ~ spl0_3
| ~ spl0_7
| ~ spl0_8 ),
inference(sat_conversion,[],[f299]) ).
cnf(s11,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f304]) ).
cnf(s12,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5
| spl0_8 ),
inference(sat_conversion,[],[f309]) ).
cnf(s13,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_4 ),
inference(sat_conversion,[],[f313]) ).
cnf(s23,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_6 ),
inference(sat_conversion,[],[f479]) ).
cnf(s24,plain,
( spl0_3
| spl0_8 ),
inference(sat_conversion,[],[f691]) ).
cnf(s77,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_66 ),
inference(sat_conversion,[],[f96327]) ).
cnf(s190,plain,
( ~ spl0_2
| ~ spl0_4
| ~ spl0_66
| spl0_130 ),
inference(sat_conversion,[],[f221731]) ).
cnf(s192,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_7
| ~ spl0_130 ),
inference(sat_conversion,[],[f221772]) ).
cnf(s213,plain,
spl0_1,
inference(rat,[],[s9,s192,s24,s190,s23,s77,s1,s3,s7]) ).
cnf(s214,plain,
~ spl0_3,
inference(rat,[],[s12,s10,s6,s11,s213]) ).
cnf(s221,plain,
spl0_4,
inference(rat,[],[s4,s214]) ).
cnf(s222,plain,
spl0_2,
inference(rat,[],[s2,s214]) ).
cnf(s230,plain,
$false,
inference(rat,[],[s13,s213,s221,s222]) ).
fof(f221773,plain,
$false,
inference(avatar_sat_refutation,[],[s230]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC113-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.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 07:55:48 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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
% 13.26/2.39 % (3843850)Will run a generic schedule for satisfiability detection.
% 13.26/2.39 % (3843859)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3399544260:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.26/2.39 % (3843856)% WARNING: option uhcvi not known.
% 13.26/2.39 % (3843855)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1828243348_2999 on theBenchmark for (2999ds/0Mi)
% 13.26/2.39 % (3843857)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1282345626:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.26/2.39 % (3843856)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2368289022:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.26/2.39 % (3843858)dis+10_1_sil=32000:sp=arity:random_seed=1450594818:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.26/2.39 % (3843861)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2571211885:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.26/2.39 % (3843860)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3036240100:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.39 % TRYING [1]
% 13.26/2.39 % TRYING [2]
% 13.26/2.39 % TRYING [3]
% 13.26/2.39 % (3843859)Instruction limit reached!
% 13.26/2.39 % (3843859)------------------------------
% 13.26/2.39 % (3843859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.39 % (3843859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.39 % (3843859)CaDiCaL version: 2.1.3
% 13.26/2.39 % (3843859)Termination reason: Instruction limit
% 13.26/2.39 % (3843859)Termination phase: Saturation
% 13.26/2.39 % (3843859)Time elapsed: 0.035 s
% 13.26/2.39 % (3843859)Peak memory usage: 13 MB
% 13.26/2.39 % (3843859)Instructions burned: 119 (million)
% 13.26/2.39 % TRYING [4]
% 13.26/2.39 % (3843869)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2418849939:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.26/2.39 % TRYING [1]
% 13.26/2.39 % TRYING [2]
% 13.26/2.39 % TRYING [3]
% 13.26/2.39 % TRYING [4]
% 13.26/2.39 % (3843858)Instruction limit reached!
% 13.26/2.39 % (3843858)------------------------------
% 13.26/2.39 % (3843858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.39 % (3843858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.39 % (3843858)CaDiCaL version: 2.1.3
% 13.26/2.39 % (3843858)Termination reason: Instruction limit
% 13.26/2.39 % (3843858)Termination phase: Saturation
% 13.26/2.39 % (3843858)Time elapsed: 0.060 s
% 13.26/2.39 % (3843858)Peak memory usage: 13 MB
% 13.26/2.39 % (3843858)Instructions burned: 103 (million)
% 13.26/2.39 % (3843860)Instruction limit reached!
% 13.26/2.39 % (3843860)------------------------------
% 13.26/2.39 % (3843860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.39 % (3843860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.39 % (3843860)CaDiCaL version: 2.1.3
% 13.26/2.39 % (3843860)Termination reason: Instruction limit
% 13.26/2.39 % (3843860)Termination phase: Saturation
% 13.26/2.39 % (3843860)Time elapsed: 0.070 s
% 13.26/2.39 % (3843860)Peak memory usage: 14 MB
% 13.26/2.39 % (3843860)Instructions burned: 133 (million)
% 13.26/2.39 % (3843871)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3082135784:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.26/2.39 % (3843861)Instruction limit reached!
% 13.26/2.39 % (3843861)------------------------------
% 13.26/2.39 % (3843861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.39 % (3843861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.39 % (3843861)CaDiCaL version: 2.1.3
% 13.26/2.39 % (3843861)Termination reason: Instruction limit
% 13.26/2.39 % (3843861)Termination phase: Saturation
% 13.26/2.39 % (3843861)Time elapsed: 0.090 s
% 13.26/2.39 % (3843861)Peak memory usage: 14 MB
% 13.26/2.39 % (3843861)Instructions burned: 159 (million)
% 13.26/2.39 % (3843872)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=1726373900:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.26/2.39 % TRYING [5]
% 13.26/2.39 % TRYING [5]
% 13.26/2.39 % (3843875)ott-21_1_sil=16000:fs=off:random_seed=3159269753:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.26/2.39 % (3843871)Instruction limit reached!
% 13.26/2.39 % (3843871)------------------------------
% 13.26/2.39 % (3843871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843871)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843871)Termination reason: Instruction limit
% 37.42/5.84 % (3843871)Termination phase: Saturation
% 37.42/5.84 % (3843871)Time elapsed: 0.073 s
% 37.42/5.84 % (3843871)Peak memory usage: 14 MB
% 37.42/5.84 % (3843871)Instructions burned: 132 (million)
% 37.42/5.84 % (3843877)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1814114620:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 37.42/5.84 % TRYING [6]
% 37.42/5.84 % (3843869)Instruction limit reached!
% 37.42/5.84 % (3843869)------------------------------
% 37.42/5.84 % (3843869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843869)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843869)Termination reason: Instruction limit
% 37.42/5.84 % (3843869)Termination phase: Finite model building constraint generation
% 37.42/5.84 % (3843869)Time elapsed: 0.151 s
% 37.42/5.84 % (3843869)Peak memory usage: 36 MB
% 37.42/5.84 % (3843869)Instructions burned: 718 (million)
% 37.42/5.84 % (3843875)Instruction limit reached!
% 37.42/5.84 % (3843875)------------------------------
% 37.42/5.84 % (3843875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843875)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843875)Termination reason: Instruction limit
% 37.42/5.84 % (3843875)Termination phase: Saturation
% 37.42/5.84 % (3843875)Time elapsed: 0.088 s
% 37.42/5.84 % (3843875)Peak memory usage: 13 MB
% 37.42/5.84 % (3843875)Instructions burned: 181 (million)
% 37.42/5.84 % (3843879)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2202327163:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.42/5.84 % TRYING [1]
% 37.42/5.84 % TRYING [2]
% 37.42/5.84 % TRYING [3]
% 37.42/5.84 % (3843880)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3007163739:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 37.42/5.84 % TRYING [4]
% 37.42/5.84 % TRYING [6]
% 37.42/5.84 % TRYING [5]
% 37.42/5.84 % (3843879)Instruction limit reached!
% 37.42/5.84 % (3843879)------------------------------
% 37.42/5.84 % (3843879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843879)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843879)Termination reason: Instruction limit
% 37.42/5.84 % (3843879)Termination phase: Finite model building SAT solving
% 37.42/5.84 % (3843879)Time elapsed: 0.178 s
% 37.42/5.84 % (3843879)Peak memory usage: 23 MB
% 37.42/5.84 % (3843879)Instructions burned: 867 (million)
% 37.42/5.84 % (3843883)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=557346228:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.42/5.84 % TRYING [14]
% 37.42/5.84 % (3843877)Instruction limit reached!
% 37.42/5.84 % (3843877)------------------------------
% 37.42/5.84 % (3843877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843877)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843877)Termination reason: Instruction limit
% 37.42/5.84 % (3843877)Termination phase: Saturation
% 37.42/5.84 % (3843877)Time elapsed: 0.300 s
% 37.42/5.84 % (3843877)Peak memory usage: 14 MB
% 37.42/5.84 % (3843877)Instructions burned: 478 (million)
% 37.42/5.84 % (3843872)Instruction limit reached!
% 37.42/5.84 % (3843872)------------------------------
% 37.42/5.84 % (3843872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.42/5.84 % (3843872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.42/5.84 % (3843872)CaDiCaL version: 2.1.3
% 37.42/5.84 % (3843872)Termination reason: Instruction limit
% 37.42/5.84 % (3843872)Termination phase: Saturation
% 37.42/5.84 % (3843872)Time elapsed: 0.384 s
% 37.42/5.84 % (3843872)Peak memory usage: 16 MB
% 37.42/5.84 % (3843872)Instructions burned: 685 (million)
% 37.42/5.84 % (3843885)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=745132443: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)
% 37.42/5.84 % (3843886)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=288350939:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 37.42/5.84 % (3843883)Instruction limit reached!
% 81.36/11.90 % (3843883)------------------------------
% 81.36/11.90 % (3843883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.90 % (3843883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.90 % (3843883)CaDiCaL version: 2.1.3
% 81.36/11.90 % (3843883)Termination reason: Instruction limit
% 81.36/11.90 % (3843883)Termination phase: Finite model building constraint generation
% 81.36/11.90 % (3843883)Time elapsed: 0.178 s
% 81.36/11.90 % (3843883)Peak memory usage: 73 MB
% 81.36/11.90 % (3843883)Instructions burned: 895 (million)
% 81.36/11.90 % (3843889)fmb+10_1_sil=64000:random_seed=3035191853:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 81.36/11.90 % TRYING [1]
% 81.36/11.90 % TRYING [2]
% 81.36/11.90 % TRYING [3]
% 81.36/11.90 % TRYING [4]
% 81.36/11.90 % TRYING [5]
% 81.36/11.90 % TRYING [7]
% 81.36/11.90 % (3843885)Instruction limit reached!
% 81.36/11.90 % (3843885)------------------------------
% 81.36/11.90 % (3843885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.90 % (3843885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.90 % (3843885)CaDiCaL version: 2.1.3
% 81.36/11.91 % (3843885)Termination reason: Instruction limit
% 81.36/11.91 % (3843885)Termination phase: Saturation
% 81.36/11.91 % (3843885)Time elapsed: 0.377 s
% 81.36/11.91 % (3843885)Peak memory usage: 19 MB
% 81.36/11.91 % (3843885)Instructions burned: 692 (million)
% 81.36/11.91 % (3843880)Instruction limit reached!
% 81.36/11.91 % (3843880)------------------------------
% 81.36/11.91 % (3843880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.91 % (3843880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.91 % (3843880)CaDiCaL version: 2.1.3
% 81.36/11.91 % (3843880)Termination reason: Instruction limit
% 81.36/11.91 % (3843880)Termination phase: Saturation
% 81.36/11.91 % (3843880)Time elapsed: 0.665 s
% 81.36/11.91 % (3843880)Peak memory usage: 29 MB
% 81.36/11.91 % (3843880)Instructions burned: 1180 (million)
% 81.36/11.91 % (3843891)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=573975911:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 81.36/11.91 % TRYING [20]
% 81.36/11.91 % (3843892)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=727291583:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 81.36/11.91 % TRYING [8]
% 81.36/11.91 % TRYING [6]
% 81.36/11.91 % (3843886)Instruction limit reached!
% 81.36/11.91 % (3843886)------------------------------
% 81.36/11.91 % (3843886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.91 % (3843886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.91 % (3843886)CaDiCaL version: 2.1.3
% 81.36/11.91 % (3843886)Termination reason: Instruction limit
% 81.36/11.91 % (3843886)Termination phase: Saturation
% 81.36/11.91 % (3843886)Time elapsed: 0.457 s
% 81.36/11.91 % (3843886)Peak memory usage: 21 MB
% 81.36/11.91 % (3843886)Instructions burned: 880 (million)
% 81.36/11.91 % (3843895)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1115634027:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 81.36/11.91 % (3843892)Instruction limit reached!
% 81.36/11.91 % (3843892)------------------------------
% 81.36/11.91 % (3843892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.91 % (3843892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.91 % (3843892)CaDiCaL version: 2.1.3
% 81.36/11.91 % (3843892)Termination reason: Instruction limit
% 81.36/11.91 % (3843892)Termination phase: Finite model building constraint generation
% 81.36/11.91 % (3843892)Time elapsed: 0.331 s
% 81.36/11.91 % (3843892)Peak memory usage: 79 MB
% 81.36/11.91 % (3843892)Instructions burned: 921 (million)
% 81.36/11.91 % (3843897)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1387873642:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 81.36/11.91 % TRYING [7]
% 81.36/11.91 % (3843897)Instruction limit reached!
% 81.36/11.91 % (3843897)------------------------------
% 81.36/11.91 % (3843897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.36/11.91 % (3843897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.36/11.91 % (3843897)CaDiCaL version: 2.1.3
% 81.36/11.91 % (3843897)Termination reason: Instruction limit
% 81.36/11.91 % (3843897)Termination phase: Saturation
% 81.36/11.91 % (3843897)Time elapsed: 0.641 s
% 81.36/11.91 % (3843897)Peak memory usage: 15 MB
% 81.36/11.91 % (3843897)Instructions burned: 1474 (million)
% 81.36/11.91 % (3843899)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3090846554:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 211.17/30.27 % TRYING [77]
% 211.17/30.27 % TRYING [8]
% 211.17/30.27 % TRYING [8]
% 211.17/30.27 % (3843895)Instruction limit reached!
% 211.17/30.27 % (3843895)------------------------------
% 211.17/30.27 % (3843895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843895)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843895)Termination reason: Instruction limit
% 211.17/30.27 % (3843895)Termination phase: Saturation
% 211.17/30.27 % (3843895)Time elapsed: 2.637 s
% 211.17/30.27 % (3843895)Peak memory usage: 57 MB
% 211.17/30.27 % (3843895)Instructions burned: 5132 (million)
% 211.17/30.27 % (3843901)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3680802578:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 211.17/30.27 % TRYING [16]
% 211.17/30.27 % TRYING [9]
% 211.17/30.27 % (3843899)Instruction limit reached!
% 211.17/30.27 % (3843899)------------------------------
% 211.17/30.27 % (3843899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843899)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843899)Termination reason: Instruction limit
% 211.17/30.27 % (3843899)Termination phase: Finite model building constraint generation
% 211.17/30.27 % (3843899)Time elapsed: 2.220 s
% 211.17/30.27 % (3843899)Peak memory usage: 411 MB
% 211.17/30.27 % (3843899)Instructions burned: 6326 (million)
% 211.17/30.27 % (3843891)Instruction limit reached!
% 211.17/30.27 % (3843891)------------------------------
% 211.17/30.27 % (3843891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843891)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843891)Termination reason: Instruction limit
% 211.17/30.27 % (3843891)Termination phase: Finite model building constraint generation
% 211.17/30.27 % (3843891)Time elapsed: 3.271 s
% 211.17/30.27 % (3843891)Peak memory usage: 589 MB
% 211.17/30.27 % (3843891)Instructions burned: 9518 (million)
% 211.17/30.27 % (3843903)ott-2_1_sil=16000:newcnf=on:random_seed=600760127:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 211.17/30.27 % (3843905)ott+10_1_sil=32000:tgt=ground:random_seed=3353365261:i=5114:av=off_2957 on theBenchmark for (2957ds/5114Mi)
% 211.17/30.27 % (3843901)Instruction limit reached!
% 211.17/30.27 % (3843901)------------------------------
% 211.17/30.27 % (3843901)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843901)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843901)Termination reason: Instruction limit
% 211.17/30.27 % (3843901)Termination phase: Finite model building constraint generation
% 211.17/30.27 % (3843901)Time elapsed: 0.749 s
% 211.17/30.27 % (3843901)Peak memory usage: 138 MB
% 211.17/30.27 % (3843901)Instructions burned: 2177 (million)
% 211.17/30.27 % (3843907)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=320358187:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 211.17/30.27 % TRYING [1]
% 211.17/30.27 % TRYING [2]
% 211.17/30.27 % TRYING [3]
% 211.17/30.27 % TRYING [4]
% 211.17/30.27 % TRYING [9]
% 211.17/30.27 % TRYING [5]
% 211.17/30.27 % (3843903)Instruction limit reached!
% 211.17/30.27 % (3843903)------------------------------
% 211.17/30.27 % (3843903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843903)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843903)Termination reason: Instruction limit
% 211.17/30.27 % (3843903)Termination phase: Saturation
% 211.17/30.27 % (3843903)Time elapsed: 0.456 s
% 211.17/30.27 % (3843903)Peak memory usage: 26 MB
% 211.17/30.27 % (3843903)Instructions burned: 870 (million)
% 211.17/30.27 % TRYING [6]
% 211.17/30.27 % (3843909)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1866735948:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 211.17/30.27 % TRYING [7]
% 211.17/30.27 % (3843889)Instruction limit reached!
% 211.17/30.27 % (3843889)------------------------------
% 211.17/30.27 % (3843889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 211.17/30.27 % (3843889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.17/30.27 % (3843889)CaDiCaL version: 2.1.3
% 211.17/30.27 % (3843889)Termination reason: Instruction limit
% 211.17/30.27 % (3843889)Termination phase: Finite model building constraint generation
% 211.17/30.27 % (3843889)Time elapsed: 4.785 s
% 211.17/30.27 % (3843889)Peak memory usage: 244 MB
% 211.17/30.27 % (3843889)Instructions burned: 22063 (million)
% 250.12/41.60 % (3843911)dis+21_1_sil=32000:sas=cadical:random_seed=2011724231:i=3773:amm=off_2945 on theBenchmark for (2945ds/3773Mi)
% 250.12/41.60 % TRYING [8]
% 250.12/41.60 % (3843911)Instruction limit reached!
% 250.12/41.60 % (3843911)------------------------------
% 250.12/41.60 % (3843911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843911)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843911)Termination reason: Instruction limit
% 250.12/41.60 % (3843911)Termination phase: Saturation
% 250.12/41.60 % (3843911)Time elapsed: 1.076 s
% 250.12/41.60 % (3843911)Peak memory usage: 47 MB
% 250.12/41.60 % (3843911)Instructions burned: 3773 (million)
% 250.12/41.60 % (3843913)ott+11_1_sil=16000:gs=on:random_seed=454042092:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2934 on theBenchmark for (2934ds/2251Mi)
% 250.12/41.60 % (3843909)Instruction limit reached!
% 250.12/41.60 % (3843909)------------------------------
% 250.12/41.60 % (3843909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843909)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843909)Termination reason: Instruction limit
% 250.12/41.60 % (3843909)Termination phase: Saturation
% 250.12/41.60 % (3843909)Time elapsed: 1.826 s
% 250.12/41.60 % (3843909)Peak memory usage: 42 MB
% 250.12/41.60 % (3843909)Instructions burned: 3512 (million)
% 250.12/41.60 % (3843915)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2245201633:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi)
% 250.12/41.60 % TRYING [7]
% 250.12/41.60 % (3843905)Instruction limit reached!
% 250.12/41.60 % (3843905)------------------------------
% 250.12/41.60 % (3843905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843905)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843905)Termination reason: Instruction limit
% 250.12/41.60 % (3843905)Termination phase: Saturation
% 250.12/41.60 % (3843905)Time elapsed: 2.745 s
% 250.12/41.60 % (3843905)Peak memory usage: 54 MB
% 250.12/41.60 % (3843905)Instructions burned: 5115 (million)
% 250.12/41.60 % (3843917)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4067847203:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2929 on theBenchmark for (2929ds/4591Mi)
% 250.12/41.60 % (3843913)Instruction limit reached!
% 250.12/41.60 % (3843913)------------------------------
% 250.12/41.60 % (3843913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843913)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843913)Termination reason: Instruction limit
% 250.12/41.60 % (3843913)Termination phase: Saturation
% 250.12/41.60 % (3843913)Time elapsed: 0.572 s
% 250.12/41.60 % (3843913)Peak memory usage: 22 MB
% 250.12/41.60 % (3843913)Instructions burned: 2255 (million)
% 250.12/41.60 % (3843919)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2484818207:i=29340_2928 on theBenchmark for (2928ds/29340Mi)
% 250.12/41.60 % TRYING [10]
% 250.12/41.60 % TRYING [8]
% 250.12/41.60 % TRYING [9]
% 250.12/41.60 % (3843917)Instruction limit reached!
% 250.12/41.60 % (3843917)------------------------------
% 250.12/41.60 % (3843917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843917)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843917)Termination reason: Instruction limit
% 250.12/41.60 % (3843917)Termination phase: Saturation
% 250.12/41.60 % (3843917)Time elapsed: 2.034 s
% 250.12/41.60 % (3843917)Peak memory usage: 56 MB
% 250.12/41.60 % (3843917)Instructions burned: 4592 (million)
% 250.12/41.60 % (3843921)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4053081566:i=5211_2908 on theBenchmark for (2908ds/5211Mi)
% 250.12/41.60 % (3843921)Instruction limit reached!
% 250.12/41.60 % (3843921)------------------------------
% 250.12/41.60 % (3843921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843921)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843921)Termination reason: Instruction limit
% 250.12/41.60 % (3843921)Termination phase: Saturation
% 250.12/41.60 % (3843921)Time elapsed: 2.344 s
% 250.12/41.60 % (3843921)Peak memory usage: 47 MB
% 250.12/41.60 % (3843921)Instructions burned: 5212 (million)
% 250.12/41.60 % (3843923)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=201485195:i=5497:nm=2_2885 on theBenchmark for (2885ds/5497Mi)
% 250.12/41.60 % TRYING [17]
% 250.12/41.60 % TRYING [9]
% 250.12/41.60 % TRYING [10]
% 250.12/41.60 % (3843923)Instruction limit reached!
% 250.12/41.60 % (3843923)------------------------------
% 250.12/41.60 % (3843923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843923)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843923)Termination reason: Instruction limit
% 250.12/41.60 % (3843923)Termination phase: Finite model building constraint generation
% 250.12/41.60 % (3843923)Time elapsed: 1.864 s
% 250.12/41.60 % (3843923)Peak memory usage: 344 MB
% 250.12/41.60 % (3843923)Instructions burned: 5500 (million)
% 250.12/41.60 % (3843925)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4214164696:fmbsr=2:i=46332_2865 on theBenchmark for (2865ds/46332Mi)
% 250.12/41.60 % TRYING [15]
% 250.12/41.60 % (3843919)Instruction limit reached!
% 250.12/41.60 % (3843919)------------------------------
% 250.12/41.60 % (3843919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843919)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843919)Termination reason: Instruction limit
% 250.12/41.60 % (3843919)Termination phase: Saturation
% 250.12/41.60 % (3843919)Time elapsed: 7.662 s
% 250.12/41.60 % (3843919)Peak memory usage: 414 MB
% 250.12/41.60 % (3843919)Instructions burned: 29343 (million)
% 250.12/41.60 % (3843927)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=331868945:i=14071_2851 on theBenchmark for (2851ds/14071Mi)
% 250.12/41.60 % TRYING [12]
% 250.12/41.60 % (3843927)Instruction limit reached!
% 250.12/41.60 % (3843927)------------------------------
% 250.12/41.60 % (3843927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843927)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843927)Termination reason: Instruction limit
% 250.12/41.60 % (3843927)Termination phase: Finite model building constraint generation
% 250.12/41.60 % (3843927)Time elapsed: 3.054 s
% 250.12/41.60 % (3843927)Peak memory usage: 819 MB
% 250.12/41.60 % (3843927)Instructions burned: 14073 (million)
% 250.12/41.60 % (3843930)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3252341539:i=22565:add=on:rawr=on_2820 on theBenchmark for (2820ds/22565Mi)
% 250.12/41.60 % TRYING [10]
% 250.12/41.60 % TRYING [11]
% 250.12/41.60 % (3843930)Instruction limit reached!
% 250.12/41.60 % (3843930)------------------------------
% 250.12/41.60 % (3843930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843930)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843930)Termination reason: Instruction limit
% 250.12/41.60 % (3843930)Termination phase: Saturation
% 250.12/41.60 % (3843930)Time elapsed: 7.269 s
% 250.12/41.60 % (3843930)Peak memory usage: 158 MB
% 250.12/41.60 % (3843930)Instructions burned: 22567 (million)
% 250.12/41.60 % (3843932)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1600467020:i=8173:av=off_2747 on theBenchmark for (2747ds/8173Mi)
% 250.12/41.60 % (3843932)Instruction limit reached!
% 250.12/41.60 % (3843932)------------------------------
% 250.12/41.60 % (3843932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843932)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843932)Termination reason: Instruction limit
% 250.12/41.60 % (3843932)Termination phase: Saturation
% 250.12/41.60 % (3843932)Time elapsed: 2.095 s
% 250.12/41.60 % (3843932)Peak memory usage: 76 MB
% 250.12/41.60 % (3843932)Instructions burned: 8173 (million)
% 250.12/41.60 % (3843934)dis+10_16:1_sil=16000:random_seed=3610726923:i=9155:fsr=off_2726 on theBenchmark for (2726ds/9155Mi)
% 250.12/41.60 % (3843934)Instruction limit reached!
% 250.12/41.60 % (3843934)------------------------------
% 250.12/41.60 % (3843934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843934)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843934)Termination reason: Instruction limit
% 250.12/41.60 % (3843934)Termination phase: Saturation
% 250.12/41.60 % (3843934)Time elapsed: 2.482 s
% 250.12/41.60 % (3843934)Peak memory usage: 85 MB
% 250.12/41.60 % (3843934)Instructions burned: 9157 (million)
% 250.12/41.60 % (3843936)ott-3_8_sil=64000:random_seed=3670374035:i=20139:bs=on_2701 on theBenchmark for (2701ds/20139Mi)
% 250.12/41.60 % (3843925)Instruction limit reached!
% 250.12/41.60 % (3843925)------------------------------
% 250.12/41.60 % (3843925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843925)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843925)Termination reason: Instruction limit
% 250.12/41.60 % (3843925)Termination phase: Finite model building constraint generation
% 250.12/41.60 % (3843925)Time elapsed: 17.960 s
% 250.12/41.60 % (3843925)Peak memory usage: 2485 MB
% 250.12/41.60 % (3843925)Instructions burned: 46335 (million)
% 250.12/41.60 % (3843938)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3138679626:fmbsr=2:i=32576_2682 on theBenchmark for (2682ds/32576Mi)
% 250.12/41.60 % TRYING [9]
% 250.12/41.60 % (3843907)Instruction limit reached!
% 250.12/41.60 % (3843907)------------------------------
% 250.12/41.60 % (3843907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843907)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843907)Termination reason: Instruction limit
% 250.12/41.60 % (3843907)Termination phase: Finite model building SAT solving
% 250.12/41.60 % (3843907)Time elapsed: 28.092 s
% 250.12/41.60 % (3843907)Peak memory usage: 1099 MB
% 250.12/41.60 % (3843907)Instructions burned: 54284 (million)
% 250.12/41.60 % TRYING [11]
% 250.12/41.60 % (3843940)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1243071534:i=11404_2672 on theBenchmark for (2672ds/11404Mi)
% 250.12/41.60 % (3843915)Instruction limit reached!
% 250.12/41.60 % (3843915)------------------------------
% 250.12/41.60 % (3843915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843915)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843915)Termination reason: Instruction limit
% 250.12/41.60 % (3843915)Termination phase: Finite model building constraint generation
% 250.12/41.60 % (3843915)Time elapsed: 27.992 s
% 250.12/41.60 % (3843915)Peak memory usage: 403 MB
% 250.12/41.60 % (3843915)Instructions burned: 67535 (million)
% 250.12/41.60 % (3843942)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2226096028:i=14134_2653 on theBenchmark for (2653ds/14134Mi)
% 250.12/41.60 % (3843936)Instruction limit reached!
% 250.12/41.60 % (3843936)------------------------------
% 250.12/41.60 % (3843936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843936)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843936)Termination reason: Instruction limit
% 250.12/41.60 % (3843936)Termination phase: Saturation
% 250.12/41.60 % (3843936)Time elapsed: 6.553 s
% 250.12/41.60 % (3843936)Peak memory usage: 157 MB
% 250.12/41.60 % (3843936)Instructions burned: 20141 (million)
% 250.12/41.60 % (3843944)dis+33_16_sil=32000:sac=on:random_seed=546626532:i=15851:nm=0_2635 on theBenchmark for (2635ds/15851Mi)
% 250.12/41.60 % TRYING [10]
% 250.12/41.60 % (3843940)Instruction limit reached!
% 250.12/41.60 % (3843940)------------------------------
% 250.12/41.60 % (3843940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843940)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843940)Termination reason: Instruction limit
% 250.12/41.60 % (3843940)Termination phase: Saturation
% 250.12/41.60 % (3843940)Time elapsed: 4.830 s
% 250.12/41.60 % (3843940)Peak memory usage: 83 MB
% 250.12/41.60 % (3843940)Instructions burned: 11405 (million)
% 250.12/41.60 % (3843946)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2437053328:avsq=on:i=17627:add=on:amm=off_2624 on theBenchmark for (2624ds/17627Mi)
% 250.12/41.60 % (3843942) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3843850-3843942"...
% 250.12/41.60 % (3843942)...printing done.
% 250.12/41.60 % (3843942)Refutation found. Thanks to Tanya!
% 250.12/41.60 % SZS status Unsatisfiable for theBenchmark
% 250.12/41.60 % SZS output start Proof for theBenchmark
% See solution above
% 250.12/41.60 % (3843942)------------------------------
% 250.12/41.60 % (3843942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 250.12/41.60 % (3843942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 250.12/41.60 % (3843942)CaDiCaL version: 2.1.3
% 250.12/41.60 % (3843942)Termination reason: Refutation
% 250.12/41.60 % (3843942)Time elapsed: 6.370 s
% 250.12/41.60 % (3843942)Peak memory usage: 147 MB
% 250.12/41.60 % (3843942)Instructions burned: 11686 (million)
% 250.12/41.60 % (3843850)Success in time 41.181 s
% 250.12/41.60 % Vampire exiting
%------------------------------------------------------------------------------