%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR027+3 : 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 : n017.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 6.76s 1.43s
% Output : Refutation 6.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 11
% Syntax : Number of formulae : 62 ( 14 unt; 3 def)
% Number of atoms : 137 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 134 ( 59 ~; 59 |; 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 : 51 ( 0 sgn 49 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f406,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+2.ax',ax2_406) ).
fof(f407,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+2.ax',ax2_407) ).
fof(f1584,axiom,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1584) ).
fof(f2362,axiom,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2362) ).
fof(f4341,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+2.ax',ax2_4341) ).
fof(f7347,axiom,
! [X0] :
( isa(X0,c_tptpcol_16_31868)
=> tptpcol_16_31868(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7347) ).
fof(f7997,axiom,
! [X0,X1] :
( ( mtvisible(X0)
& genlmt(X0,X1) )
=> mtvisible(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7997) ).
fof(f8006,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',query127) ).
fof(f8007,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)],[f8006]) ).
fof(f8874,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,[],[f406]) ).
fof(f8875,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,[],[f8874]) ).
fof(f8876,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,[],[f407]) ).
fof(f10468,plain,
! [X0,X1,X2,X3] :
( isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| ~ isa(X0,X1)
| ~ relationallexists(X2,X1,X3) ),
inference(ennf_transformation,[],[f4341]) ).
fof(f10469,plain,
! [X0,X1,X2,X3] :
( isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| ~ isa(X0,X1)
| ~ relationallexists(X2,X1,X3) ),
inference(flattening,[],[f10468]) ).
fof(f12892,plain,
! [X0] :
( tptpcol_16_31868(X0)
| ~ isa(X0,c_tptpcol_16_31868) ),
inference(ennf_transformation,[],[f7347]) ).
fof(f13390,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(ennf_transformation,[],[f7997]) ).
fof(f13391,plain,
! [X0,X1] :
( mtvisible(X1)
| ~ mtvisible(X0)
| ~ genlmt(X0,X1) ),
inference(flattening,[],[f13390]) ).
fof(f13400,plain,
! [X0] :
( ( ~ tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0)
| ~ tptpcol_16_31868(X0) )
& mtvisible(c_tptp_spindlecollectormt) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f13799,plain,
! [X0] :
( ~ isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| ~ mtvisible(c_tptp_member2610_mt)
| 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)) ),
inference(cnf_transformation,[],[f8875]) ).
fof(f13800,plain,
( ~ mtvisible(c_tptp_member2610_mt)
| relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) ),
inference(cnf_transformation,[],[f8876]) ).
fof(f14952,plain,
isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),
inference(cnf_transformation,[],[f1584]) ).
fof(f15719,plain,
genlmt(c_tptp_spindlecollectormt,c_tptp_member2610_mt),
inference(cnf_transformation,[],[f2362]) ).
fof(f17667,plain,
! [X2,X3,X0,X1] :
( ~ relationallexists(X2,X1,X3)
| ~ isa(X0,X1)
| isa(f_relationallexistsfn(X0,X2,X1,X3),X3) ),
inference(cnf_transformation,[],[f10469]) ).
fof(f20188,plain,
! [X0] :
( ~ isa(X0,c_tptpcol_16_31868)
| tptpcol_16_31868(X0) ),
inference(cnf_transformation,[],[f12892]) ).
fof(f20678,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| ~ mtvisible(X0)
| mtvisible(X1) ),
inference(cnf_transformation,[],[f13391]) ).
fof(f20687,plain,
! [X0] :
( ~ tptpcol_16_31868(X0)
| ~ tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0) ),
inference(cnf_transformation,[],[f13400]) ).
fof(f20688,plain,
mtvisible(c_tptp_spindlecollectormt),
inference(cnf_transformation,[],[f13400]) ).
fof(f20899,plain,
! [X0] :
( isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| mtvisible(c_tptp_member2610_mt)
| ~ 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)) ),
inference(consistent_polarity_flipping,[],[f13799]) ).
fof(f20900,plain,
( mtvisible(c_tptp_member2610_mt)
| relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868) ),
inference(consistent_polarity_flipping,[],[f13800]) ).
fof(f21583,plain,
~ isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)),
inference(consistent_polarity_flipping,[],[f14952]) ).
fof(f23154,plain,
! [X2,X3,X0,X1] :
( ~ isa(f_relationallexistsfn(X0,X2,X1,X3),X3)
| isa(X0,X1)
| ~ relationallexists(X2,X1,X3) ),
inference(consistent_polarity_flipping,[],[f17667]) ).
fof(f25487,plain,
! [X0] :
( isa(X0,c_tptpcol_16_31868)
| tptpcol_16_31868(X0) ),
inference(consistent_polarity_flipping,[],[f20188]) ).
fof(f25936,plain,
! [X0,X1] :
( ~ genlmt(X0,X1)
| mtvisible(X0)
| ~ mtvisible(X1) ),
inference(consistent_polarity_flipping,[],[f20678]) ).
fof(f25938,plain,
~ mtvisible(c_tptp_spindlecollectormt),
inference(consistent_polarity_flipping,[],[f20688]) ).
fof(f25939,plain,
! [X0] :
( ~ tptpcol_16_31868(X0)
| tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,X0) ),
inference(consistent_polarity_flipping,[],[f20687]) ).
fof(f28230,definition,
( spl0_491
<=> 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_491])],[avatar_definition]) ).
fof(f28232,plain,
( relationallexists(c_tptp_8_875,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent),c_tptpcol_16_31868)
| ~ spl0_491 ),
inference(avatar_component_clause,[],[f28230]) ).
fof(f28234,definition,
( spl0_492
<=> mtvisible(c_tptp_member2610_mt) ),
introduced(definition,[new_symbols(definition,[spl0_492])],[avatar_definition]) ).
fof(f28236,plain,
( mtvisible(c_tptp_member2610_mt)
| ~ spl0_492 ),
inference(avatar_component_clause,[],[f28234]) ).
fof(f28239,definition,
( spl0_493
<=> ! [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)) ) ),
introduced(definition,[new_symbols(definition,[spl0_493])],[avatar_definition]) ).
fof(f28240,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))
| isa(X0,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent)) )
| ~ spl0_493 ),
inference(avatar_component_clause,[],[f28239]) ).
fof(f29365,plain,
( spl0_491
| spl0_492 ),
inference(avatar_split_clause,[],[f20900,f28234,f28230]) ).
fof(f29366,plain,
( spl0_492
| spl0_493 ),
inference(avatar_split_clause,[],[f20899,f28239,f28234]) ).
fof(f29657,plain,
( mtvisible(c_tptp_spindlecollectormt)
| ~ mtvisible(c_tptp_member2610_mt) ),
inference(resolution,[],[f15719,f25936]) ).
fof(f29658,plain,
~ mtvisible(c_tptp_member2610_mt),
inference(forward_subsumption_resolution,[],[f29657,f25938]) ).
fof(f29659,plain,
( $false
| ~ spl0_492 ),
inference(forward_subsumption_resolution,[],[f29658,f28236]) ).
fof(f29660,plain,
~ spl0_492,
inference(avatar_contradiction_clause,[],[f29659]) ).
fof(f32757,plain,
! [X2,X0,X1] :
( ~ relationallexists(X1,X2,c_tptpcol_16_31868)
| isa(X0,X2)
| tptpcol_16_31868(f_relationallexistsfn(X0,X1,X2,c_tptpcol_16_31868)) ),
inference(resolution,[],[f25487,f23154]) ).
fof(f32912,plain,
( ! [X0] :
( tptpcol_16_31868(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)) )
| ~ spl0_491 ),
inference(resolution,[],[f32757,f28232]) ).
fof(f33601,plain,
( ! [X0] :
( tptp_8_875(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,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)) )
| ~ spl0_491 ),
inference(resolution,[],[f32912,f25939]) ).
fof(f33604,plain,
( isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| ~ spl0_491
| ~ spl0_493 ),
inference(resolution,[],[f33601,f28240]) ).
fof(f33605,plain,
( isa(c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786,f_subcollectionofwithrelationfromtypefn(c_unitvectorinterval,c_directionoftranslation_throughout,c_movement_translationevent))
| ~ spl0_491
| ~ spl0_493 ),
inference(duplicate_literal_removal,[],[f33604]) ).
fof(f33606,plain,
( $false
| ~ spl0_491
| ~ spl0_493 ),
inference(forward_subsumption_resolution,[],[f33605,f21583]) ).
fof(f33607,plain,
( ~ spl0_491
| ~ spl0_493 ),
inference(avatar_contradiction_clause,[],[f33606]) ).
cnf(s642,plain,
( spl0_491
| spl0_492 ),
inference(sat_conversion,[],[f29365]) ).
cnf(s643,plain,
( spl0_492
| spl0_493 ),
inference(sat_conversion,[],[f29366]) ).
cnf(s699,plain,
~ spl0_492,
inference(sat_conversion,[],[f29660]) ).
cnf(s869,plain,
( ~ spl0_491
| ~ spl0_493 ),
inference(sat_conversion,[],[f33607]) ).
cnf(s925,plain,
spl0_493,
inference(rat,[],[s643,s699]) ).
cnf(s926,plain,
~ spl0_491,
inference(rat,[],[s869,s925]) ).
cnf(s927,plain,
$false,
inference(rat,[],[s642,s699,s926]) ).
fof(f33608,plain,
$false,
inference(avatar_sat_refutation,[],[s927]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR027+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n017.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:03:07 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.76/1.43 % (4090323)Will run a generic schedule for satisfiability detection.
% 6.76/1.43 % (4090341)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4107408933:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 6.76/1.43 % (4090340)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3618748468:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 6.76/1.43 % (4090336)% WARNING: option uhcvi not known.
% 6.76/1.43 % (4090335)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4011979172_2998 on theBenchmark for (2998ds/0Mi)
% 6.76/1.43 % (4090336)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4198507588:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 6.76/1.43 % (4090337)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1742638101:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 6.76/1.43 % (4090338)dis+10_1_sil=32000:sp=arity:random_seed=567350177:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 6.76/1.43 % (4090339)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1736022690:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 6.76/1.43 % (4090341)Instruction limit reached!
% 6.76/1.43 % (4090341)------------------------------
% 6.76/1.43 % (4090341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090341)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090341)Termination reason: Instruction limit
% 6.76/1.43 % (4090341)Termination phase: Saturation
% 6.76/1.43 % (4090341)Time elapsed: 0.089 s
% 6.76/1.43 % (4090341)Peak memory usage: 25 MB
% 6.76/1.43 % (4090341)Instructions burned: 160 (million)
% 6.76/1.43 % (4090338)Instruction limit reached!
% 6.76/1.43 % (4090338)------------------------------
% 6.76/1.43 % (4090338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090338)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090338)Termination reason: Instruction limit
% 6.76/1.43 % (4090338)Termination phase: Saturation
% 6.76/1.43 % (4090338)Time elapsed: 0.098 s
% 6.76/1.43 % (4090338)Peak memory usage: 22 MB
% 6.76/1.43 % (4090338)Instructions burned: 104 (million)
% 6.76/1.43 % (4090349)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2133073161:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 6.76/1.43 % (4090340)Instruction limit reached!
% 6.76/1.43 % (4090340)------------------------------
% 6.76/1.43 % (4090340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090340)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090340)Termination reason: Instruction limit
% 6.76/1.43 % (4090340)Termination phase: Saturation
% 6.76/1.43 % (4090340)Time elapsed: 0.114 s
% 6.76/1.43 % (4090340)Peak memory usage: 23 MB
% 6.76/1.43 % (4090340)Instructions burned: 132 (million)
% 6.76/1.43 % (4090339)Instruction limit reached!
% 6.76/1.43 % (4090339)------------------------------
% 6.76/1.43 % (4090339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090339)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090339)Termination reason: Instruction limit
% 6.76/1.43 % (4090339)Termination phase: Blocked clause elimination
% 6.76/1.43 % (4090339)Time elapsed: 0.118 s
% 6.76/1.43 % (4090339)Peak memory usage: 24 MB
% 6.76/1.43 % (4090339)Instructions burned: 116 (million)
% 6.76/1.43 % (4090350)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1671669786:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 6.76/1.43 % (4090353)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=354237023:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 6.76/1.43 % (4090355)ott-21_1_sil=16000:fs=off:random_seed=2402322608:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 6.76/1.43 % (4090350)Instruction limit reached!
% 6.76/1.43 % (4090350)------------------------------
% 6.76/1.43 % (4090350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090350)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090350)Termination reason: Instruction limit
% 6.76/1.43 % (4090350)Termination phase: Blocked clause elimination
% 6.76/1.43 % (4090350)Time elapsed: 0.081 s
% 6.76/1.43 % (4090350)Peak memory usage: 24 MB
% 6.76/1.43 % (4090350)Instructions burned: 132 (million)
% 6.76/1.43 % (4090363)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2693218528:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 6.76/1.43 % (4090355)Instruction limit reached!
% 6.76/1.43 % (4090355)------------------------------
% 6.76/1.43 % (4090355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090355)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090355)Termination reason: Instruction limit
% 6.76/1.43 % (4090355)Termination phase: Saturation
% 6.76/1.43 % (4090355)Time elapsed: 0.178 s
% 6.76/1.43 % (4090355)Peak memory usage: 23 MB
% 6.76/1.43 % (4090355)Instructions burned: 181 (million)
% 6.76/1.43 % (4090367)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3079882546:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 6.76/1.43 % TRYING [1]
% 6.76/1.43 % TRYING [2]
% 6.76/1.43 % (4090363)Instruction limit reached!
% 6.76/1.43 % (4090363)------------------------------
% 6.76/1.43 % (4090363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090363)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090363)Termination reason: Instruction limit
% 6.76/1.43 % (4090363)Termination phase: Saturation
% 6.76/1.43 % (4090363)Time elapsed: 0.247 s
% 6.76/1.43 % (4090363)Peak memory usage: 28 MB
% 6.76/1.43 % (4090363)Instructions burned: 479 (million)
% 6.76/1.43 % TRYING [1]
% 6.76/1.43 % (4090370)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3111224673:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 6.76/1.43 % TRYING [3]
% 6.76/1.43 % TRYING [2]
% 6.76/1.43 % TRYING [3]
% 6.76/1.43 % (4090349)Instruction limit reached!
% 6.76/1.43 % (4090349)------------------------------
% 6.76/1.43 % (4090349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090349)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090349)Termination reason: Instruction limit
% 6.76/1.43 % (4090349)Termination phase: Finite model building constraint generation
% 6.76/1.43 % (4090349)Time elapsed: 0.571 s
% 6.76/1.43 % (4090349)Peak memory usage: 41 MB
% 6.76/1.43 % (4090349)Instructions burned: 717 (million)
% 6.76/1.43 % TRYING [4]
% 6.76/1.43 % (4090374)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3817302947:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 6.76/1.43 % TRYING [1]
% 6.76/1.43 % (4090353)Instruction limit reached!
% 6.76/1.43 % (4090353)------------------------------
% 6.76/1.43 % (4090353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090353)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090353)Termination reason: Instruction limit
% 6.76/1.43 % (4090353)Termination phase: Saturation
% 6.76/1.43 % (4090353)Time elapsed: 0.564 s
% 6.76/1.43 % (4090353)Peak memory usage: 35 MB
% 6.76/1.43 % (4090353)Instructions burned: 684 (million)
% 6.76/1.43 % (4090376)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=710624253:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 6.76/1.43 % TRYING [2]
% 6.76/1.43 % (4090370)Instruction limit reached!
% 6.76/1.43 % (4090370)------------------------------
% 6.76/1.43 % (4090370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090370)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090370)Termination reason: Instruction limit
% 6.76/1.43 % (4090370)Termination phase: Saturation
% 6.76/1.43 % (4090370)Time elapsed: 0.384 s
% 6.76/1.43 % (4090370)Peak memory usage: 47 MB
% 6.76/1.43 % (4090370)Instructions burned: 1179 (million)
% 6.76/1.43 % (4090379)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=120683291:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 6.76/1.43 % (4090367)Instruction limit reached!
% 6.76/1.43 % (4090367)------------------------------
% 6.76/1.43 % (4090367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.43 % (4090367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.43 % (4090367)CaDiCaL version: 2.1.3
% 6.76/1.43 % (4090367)Termination reason: Instruction limit
% 6.76/1.43 % (4090367)Termination phase: Finite model building SAT solving
% 6.76/1.43 % (4090367)Time elapsed: 0.535 s
% 6.76/1.43 % (4090367)Peak memory usage: 41 MB
% 6.76/1.43 % (4090367)Instructions burned: 865 (million)
% 6.76/1.43 % (4090381)fmb+10_1_sil=64000:random_seed=3289556065:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 6.76/1.43 % TRYING [5]
% 6.76/1.43 % (4090376) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4090323-4090376"...
% 6.76/1.43 % (4090376)...printing done.
% 6.76/1.43 % (4090376)Refutation found. Thanks to Tanya!
% 6.76/1.43 % SZS status Theorem for theBenchmark
% 6.76/1.43 % SZS output start Proof for theBenchmark
% See solution above
% 6.76/1.44 % (4090376)------------------------------
% 6.76/1.44 % (4090376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.76/1.44 % (4090376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.44 % (4090376)CaDiCaL version: 2.1.3
% 6.76/1.44 % (4090376)Termination reason: Refutation
% 6.76/1.44 % (4090376)Time elapsed: 0.273 s
% 6.76/1.44 % (4090376)Peak memory usage: 33 MB
% 6.76/1.44 % (4090376)Instructions burned: 438 (million)
% 6.76/1.44 % (4090323)Success in time 1.205 s
% 6.76/1.44 % Vampire exiting
%------------------------------------------------------------------------------