%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR027+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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 09:44:24 AM UTC 2026
% Result : Theorem 29.21s 8.64s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 52 ( 12 unt; 3 def)
% Number of atoms : 110 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 107 ( 49 ~; 42 |; 6 &)
% ( 3 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 4 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-4 aty)
% Number of variables : 39 ( 0 sgn 37 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10954,axiom,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_10954) ).
fof(f11449,axiom,
! [X0] :
( ( mtvisible(c_tptp_member2610_mt)
& isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) )
=> tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_11449) ).
fof(f11450,axiom,
( mtvisible(c_tptp_member2610_mt)
=> relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_11450) ).
fof(f26597,axiom,
! [X0,X1,X2,X3] :
( ( isa(X0,X1)
& relationallexists(X2,X1,X3) )
=> isa(f_relationallexistsfn(X0,X2,X1,X3),X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_26597) ).
fof(f27477,axiom,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_27477) ).
fof(f37514,axiom,
! [X0] :
( isa(X0,c_tptpcol_16_31868)
=> tptpcol_16_31868(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_37514) ).
fof(f44208,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_44208) ).
fof(f44217,conjecture,
? [X0] :
( mtvisible(c_tptp_spindlecollectormt)
=> ( tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0)
& tptpcol_16_31868(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query177) ).
fof(f44218,negated_conjecture,
~ ? [X0] :
( mtvisible(c_tptp_spindlecollectormt)
=> ( tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0)
& tptpcol_16_31868(X0) ) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f49513,plain,
! [X0] :
( tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ mtvisible(c_tptp_member2610_mt)
| ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ),
inference(ennf_transformation,[],[f11449]) ).
fof(f49514,plain,
! [X0] :
( tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ mtvisible(c_tptp_member2610_mt)
| ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ),
inference(flattening,[],[f49513]) ).
fof(f49515,plain,
( relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)
| ~ mtvisible(c_tptp_member2610_mt) ),
inference(ennf_transformation,[],[f11450]) ).
fof(f53169,plain,
! [X0,X1,X2,X3] :
( isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| ~ isa(X0,X1)
| ~ relationallexists(X2,X1,X3) ),
inference(ennf_transformation,[],[f26597]) ).
fof(f53170,plain,
! [X0,X1,X2,X3] :
( isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| ~ isa(X0,X1)
| ~ relationallexists(X2,X1,X3) ),
inference(flattening,[],[f53169]) ).
fof(f60728,plain,
! [X0] :
( tptpcol_16_31868(X0)
| ~ isa(X0,c_tptpcol_16_31868) ),
inference(ennf_transformation,[],[f37514]) ).
fof(f66305,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f44208]) ).
fof(f66306,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f66305]) ).
fof(f66315,plain,
! [X0] :
( ( ~ tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0)
| ~ tptpcol_16_31868(X0) )
& mtvisible(c_tptp_spindlecollectormt) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f77058,plain,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),
inference(cnf_transformation,[],[f10954]) ).
fof(f77548,plain,
! [X0] :
( tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ mtvisible(c_tptp_member2610_mt)
| ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ),
inference(cnf_transformation,[],[f49514]) ).
fof(f77549,plain,
( relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)
| ~ mtvisible(c_tptp_member2610_mt) ),
inference(cnf_transformation,[],[f49515]) ).
fof(f92407,plain,
! [X2,X3,X0,X1] :
( ~ isa(X0,X1)
| isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| ~ relationallexists(X2,X1,X3) ),
inference(cnf_transformation,[],[f53170]) ).
fof(f93270,plain,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt),
inference(cnf_transformation,[],[f27477]) ).
fof(f102370,plain,
! [X0] :
( ~ isa(X0,c_tptpcol_16_31868)
| tptpcol_16_31868(X0) ),
inference(cnf_transformation,[],[f60728]) ).
fof(f108033,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(cnf_transformation,[],[f66306]) ).
fof(f108042,plain,
mtvisible(c_tptp_spindlecollectormt),
inference(cnf_transformation,[],[f66315]) ).
fof(f108043,plain,
! [X0] :
( ~ tptpcol_16_31868(X0)
| ~ tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0) ),
inference(cnf_transformation,[],[f66315]) ).
fof(f112200,definition,
( spl0_894
<=> mtvisible(c_tptp_member2610_mt) ),
introduced(definition,[new_symbols(definition,[spl0_894])],[avatar_definition]) ).
fof(f112204,definition,
( spl0_895
<=> relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) ),
introduced(definition,[new_symbols(definition,[spl0_895])],[avatar_definition]) ).
fof(f112206,plain,
( relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)
| ~ spl0_895 ),
inference(avatar_component_clause,[],[f112204]) ).
fof(f112209,definition,
( spl0_896
<=> ! [X0] :
( tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) ) ),
introduced(definition,[new_symbols(definition,[spl0_896])],[avatar_definition]) ).
fof(f112210,plain,
( ! [X0] :
( ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| tptp_8_875(X0,f_relationallexistsfn(X0,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)) )
| ~ spl0_896 ),
inference(avatar_component_clause,[],[f112209]) ).
fof(f113169,plain,
( ~ spl0_894
| spl0_895 ),
inference(avatar_split_clause,[],[f77549,f112204,f112200]) ).
fof(f113170,plain,
( ~ spl0_894
| spl0_896 ),
inference(avatar_split_clause,[],[f77548,f112209,f112200]) ).
fof(f116272,plain,
( ~ mtvisible(c_tptp_spindlecollectormt)
| mtvisible(c_tptp_member2610_mt) ),
inference(resolution,[],[f93270,f108033]) ).
fof(f116273,plain,
mtvisible(c_tptp_member2610_mt),
inference(global_subsumption,[],[f116272,f108042]) ).
fof(f116274,plain,
spl0_894,
inference(avatar_split_clause,[],[f116273,f112200]) ).
fof(f116275,plain,
( tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ spl0_896 ),
inference(resolution,[],[f112210,f77058]) ).
fof(f116289,plain,
! [X0,X1] :
( ~ relationallexists(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),X1)
| isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),X1),X1) ),
inference(resolution,[],[f92407,f77058]) ).
fof(f116341,plain,
( isa(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868),c_tptpcol_16_31868)
| ~ spl0_895 ),
inference(resolution,[],[f116289,f112206]) ).
fof(f116514,plain,
( tptpcol_16_31868(f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ spl0_895 ),
inference(resolution,[],[f116341,f102370]) ).
fof(f116982,plain,
( ~ tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_relationallexistsfn(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868))
| ~ spl0_895 ),
inference(resolution,[],[f116514,f108043]) ).
fof(f116983,plain,
( $false
| ~ spl0_895
| ~ spl0_896 ),
inference(resolution,[],[f116982,f116275]) ).
fof(f116984,plain,
( ~ spl0_895
| ~ spl0_896 ),
inference(avatar_contradiction_clause,[],[f116983]) ).
cnf(s30692,plain,
( ~ spl0_894
| spl0_895 ),
inference(sat_conversion,[],[f113169]) ).
cnf(s30694,plain,
( ~ spl0_894
| spl0_896 ),
inference(sat_conversion,[],[f113170]) ).
cnf(s42187,plain,
spl0_894,
inference(sat_conversion,[],[f116274]) ).
cnf(s42623,plain,
( ~ spl0_895
| ~ spl0_896 ),
inference(sat_conversion,[],[f116984]) ).
cnf(s42627,plain,
spl0_896,
inference(rat,[],[s30694,s42187]) ).
cnf(s42628,plain,
~ spl0_895,
inference(rat,[],[s42623,s42627]) ).
cnf(s42629,plain,
$false,
inference(rat,[],[s30692,s42628,s42187]) ).
fof(f116985,plain,
$false,
inference(avatar_sat_refutation,[],[s42629]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR027+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.17 % Computer : n016.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 22:12:49 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.20 Running first-order model finding
% 0.06/0.20 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
% 19.71/3.80 % (4092693)Will run a generic schedule for satisfiability detection.
% 19.71/3.80 % (4092699)% WARNING: option uhcvi not known.
% 19.71/3.80 % (4092704)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1255558206:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2991 on theBenchmark for (2991ds/159Mi)
% 19.71/3.80 % (4092698)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1967653406_2991 on theBenchmark for (2991ds/0Mi)
% 19.71/3.80 % (4092699)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=950964497:i=135531:add=off:rawr=on_2991 on theBenchmark for (2991ds/135531Mi)
% 19.71/3.80 % (4092700)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1617063994:i=88024:add=on:rawr=on_2991 on theBenchmark for (2991ds/88024Mi)
% 19.71/3.80 % (4092701)dis+10_1_sil=32000:sp=arity:random_seed=711579431:i=103:fgj=on_2991 on theBenchmark for (2991ds/103Mi)
% 19.71/3.80 % (4092702)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1898495936:i=116_2991 on theBenchmark for (2991ds/116Mi)
% 19.71/3.80 % (4092703)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3215155225:i=131_2991 on theBenchmark for (2991ds/131Mi)
% 19.71/3.80 % (4092704)Instruction limit reached!
% 19.71/3.80 % (4092704)------------------------------
% 19.71/3.80 % (4092704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.71/3.80 % (4092704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.71/3.80 % (4092704)CaDiCaL version: 2.1.3
% 19.71/3.80 % (4092704)Termination reason: Instruction limit
% 19.71/3.80 % (4092704)Termination phase: Naming
% 19.71/3.80 % (4092704)Time elapsed: 0.075 s
% 19.71/3.80 % (4092704)Peak memory usage: 62 MB
% 19.71/3.80 % (4092704)Instructions burned: 164 (million)
% 19.71/3.80 % (4092712)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=180862632:i=714:nm=2_2990 on theBenchmark for (2990ds/714Mi)
% 19.71/3.80 % (4092701)Instruction limit reached!
% 19.71/3.80 % (4092701)------------------------------
% 19.71/3.80 % (4092701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.71/3.80 % (4092701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.71/3.80 % (4092701)CaDiCaL version: 2.1.3
% 19.71/3.80 % (4092701)Termination reason: Instruction limit
% 19.71/3.80 % (4092701)Termination phase: Preprocessing 2
% 19.71/3.80 % (4092701)Time elapsed: 0.091 s
% 19.71/3.80 % (4092701)Peak memory usage: 61 MB
% 19.71/3.80 % (4092701)Instructions burned: 103 (million)
% 19.71/3.80 % (4092702)Instruction limit reached!
% 19.71/3.80 % (4092702)------------------------------
% 19.71/3.80 % (4092702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.71/3.80 % (4092702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.71/3.80 % (4092702)CaDiCaL version: 2.1.3
% 19.71/3.80 % (4092702)Termination reason: Instruction limit
% 19.71/3.80 % (4092702)Termination phase: Preprocessing 2
% 19.71/3.80 % (4092702)Time elapsed: 0.103 s
% 19.71/3.80 % (4092702)Peak memory usage: 61 MB
% 19.71/3.80 % (4092702)Instructions burned: 116 (million)
% 19.71/3.80 % (4092703)Instruction limit reached!
% 19.71/3.80 % (4092703)------------------------------
% 19.71/3.80 % (4092703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.71/3.80 % (4092703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.71/3.80 % (4092703)CaDiCaL version: 2.1.3
% 19.71/3.80 % (4092703)Termination reason: Instruction limit
% 19.71/3.80 % (4092703)Termination phase: Preprocessing 2
% 19.71/3.80 % (4092703)Time elapsed: 0.112 s
% 19.71/3.80 % (4092703)Peak memory usage: 61 MB
% 19.71/3.80 % (4092703)Instructions burned: 132 (million)
% 19.71/3.80 % (4092714)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=317317874:i=131:bd=preordered:fsd=on_2990 on theBenchmark for (2990ds/131Mi)
% 19.71/3.80 % (4092715)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=2201411361:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2990 on theBenchmark for (2990ds/684Mi)
% 19.71/3.80 % (4092717)ott-21_1_sil=16000:fs=off:random_seed=1597557265:i=180:av=off:fsr=off_2990 on theBenchmark for (2990ds/180Mi)
% 19.71/3.80 % (4092714)Instruction limit reached!
% 19.71/3.80 % (4092714)------------------------------
% 19.71/3.80 % (4092714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.71/3.80 % (4092714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092714)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092714)Termination reason: Instruction limit
% 47.37/7.70 % (4092714)Termination phase: Preprocessing 2
% 47.37/7.70 % (4092714)Time elapsed: 0.108 s
% 47.37/7.70 % (4092714)Peak memory usage: 61 MB
% 47.37/7.70 % (4092714)Instructions burned: 132 (million)
% 47.37/7.70 % (4092720)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2201143625:i=477:bd=all_2989 on theBenchmark for (2989ds/477Mi)
% 47.37/7.70 % (4092717)Instruction limit reached!
% 47.37/7.70 % (4092717)------------------------------
% 47.37/7.70 % (4092717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092717)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092717)Termination reason: Instruction limit
% 47.37/7.70 % (4092717)Termination phase: Preprocessing 3
% 47.37/7.70 % (4092717)Time elapsed: 0.128 s
% 47.37/7.70 % (4092717)Peak memory usage: 62 MB
% 47.37/7.70 % (4092717)Instructions burned: 181 (million)
% 47.37/7.70 % (4092722)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4121310153:fmbsr=1.3:i=865:ins=25_2988 on theBenchmark for (2988ds/865Mi)
% 47.37/7.70 % (4092712)Instruction limit reached!
% 47.37/7.70 % (4092712)------------------------------
% 47.37/7.70 % (4092712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092712)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092712)Termination reason: Instruction limit
% 47.37/7.70 % (4092712)Termination phase: Finite model building preprocessing
% 47.37/7.70 % (4092712)Time elapsed: 0.238 s
% 47.37/7.70 % (4092712)Peak memory usage: 68 MB
% 47.37/7.70 % (4092712)Instructions burned: 717 (million)
% 47.37/7.70 % (4092724)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=128344366:i=1179_2988 on theBenchmark for (2988ds/1179Mi)
% 47.37/7.70 % (4092720)Instruction limit reached!
% 47.37/7.70 % (4092720)------------------------------
% 47.37/7.70 % (4092720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092720)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092720)Termination reason: Instruction limit
% 47.37/7.70 % (4092720)Termination phase: Property scanning
% 47.37/7.70 % (4092720)Time elapsed: 0.296 s
% 47.37/7.70 % (4092720)Peak memory usage: 66 MB
% 47.37/7.70 % (4092720)Instructions burned: 477 (million)
% 47.37/7.70 % (4092715)Instruction limit reached!
% 47.37/7.70 % (4092715)------------------------------
% 47.37/7.70 % (4092715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092715)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092715)Termination reason: Instruction limit
% 47.37/7.70 % (4092715)Termination phase: Property scanning
% 47.37/7.70 % (4092715)Time elapsed: 0.435 s
% 47.37/7.70 % (4092715)Peak memory usage: 73 MB
% 47.37/7.70 % (4092715)Instructions burned: 686 (million)
% 47.37/7.70 % (4092726)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1166483337:i=889:ins=1_2985 on theBenchmark for (2985ds/889Mi)
% 47.37/7.70 % (4092727)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=3582127103:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2985 on theBenchmark for (2985ds/692Mi)
% 47.37/7.70 % (4092724)Instruction limit reached!
% 47.37/7.70 % (4092724)------------------------------
% 47.37/7.70 % (4092724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.37/7.70 % (4092724)CaDiCaL version: 2.1.3
% 47.37/7.70 % (4092724)Termination reason: Instruction limit
% 47.37/7.70 % (4092724)Termination phase: Saturation
% 47.37/7.70 % (4092724)Time elapsed: 0.375 s
% 47.37/7.70 % (4092724)Peak memory usage: 81 MB
% 47.37/7.70 % (4092724)Instructions burned: 1180 (million)
% 47.37/7.70 % (4092730)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1214924892:i=879:kws=inv_precedence:fsr=off_2984 on theBenchmark for (2984ds/879Mi)
% 47.37/7.70 % (4092722)Instruction limit reached!
% 47.37/7.70 % (4092722)------------------------------
% 47.37/7.70 % (4092722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.37/7.70 % (4092722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092722)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092722)Termination reason: Instruction limit
% 29.21/8.64 % (4092722)Termination phase: Finite model building preprocessing
% 29.21/8.64 % (4092722)Time elapsed: 0.500 s
% 29.21/8.64 % (4092722)Peak memory usage: 86 MB
% 29.21/8.64 % (4092722)Instructions burned: 865 (million)
% 29.21/8.64 % (4092732)fmb+10_1_sil=64000:random_seed=262888379:i=22061:nm=2:gsp=on_2983 on theBenchmark for (2983ds/22061Mi)
% 29.21/8.64 % (4092727)Instruction limit reached!
% 29.21/8.64 % (4092727)------------------------------
% 29.21/8.64 % (4092727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092727)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092727)Termination reason: Instruction limit
% 29.21/8.64 % (4092727)Termination phase: Property scanning
% 29.21/8.64 % (4092727)Time elapsed: 0.445 s
% 29.21/8.64 % (4092727)Peak memory usage: 76 MB
% 29.21/8.64 % (4092727)Instructions burned: 694 (million)
% 29.21/8.64 % (4092730)Instruction limit reached!
% 29.21/8.64 % (4092730)------------------------------
% 29.21/8.64 % (4092730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092730)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092730)Termination reason: Instruction limit
% 29.21/8.64 % (4092730)Termination phase: Saturation
% 29.21/8.64 % (4092730)Time elapsed: 0.322 s
% 29.21/8.64 % (4092730)Peak memory usage: 91 MB
% 29.21/8.64 % (4092730)Instructions burned: 879 (million)
% 29.21/8.64 % (4092734)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1239536258:i=9515:nm=5_2980 on theBenchmark for (2980ds/9515Mi)
% 29.21/8.64 % (4092735)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=36831110:fmbsr=1.7:i=920_2980 on theBenchmark for (2980ds/920Mi)
% 29.21/8.64 % (4092726)Instruction limit reached!
% 29.21/8.64 % (4092726)------------------------------
% 29.21/8.64 % (4092726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092726)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092726)Termination reason: Instruction limit
% 29.21/8.64 % (4092726)Termination phase: Finite model building preprocessing
% 29.21/8.64 % (4092726)Time elapsed: 0.539 s
% 29.21/8.64 % (4092726)Peak memory usage: 86 MB
% 29.21/8.64 % (4092726)Instructions burned: 890 (million)
% 29.21/8.64 % (4092738)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1154769277:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 29.21/8.64 % (4092735)Instruction limit reached!
% 29.21/8.64 % (4092735)------------------------------
% 29.21/8.64 % (4092735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092735)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092735)Termination reason: Instruction limit
% 29.21/8.64 % (4092735)Termination phase: Finite model building preprocessing
% 29.21/8.64 % (4092735)Time elapsed: 0.310 s
% 29.21/8.64 % (4092735)Peak memory usage: 79 MB
% 29.21/8.64 % (4092735)Instructions burned: 920 (million)
% 29.21/8.64 % (4092740)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3656346357:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 29.21/8.64 % TRYING [1]
% 29.21/8.64 % TRYING [2]
% 29.21/8.64 % (4092740)Instruction limit reached!
% 29.21/8.64 % (4092740)------------------------------
% 29.21/8.64 % (4092740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092740)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092740)Termination reason: Instruction limit
% 29.21/8.64 % (4092740)Termination phase: Saturation
% 29.21/8.64 % (4092740)Time elapsed: 0.440 s
% 29.21/8.64 % (4092740)Peak memory usage: 82 MB
% 29.21/8.64 % (4092740)Instructions burned: 1474 (million)
% 29.21/8.64 % (4092742)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=476449588:i=6324_2972 on theBenchmark for (2972ds/6324Mi)
% 29.21/8.64 % TRYING [3]
% 29.21/8.64 % TRYING [1]
% 29.21/8.64 % TRYING [20]
% 29.21/8.64 % (4092742)Cannot represent all propositional literals internally
% 29.21/8.64 % (4092742)Refutation not found, incomplete strategy
% 29.21/8.64 % (4092742)------------------------------
% 29.21/8.64 % (4092742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092742)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092742)Termination reason: Refutation not found, incomplete strategy
% 29.21/8.64 % (4092742)Time elapsed: 0.863 s
% 29.21/8.64 % (4092742)Peak memory usage: 115 MB
% 29.21/8.64 % (4092742)Instructions burned: 2685 (million)
% 29.21/8.64 % (4092742)------------------------------
% 29.21/8.64 % (4092742)------------------------------
% 29.21/8.64 % (4092745)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3044627136:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 29.21/8.64 % TRYING [4]
% 29.21/8.64 % (4092745)Instruction limit reached!
% 29.21/8.64 % (4092745)------------------------------
% 29.21/8.64 % (4092745)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092745)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092745)Termination reason: Instruction limit
% 29.21/8.64 % (4092745)Termination phase: Finite model building preprocessing
% 29.21/8.64 % (4092745)Time elapsed: 0.710 s
% 29.21/8.64 % (4092745)Peak memory usage: 139 MB
% 29.21/8.64 % (4092745)Instructions burned: 2175 (million)
% 29.21/8.64 % (4092747)ott-2_1_sil=16000:newcnf=on:random_seed=3033957102:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 29.21/8.64 % TRYING [2]
% 29.21/8.64 % (4092747)Instruction limit reached!
% 29.21/8.64 % (4092747)------------------------------
% 29.21/8.64 % (4092747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092747)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092747)Termination reason: Instruction limit
% 29.21/8.64 % (4092747)Termination phase: Saturation
% 29.21/8.64 % (4092747)Time elapsed: 0.300 s
% 29.21/8.64 % (4092747)Peak memory usage: 77 MB
% 29.21/8.64 % (4092747)Instructions burned: 870 (million)
% 29.21/8.64 % (4092749)ott+10_1_sil=32000:tgt=ground:random_seed=3395812725:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 29.21/8.64 % (4092738)Instruction limit reached!
% 29.21/8.64 % (4092738)------------------------------
% 29.21/8.64 % (4092738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092738)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092738)Termination reason: Instruction limit
% 29.21/8.64 % (4092738)Termination phase: Saturation
% 29.21/8.64 % (4092738)Time elapsed: 3.217 s
% 29.21/8.64 % (4092738)Peak memory usage: 159 MB
% 29.21/8.64 % (4092738)Instructions burned: 5131 (million)
% 29.21/8.64 % (4092751)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1246504628:i=54282_2947 on theBenchmark for (2947ds/54282Mi)
% 29.21/8.64 % (4092734)Instruction limit reached!
% 29.21/8.64 % (4092734)------------------------------
% 29.21/8.64 % (4092734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092734)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092734)Termination reason: Instruction limit
% 29.21/8.64 % (4092734)Termination phase: Finite model building constraint generation
% 29.21/8.64 % (4092734)Time elapsed: 3.815 s
% 29.21/8.64 % (4092734)Peak memory usage: 509 MB
% 29.21/8.64 % (4092734)Instructions burned: 9515 (million)
% 29.21/8.64 % (4092753)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2950277117:i=3512:aac=none_2941 on theBenchmark for (2941ds/3512Mi)
% 29.21/8.64 % TRYING [5]
% 29.21/8.64 % (4092749)Instruction limit reached!
% 29.21/8.64 % (4092749)------------------------------
% 29.21/8.64 % (4092749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092749)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092749)Termination reason: Instruction limit
% 29.21/8.64 % (4092749)Termination phase: Saturation
% 29.21/8.64 % (4092749)Time elapsed: 1.668 s
% 29.21/8.64 % (4092749)Peak memory usage: 144 MB
% 29.21/8.64 % (4092749)Instructions burned: 5119 (million)
% 29.21/8.64 % (4092755)dis+21_1_sil=32000:sas=cadical:random_seed=3373410113:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi)
% 29.21/8.64 % TRYING [1]
% 29.21/8.64 % TRYING [2]
% 29.21/8.64 % TRYING [3]
% 29.21/8.64 % (4092755)Instruction limit reached!
% 29.21/8.64 % (4092755)------------------------------
% 29.21/8.64 % (4092755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092755)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092755)Termination reason: Instruction limit
% 29.21/8.64 % (4092755)Termination phase: Saturation
% 29.21/8.64 % (4092755)Time elapsed: 1.104 s
% 29.21/8.64 % (4092755)Peak memory usage: 106 MB
% 29.21/8.64 % (4092755)Instructions burned: 3774 (million)
% 29.21/8.64 % (4092757)ott+11_1_sil=16000:gs=on:random_seed=2568248286:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2925 on theBenchmark for (2925ds/2251Mi)
% 29.21/8.64 % (4092753)Instruction limit reached!
% 29.21/8.64 % (4092753)------------------------------
% 29.21/8.64 % (4092753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.21/8.64 % (4092753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.21/8.64 % (4092753)CaDiCaL version: 2.1.3
% 29.21/8.64 % (4092753)Termination reason: Instruction limit
% 29.21/8.64 % (4092753)Termination phase: Saturation
% 29.21/8.64 % (4092753)Time elapsed: 2.147 s
% 29.21/8.64 % (4092753)Peak memory usage: 117 MB
% 29.21/8.64 % (4092753)Instructions burned: 3512 (million)
% 29.21/8.64 % (4092759)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1076671907:fmbsr=1.6:i=67534_2920 on theBenchmark for (2920ds/67534Mi)
% 29.21/8.64 % (4092757) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4092693-4092757"...
% 29.21/8.64 % (4092757)...printing done.
% 29.21/8.64 % (4092757)Refutation found. Thanks to Tanya!
% 29.21/8.64 % SZS status Theorem for theBenchmark
% 29.21/8.64 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/8.70 % (4092757)------------------------------
% 0.18/8.70 % (4092757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/8.70 % (4092757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/8.70 % (4092757)CaDiCaL version: 2.1.3
% 0.18/8.70 % (4092757)Termination reason: Refutation
% 0.18/8.70 % (4092757)Time elapsed: 0.800 s
% 0.18/8.70 % (4092757)Peak memory usage: 106 MB
% 0.18/8.70 % (4092757)Instructions burned: 2404 (million)
% 0.18/8.70 % (4092693)Success in time 8.431 s
% 0.18/8.70 % Vampire exiting
%------------------------------------------------------------------------------