%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU290+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 12:52:44 PM UTC 2026
% Result : Theorem 43.26s 7.60s
% Output : Refutation 43.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 57 ( 18 unt; 2 def)
% Number of atoms : 220 ( 74 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 255 ( 92 ~; 90 |; 48 &)
% ( 13 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-3 aty)
% Number of variables : 112 ( 95 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
=> relation(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f27,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> ( ( ( X1 = empty_set
=> X0 = empty_set )
=> ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) ) )
& ( X1 = empty_set
=> ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_funct_2) ).
fof(f61,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_funct_1) ).
fof(f120,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> element(X2,powerset(cartesian_product2(X0,X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(f196,axiom,
! [X0,X1,X2] :
( relation_of2(X2,X0,X1)
=> relation_dom_as_subset(X0,X1,X2) = relation_dom(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(f201,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
<=> relation_of2(X2,X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f357,conjecture,
! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( in(X2,X0)
=> ( X1 = empty_set
| in(apply(X3,X2),relation_rng(X3)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_funct_2) ).
fof(f358,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( in(X2,X0)
=> ( X1 = empty_set
| in(apply(X3,X2),relation_rng(X3)) ) ) ),
inference(negated_conjecture,[status(cth)],[f357]) ).
fof(f416,plain,
! [X0,X1,X2] :
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(ennf_transformation,[],[f6]) ).
fof(f439,plain,
! [X0,X1,X2] :
( ( ( ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f440,plain,
! [X0,X1,X2] :
( ( ( ( quasi_total(X2,X0,X1)
<=> X0 = relation_dom_as_subset(X0,X1,X2) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( quasi_total(X2,X0,X1)
<=> X2 = empty_set )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(flattening,[],[f439]) ).
fof(f463,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f464,plain,
! [X0] :
( ! [X1] :
( X1 = relation_rng(X0)
<=> ! [X2] :
( in(X2,X1)
<=> ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f463]) ).
fof(f501,plain,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f558,plain,
! [X0,X1,X2] :
( relation_dom_as_subset(X0,X1,X2) = relation_dom(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f196]) ).
fof(f759,plain,
? [X0,X1,X2,X3] :
( empty_set != X1
& ~ in(apply(X3,X2),relation_rng(X3))
& in(X2,X0)
& function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) ),
inference(ennf_transformation,[],[f358]) ).
fof(f760,plain,
? [X0,X1,X2,X3] :
( empty_set != X1
& ~ in(apply(X3,X2),relation_rng(X3))
& in(X2,X0)
& function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) ),
inference(flattening,[],[f759]) ).
fof(f860,plain,
! [X0,X1,X2] :
( ( ( ( ( quasi_total(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) != X0 )
& ( X0 = relation_dom_as_subset(X0,X1,X2)
| ~ quasi_total(X2,X0,X1) ) )
| ( empty_set != X0
& X1 = empty_set ) )
& ( X0 = empty_set
| ( ( quasi_total(X2,X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| ~ quasi_total(X2,X0,X1) ) )
| empty_set != X1 ) )
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(nnf_transformation,[],[f440]) ).
fof(f952,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 )
| ~ in(X2,X1) )
& ( ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) )
| in(X2,X1) ) ) )
& ( ! [X2] :
( ( in(X2,X1)
| ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 ) )
& ( ? [X3] :
( in(X3,relation_dom(X0))
& X2 = apply(X0,X3) )
| ~ in(X2,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f464]) ).
fof(f953,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ? [X2] :
( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != X2 )
| ~ in(X2,X1) )
& ( ? [X4] :
( in(X4,relation_dom(X0))
& apply(X0,X4) = X2 )
| in(X2,X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5 ) )
& ( ? [X7] :
( in(X7,relation_dom(X0))
& apply(X0,X7) = X5 )
| ~ in(X5,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f952]) ).
fof(f954,plain,
! [X0] :
( ! [X1] :
( ( X1 = relation_rng(X0)
| ( ( ! [X3] :
( ~ in(X3,relation_dom(X0))
| apply(X0,X3) != sK90(X0,X1) )
| ~ in(sK90(X0,X1),X1) )
& ( ( in(sK91(X0,X1),relation_dom(X0))
& sK90(X0,X1) = apply(X0,sK91(X0,X1)) )
| in(sK90(X0,X1),X1) ) ) )
& ( ! [X5] :
( ( in(X5,X1)
| ! [X6] :
( ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5 ) )
& ( ( in(sK92(X0,X5),relation_dom(X0))
& apply(X0,sK92(X0,X5)) = X5 )
| ~ in(X5,X1) ) )
| relation_rng(X0) != X1 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK90,sK91,sK92]),skolemize(X2,sK90(X0,X1)),skolemize(X4,sK91(X0,X1)),skolemize(X7,sK92(X0,X5))],[f953]) ).
fof(f1030,plain,
! [X0,X1,X2] :
( ( relation_of2_as_subset(X2,X0,X1)
| ~ relation_of2(X2,X0,X1) )
& ( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f201]) ).
fof(f1202,plain,
( empty_set != sK273
& ~ in(apply(sK275,sK274),relation_rng(sK275))
& in(sK274,sK272)
& function(sK275)
& quasi_total(sK275,sK272,sK273)
& relation_of2_as_subset(sK275,sK272,sK273) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK272,sK273,sK274,sK275]),skolemize(X0,sK272),skolemize(X1,sK273),skolemize(X2,sK274),skolemize(X3,sK275)],[f760]) ).
fof(f1219,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(cartesian_product2(X0,X1)))
| relation(X2) ),
inference(cnf_transformation,[],[f416]) ).
fof(f1298,plain,
! [X2,X0,X1] :
( ~ quasi_total(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) = X0
| empty_set = X1
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f860]) ).
fof(f1451,plain,
! [X0,X1,X6,X5] :
( in(X5,X1)
| ~ in(X6,relation_dom(X0))
| apply(X0,X6) != X5
| relation_rng(X0) != X1
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f954]) ).
fof(f1541,plain,
! [X2,X0,X1] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f501]) ).
fof(f1697,plain,
! [X2,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| relation_dom_as_subset(X0,X1,X2) = relation_dom(X2) ),
inference(cnf_transformation,[],[f558]) ).
fof(f1702,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f1030]) ).
fof(f2132,plain,
relation_of2_as_subset(sK275,sK272,sK273),
inference(cnf_transformation,[],[f1202]) ).
fof(f2133,plain,
quasi_total(sK275,sK272,sK273),
inference(cnf_transformation,[],[f1202]) ).
fof(f2134,plain,
function(sK275),
inference(cnf_transformation,[],[f1202]) ).
fof(f2135,plain,
in(sK274,sK272),
inference(cnf_transformation,[],[f1202]) ).
fof(f2136,plain,
~ in(apply(sK275,sK274),relation_rng(sK275)),
inference(cnf_transformation,[],[f1202]) ).
fof(f2137,plain,
empty_set != sK273,
inference(cnf_transformation,[],[f1202]) ).
fof(f2559,plain,
! [X0,X1,X6] :
( in(apply(X0,X6),X1)
| ~ in(X6,relation_dom(X0))
| relation_rng(X0) != X1
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f1451]) ).
fof(f2560,plain,
! [X0,X6] :
( in(apply(X0,X6),relation_rng(X0))
| ~ in(X6,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f2559]) ).
fof(f2627,definition,
sF279 = apply(sK275,sK274),
introduced(definition,[new_symbols(definition,[sF279])],[function_definition]) ).
fof(f2628,plain,
apply(sK275,sK274) = sF279,
inference(reorient_equations,[],[f2627]) ).
fof(f2629,definition,
sF280 = relation_rng(sK275),
introduced(definition,[new_symbols(definition,[sF280])],[function_definition]) ).
fof(f2630,plain,
relation_rng(sK275) = sF280,
inference(reorient_equations,[],[f2629]) ).
fof(f2631,plain,
~ in(sF279,sF280),
inference(definition_folding,[],[f2136,f2630,f2628]) ).
fof(f4125,plain,
relation_of2(sK275,sK272,sK273),
inference(resolution,[],[f1702,f2132]) ).
fof(f6416,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X0,X1,X2)
| relation(X0) ),
inference(resolution,[],[f1541,f1219]) ).
fof(f8138,plain,
relation_dom(sK275) = relation_dom_as_subset(sK272,sK273,sK275),
inference(resolution,[],[f1697,f4125]) ).
fof(f13042,plain,
( in(sF279,relation_rng(sK275))
| ~ in(sK274,relation_dom(sK275))
| ~ relation(sK275)
| ~ function(sK275) ),
inference(superposition,[],[f2560,f2628]) ).
fof(f13053,plain,
( in(sF279,relation_rng(sK275))
| ~ in(sK274,relation_dom(sK275))
| ~ relation(sK275) ),
inference(forward_subsumption_resolution,[],[f13042,f2134]) ).
fof(f13061,plain,
( in(sF279,sF280)
| ~ in(sK274,relation_dom(sK275))
| ~ relation(sK275) ),
inference(forward_demodulation,[],[f13053,f2630]) ).
fof(f13065,plain,
( ~ in(sK274,relation_dom(sK275))
| ~ relation(sK275) ),
inference(forward_subsumption_resolution,[],[f13061,f2631]) ).
fof(f17787,plain,
( sK272 = relation_dom_as_subset(sK272,sK273,sK275)
| empty_set = sK273
| ~ relation_of2_as_subset(sK275,sK272,sK273) ),
inference(resolution,[],[f1298,f2133]) ).
fof(f17790,plain,
( sK272 = relation_dom_as_subset(sK272,sK273,sK275)
| ~ relation_of2_as_subset(sK275,sK272,sK273) ),
inference(forward_subsumption_resolution,[],[f17787,f2137]) ).
fof(f17792,plain,
sK272 = relation_dom_as_subset(sK272,sK273,sK275),
inference(forward_subsumption_resolution,[],[f17790,f2132]) ).
fof(f18414,plain,
sK272 = relation_dom(sK275),
inference(superposition,[],[f8138,f17792]) ).
fof(f18449,plain,
( ~ in(sK274,sK272)
| ~ relation(sK275) ),
inference(superposition,[],[f13065,f18414]) ).
fof(f18484,plain,
~ relation(sK275),
inference(forward_subsumption_resolution,[],[f18449,f2135]) ).
fof(f59527,plain,
relation(sK275),
inference(resolution,[],[f6416,f2132]) ).
fof(f59533,plain,
$false,
inference(forward_subsumption_resolution,[],[f59527,f18484]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU290+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.37 % Computer : n016.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8046.5625MB
% 0.13/0.37 % OS : Linux 6.8.0-71-generic
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Mon Sep 28 04:36:47 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.41 Running first-order model finding
% 0.13/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.07/2.78 % (3260881)Will run a generic schedule for satisfiability detection.
% 16.07/2.78 % (3260890)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3609814139:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.07/2.78 % (3260887)% WARNING: option uhcvi not known.
% 16.07/2.78 % (3260886)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3547288718_2999 on theBenchmark for (2999ds/0Mi)
% 16.07/2.78 % (3260887)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2946058814:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.07/2.78 % (3260888)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=416027915:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.07/2.78 % (3260889)dis+10_1_sil=32000:sp=arity:random_seed=3252214806:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.07/2.78 % (3260892)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1274839769:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.07/2.78 % (3260891)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2554806846:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.07/2.78 % (3260890)Instruction limit reached!
% 16.07/2.78 % (3260890)------------------------------
% 16.07/2.78 % (3260890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.78 % (3260890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.78 % (3260890)CaDiCaL version: 2.1.3
% 16.07/2.78 % (3260890)Termination reason: Instruction limit
% 16.07/2.78 % (3260890)Termination phase: Saturation
% 16.07/2.78 % (3260890)Time elapsed: 0.032 s
% 16.07/2.78 % (3260890)Peak memory usage: 13 MB
% 16.07/2.78 % (3260890)Instructions burned: 116 (million)
% 16.07/2.78 % (3260900)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1589091385:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.07/2.78 % (3260889)Instruction limit reached!
% 16.07/2.78 % (3260889)------------------------------
% 16.07/2.78 % (3260889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.78 % (3260889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.78 % (3260889)CaDiCaL version: 2.1.3
% 16.07/2.78 % (3260889)Termination reason: Instruction limit
% 16.07/2.78 % (3260889)Termination phase: Saturation
% 16.07/2.78 % (3260889)Time elapsed: 0.065 s
% 16.07/2.78 % (3260889)Peak memory usage: 14 MB
% 16.07/2.78 % (3260889)Instructions burned: 104 (million)
% 16.07/2.78 % (3260891)Instruction limit reached!
% 16.07/2.78 % (3260891)------------------------------
% 16.07/2.78 % (3260891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.78 % (3260891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.78 % (3260891)CaDiCaL version: 2.1.3
% 16.07/2.78 % (3260891)Termination reason: Instruction limit
% 16.07/2.78 % (3260891)Termination phase: Saturation
% 16.07/2.78 % (3260891)Time elapsed: 0.075 s
% 16.07/2.78 % (3260891)Peak memory usage: 14 MB
% 16.07/2.78 % (3260891)Instructions burned: 132 (million)
% 16.07/2.78 % (3260902)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1712554226:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.07/2.78 % TRYING [1]
% 16.07/2.78 % TRYING [2]
% 16.07/2.78 % (3260892)Instruction limit reached!
% 16.07/2.78 % (3260892)------------------------------
% 16.07/2.78 % (3260892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.78 % (3260903)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=947034822:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.07/2.78 % (3260892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.07/2.78 % (3260892)CaDiCaL version: 2.1.3
% 16.07/2.78 % (3260892)Termination reason: Instruction limit
% 16.07/2.78 % (3260892)Termination phase: Saturation
% 16.07/2.78 % (3260892)Time elapsed: 0.096 s
% 16.07/2.78 % (3260892)Peak memory usage: 15 MB
% 16.07/2.78 % (3260892)Instructions burned: 159 (million)
% 16.07/2.78 % (3260906)ott-21_1_sil=16000:fs=off:random_seed=4113596605:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.07/2.78 % TRYING [1]
% 16.07/2.78 % TRYING [3]
% 16.07/2.78 % TRYING [2]
% 16.07/2.78 % (3260902)Instruction limit reached!
% 16.07/2.78 % (3260902)------------------------------
% 16.07/2.78 % (3260902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.07/2.78 % (3260902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.07 % (3260902)CaDiCaL version: 2.1.3
% 41.01/7.07 % (3260902)Termination reason: Instruction limit
% 41.01/7.07 % (3260902)Termination phase: Saturation
% 41.01/7.07 % (3260902)Time elapsed: 0.075 s
% 41.01/7.07 % (3260902)Peak memory usage: 14 MB
% 41.01/7.07 % (3260902)Instructions burned: 132 (million)
% 41.01/7.07 % (3260908)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3750909709:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 41.01/7.07 % TRYING [3]
% 41.01/7.07 % (3260900)Instruction limit reached!
% 41.01/7.07 % (3260900)------------------------------
% 41.01/7.07 % (3260900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/7.07 % (3260900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.07 % (3260900)CaDiCaL version: 2.1.3
% 41.01/7.07 % (3260900)Termination reason: Instruction limit
% 41.01/7.07 % (3260900)Termination phase: Finite model building constraint generation
% 41.01/7.07 % (3260900)Time elapsed: 0.166 s
% 41.01/7.07 % (3260900)Peak memory usage: 45 MB
% 41.01/7.07 % (3260900)Instructions burned: 719 (million)
% 41.01/7.07 % (3260906)Instruction limit reached!
% 41.01/7.08 % (3260906)------------------------------
% 41.01/7.08 % (3260906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/7.08 % (3260906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.08 % (3260906)CaDiCaL version: 2.1.3
% 41.01/7.08 % (3260906)Termination reason: Instruction limit
% 41.01/7.08 % (3260906)Termination phase: Saturation
% 41.01/7.08 % (3260906)Time elapsed: 0.098 s
% 41.01/7.08 % (3260906)Peak memory usage: 15 MB
% 41.01/7.08 % (3260906)Instructions burned: 181 (million)
% 41.01/7.08 % (3260910)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2056862072:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.01/7.08 % (3260911)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2173478484:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 41.01/7.08 % TRYING [1]
% 41.01/7.08 % TRYING [2]
% 41.01/7.08 % TRYING [3]
% 41.01/7.08 % (3260910)Instruction limit reached!
% 41.01/7.08 % (3260910)------------------------------
% 41.01/7.08 % (3260910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/7.08 % (3260910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.08 % (3260910)CaDiCaL version: 2.1.3
% 41.01/7.08 % (3260910)Termination reason: Instruction limit
% 41.01/7.08 % (3260910)Termination phase: Finite model building constraint generation
% 41.01/7.08 % (3260910)Time elapsed: 0.201 s
% 41.01/7.08 % (3260910)Peak memory usage: 39 MB
% 41.01/7.08 % (3260910)Instructions burned: 868 (million)
% 41.01/7.08 % (3260914)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=119977767:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.01/7.08 % (3260903)Instruction limit reached!
% 41.01/7.08 % (3260903)------------------------------
% 41.01/7.08 % (3260903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/7.08 % (3260903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.08 % (3260903)CaDiCaL version: 2.1.3
% 41.01/7.08 % (3260903)Termination reason: Instruction limit
% 41.01/7.08 % (3260903)Termination phase: Saturation
% 41.01/7.08 % (3260903)Time elapsed: 0.407 s
% 41.01/7.08 % (3260903)Peak memory usage: 20 MB
% 41.01/7.08 % (3260903)Instructions burned: 685 (million)
% 41.01/7.08 % (3260908)Instruction limit reached!
% 41.01/7.08 % (3260908)------------------------------
% 41.01/7.08 % (3260908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.01/7.08 % (3260908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.01/7.08 % (3260908)CaDiCaL version: 2.1.3
% 41.01/7.08 % (3260908)Termination reason: Instruction limit
% 41.01/7.08 % (3260908)Termination phase: Saturation
% 41.01/7.08 % (3260908)Time elapsed: 0.329 s
% 41.01/7.08 % (3260908)Peak memory usage: 16 MB
% 41.01/7.08 % (3260908)Instructions burned: 478 (million)
% 41.01/7.08 % (3260916)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=3887810299: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)
% 41.01/7.08 % (3260917)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3425873203:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 41.01/7.08 % TRYING [4]
% 41.01/7.08 % (3260914)Instruction limit reached!
% 41.01/7.08 % (3260914)------------------------------
% 41.01/7.08 % (3260914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260914)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260914)Termination reason: Instruction limit
% 43.26/7.60 % (3260914)Termination phase: Finite model building constraint generation
% 43.26/7.60 % (3260914)Time elapsed: 0.247 s
% 43.26/7.60 % (3260914)Peak memory usage: 97 MB
% 43.26/7.60 % (3260914)Instructions burned: 892 (million)
% 43.26/7.60 % (3260920)fmb+10_1_sil=64000:random_seed=584675876:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 43.26/7.60 % TRYING [1]
% 43.26/7.60 % TRYING [2]
% 43.26/7.60 % TRYING [3]
% 43.26/7.60 % (3260916)Instruction limit reached!
% 43.26/7.60 % (3260916)------------------------------
% 43.26/7.60 % (3260916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260916)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260916)Termination reason: Instruction limit
% 43.26/7.60 % (3260916)Termination phase: Saturation
% 43.26/7.60 % (3260916)Time elapsed: 0.373 s
% 43.26/7.60 % (3260916)Peak memory usage: 27 MB
% 43.26/7.60 % (3260916)Instructions burned: 692 (million)
% 43.26/7.60 % (3260922)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=572971309:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 43.26/7.60 % (3260911)Instruction limit reached!
% 43.26/7.60 % (3260911)------------------------------
% 43.26/7.60 % (3260911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260911)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260911)Termination reason: Instruction limit
% 43.26/7.60 % (3260911)Termination phase: Saturation
% 43.26/7.60 % (3260911)Time elapsed: 0.742 s
% 43.26/7.60 % (3260911)Peak memory usage: 29 MB
% 43.26/7.60 % (3260911)Instructions burned: 1180 (million)
% 43.26/7.60 % (3260917)Instruction limit reached!
% 43.26/7.60 % (3260917)------------------------------
% 43.26/7.60 % (3260917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260917)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260917)Termination reason: Instruction limit
% 43.26/7.60 % (3260917)Termination phase: Saturation
% 43.26/7.60 % (3260917)Time elapsed: 0.460 s
% 43.26/7.60 % (3260917)Peak memory usage: 22 MB
% 43.26/7.60 % (3260917)Instructions burned: 880 (million)
% 43.26/7.60 % (3260924)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=462673504:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 43.26/7.60 % (3260925)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1513232642:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 43.26/7.60 % TRYING [20]
% 43.26/7.60 % TRYING [8]
% 43.26/7.60 % TRYING [4]
% 43.26/7.60 % (3260924)Instruction limit reached!
% 43.26/7.60 % (3260924)------------------------------
% 43.26/7.60 % (3260924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260924)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260924)Termination reason: Instruction limit
% 43.26/7.60 % (3260924)Termination phase: Finite model building constraint generation
% 43.26/7.60 % (3260924)Time elapsed: 0.343 s
% 43.26/7.60 % (3260924)Peak memory usage: 57 MB
% 43.26/7.60 % (3260924)Instructions burned: 921 (million)
% 43.26/7.60 % (3260928)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3282107868:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 43.26/7.60 % TRYING [5]
% 43.26/7.60 % (3260928)Instruction limit reached!
% 43.26/7.60 % (3260928)------------------------------
% 43.26/7.60 % (3260928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260928)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260928)Termination reason: Instruction limit
% 43.26/7.60 % (3260928)Termination phase: Saturation
% 43.26/7.60 % (3260928)Time elapsed: 0.803 s
% 43.26/7.60 % (3260928)Peak memory usage: 27 MB
% 43.26/7.60 % (3260928)Instructions burned: 1472 (million)
% 43.26/7.60 % (3260930)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1613930619:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 43.26/7.60 % (3260930)Cannot represent all propositional literals internally
% 43.26/7.60 % (3260930)Refutation not found, incomplete strategy
% 43.26/7.60 % (3260930)------------------------------
% 43.26/7.60 % (3260930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260930)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260930)Termination reason: Refutation not found, incomplete strategy
% 43.26/7.60 % (3260930)Time elapsed: 0.118 s
% 43.26/7.60 % (3260930)Peak memory usage: 16 MB
% 43.26/7.60 % (3260930)Instructions burned: 236 (million)
% 43.26/7.60 % (3260930)------------------------------
% 43.26/7.60 % (3260930)------------------------------
% 43.26/7.60 % (3260932)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=270604096:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 43.26/7.60 % TRYING [16]
% 43.26/7.60 % TRYING [5]
% 43.26/7.60 % (3260932)Instruction limit reached!
% 43.26/7.60 % (3260932)------------------------------
% 43.26/7.60 % (3260932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260932)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260932)Termination reason: Instruction limit
% 43.26/7.60 % (3260932)Termination phase: Finite model building constraint generation
% 43.26/7.60 % (3260932)Time elapsed: 0.930 s
% 43.26/7.60 % (3260932)Peak memory usage: 82 MB
% 43.26/7.60 % (3260932)Instructions burned: 2175 (million)
% 43.26/7.60 % (3260934)ott-2_1_sil=16000:newcnf=on:random_seed=447984270:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 43.26/7.60 % (3260934)Instruction limit reached!
% 43.26/7.60 % (3260934)------------------------------
% 43.26/7.60 % (3260934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260934)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260934)Termination reason: Instruction limit
% 43.26/7.60 % (3260934)Termination phase: Saturation
% 43.26/7.60 % (3260934)Time elapsed: 0.507 s
% 43.26/7.60 % (3260934)Peak memory usage: 23 MB
% 43.26/7.60 % (3260934)Instructions burned: 869 (million)
% 43.26/7.60 % (3260936)ott+10_1_sil=32000:tgt=ground:random_seed=3877245508:i=5114:av=off_2961 on theBenchmark for (2961ds/5114Mi)
% 43.26/7.60 % (3260925)Instruction limit reached!
% 43.26/7.60 % (3260925)------------------------------
% 43.26/7.60 % (3260925)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260925)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260925)Termination reason: Instruction limit
% 43.26/7.60 % (3260925)Termination phase: Saturation
% 43.26/7.60 % (3260925)Time elapsed: 3.074 s
% 43.26/7.60 % (3260925)Peak memory usage: 48 MB
% 43.26/7.60 % (3260925)Instructions burned: 5132 (million)
% 43.26/7.60 % (3260938)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2008311559:i=54282_2958 on theBenchmark for (2958ds/54282Mi)
% 43.26/7.60 % TRYING [1]
% 43.26/7.60 % TRYING [2]
% 43.26/7.60 % TRYING [3]
% 43.26/7.60 % (3260922)Instruction limit reached!
% 43.26/7.60 % (3260922)------------------------------
% 43.26/7.60 % (3260922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260922)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260922)Termination reason: Instruction limit
% 43.26/7.60 % (3260922)Termination phase: Finite model building constraint generation
% 43.26/7.60 % (3260922)Time elapsed: 3.419 s
% 43.26/7.60 % (3260922)Peak memory usage: 618 MB
% 43.26/7.60 % (3260922)Instructions burned: 9518 (million)
% 43.26/7.60 % (3260940)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=120232433:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi)
% 43.26/7.60 % TRYING [4]
% 43.26/7.60 % TRYING [5]
% 43.26/7.60 % (3260920)Instruction limit reached!
% 43.26/7.60 % (3260920)------------------------------
% 43.26/7.60 % (3260920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260920)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260920)Termination reason: Instruction limit
% 43.26/7.60 % (3260920)Termination phase: Finite model building SAT solving
% 43.26/7.60 % (3260920)Time elapsed: 5.871 s
% 43.26/7.60 % (3260920)Peak memory usage: 447 MB
% 43.26/7.60 % (3260920)Instructions burned: 22063 (million)
% 43.26/7.60 % (3260943)dis+21_1_sil=32000:sas=cadical:random_seed=3724005518:i=3773:amm=off_2933 on theBenchmark for (2933ds/3773Mi)
% 43.26/7.60 % (3260940)Instruction limit reached!
% 43.26/7.60 % (3260940)------------------------------
% 43.26/7.60 % (3260940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260940)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260940)Termination reason: Instruction limit
% 43.26/7.60 % (3260940)Termination phase: Saturation
% 43.26/7.60 % (3260940)Time elapsed: 2.212 s
% 43.26/7.60 % (3260940)Peak memory usage: 41 MB
% 43.26/7.60 % (3260940)Instructions burned: 3512 (million)
% 43.26/7.60 % (3260945)ott+11_1_sil=16000:gs=on:random_seed=1787110854:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 43.26/7.60 % TRYING [6]
% 43.26/7.60 % (3260936) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3260881-3260936"...
% 43.26/7.60 % (3260936)...printing done.
% 43.26/7.60 % (3260936)Refutation found. Thanks to Tanya!
% 43.26/7.60 % SZS status Theorem for theBenchmark
% 43.26/7.60 % SZS output start Proof for theBenchmark
% See solution above
% 43.26/7.60 % (3260936)------------------------------
% 43.26/7.60 % (3260936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.26/7.60 % (3260936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.26/7.60 % (3260936)CaDiCaL version: 2.1.3
% 43.26/7.60 % (3260936)Termination reason: Refutation
% 43.26/7.60 % (3260936)Time elapsed: 3.214 s
% 43.26/7.60 % (3260936)Peak memory usage: 67 MB
% 43.26/7.60 % (3260936)Instructions burned: 4965 (million)
% 43.26/7.60 % (3260881)Success in time 7.181 s
% 43.26/7.60 % Vampire exiting
%------------------------------------------------------------------------------