%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV096+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 11:23:17 AM UTC 2026
% Result : Theorem 169.16s 27.45s
% Output : Refutation 169.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 52 ( 14 unt; 0 def)
% Number of atoms : 112 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 102 ( 42 ~; 29 |; 14 &)
% ( 9 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 47 ( 46 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f615,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssertion) ).
fof(f616,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f615]) ).
fof(f617,axiom,
! [X0] :
( ~ v4(X0)
<=> v133774(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_11138) ).
fof(f618,axiom,
! [X0] :
( ~ v133774(X0)
<=> v133775(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_11137) ).
fof(f619,axiom,
! [X0] :
( v133775(X0)
<=> ( v133777(X0)
& v133789(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_26827) ).
fof(f620,axiom,
! [X0] :
( v133789(X0)
<=> ( v133779(X0,bitIndex0)
| v133779(X0,bitIndex1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3137) ).
fof(f621,axiom,
! [X0] :
( ~ v133777(X0)
<=> v133778(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_11136) ).
fof(f622,axiom,
! [X0] :
( v133778(X0)
<=> ( v133779(X0,bitIndex0)
& v133779(X0,bitIndex1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3136) ).
fof(f623,axiom,
! [X0] :
( v133779(X0,bitIndex0)
<=> v133780(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_43639) ).
fof(f624,axiom,
! [X0] :
( v133779(X0,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_43638) ).
fof(f625,axiom,
! [X0] :
( v133780(X0)
<=> ( v133782(X0)
& v133786(X0,bitIndex5) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3135) ).
fof(f633,axiom,
! [X0] : ~ v133786(X0,bitIndex5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addZeroExtensionConstraint_15) ).
fof(f134685,plain,
! [X0] : v133779(X0,bitIndex1),
inference(true_and_false_elimination,[],[f624]) ).
fof(f173411,plain,
! [X0] :
( ~ v4(X0)
=> v133774(X0) ),
inference(unused_predicate_definition_removal,[],[f617]) ).
fof(f173412,plain,
! [X0] :
( v133775(X0)
=> ~ v133774(X0) ),
inference(unused_predicate_definition_removal,[],[f618]) ).
fof(f173413,plain,
! [X0] :
( ( v133777(X0)
& v133789(X0) )
=> v133775(X0) ),
inference(unused_predicate_definition_removal,[],[f619]) ).
fof(f173414,plain,
! [X0] :
( ~ v133777(X0)
=> v133778(X0) ),
inference(unused_predicate_definition_removal,[],[f621]) ).
fof(f173415,plain,
! [X0] :
( v133778(X0)
=> ( v133779(X0,bitIndex0)
& v133779(X0,bitIndex1) ) ),
inference(unused_predicate_definition_removal,[],[f622]) ).
fof(f173416,plain,
! [X0] :
( ( v133779(X0,bitIndex0)
| v133779(X0,bitIndex1) )
=> v133789(X0) ),
inference(unused_predicate_definition_removal,[],[f620]) ).
fof(f174753,plain,
? [X0] :
( ~ v4(X0)
& reachableState(X0) ),
inference(ennf_transformation,[],[f616]) ).
fof(f174754,plain,
! [X0] :
( v133774(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f173411]) ).
fof(f174755,plain,
! [X0] :
( ~ v133774(X0)
| ~ v133775(X0) ),
inference(ennf_transformation,[],[f173412]) ).
fof(f174756,plain,
! [X0] :
( v133775(X0)
| ~ v133777(X0)
| ~ v133789(X0) ),
inference(ennf_transformation,[],[f173413]) ).
fof(f174757,plain,
! [X0] :
( v133775(X0)
| ~ v133777(X0)
| ~ v133789(X0) ),
inference(flattening,[],[f174756]) ).
fof(f174758,plain,
! [X0] :
( v133789(X0)
| ( ~ v133779(X0,bitIndex0)
& ~ v133779(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f173416]) ).
fof(f174759,plain,
! [X0] :
( v133778(X0)
| v133777(X0) ),
inference(ennf_transformation,[],[f173414]) ).
fof(f174760,plain,
! [X0] :
( ( v133779(X0,bitIndex0)
& v133779(X0,bitIndex1) )
| ~ v133778(X0) ),
inference(ennf_transformation,[],[f173415]) ).
fof(f250235,plain,
( ~ v4(sK27356)
& reachableState(sK27356) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27356]),skolemize(X0,sK27356)],[f174753]) ).
fof(f250236,plain,
! [X0] :
( ( v133779(X0,bitIndex0)
| ~ v133780(X0) )
& ( v133780(X0)
| ~ v133779(X0,bitIndex0) ) ),
inference(nnf_transformation,[],[f623]) ).
fof(f250237,plain,
! [X0] :
( ( v133780(X0)
| ~ v133782(X0)
| ~ v133786(X0,bitIndex5) )
& ( ( v133782(X0)
& v133786(X0,bitIndex5) )
| ~ v133780(X0) ) ),
inference(nnf_transformation,[],[f625]) ).
fof(f250238,plain,
! [X0] :
( ( v133780(X0)
| ~ v133782(X0)
| ~ v133786(X0,bitIndex5) )
& ( ( v133782(X0)
& v133786(X0,bitIndex5) )
| ~ v133780(X0) ) ),
inference(flattening,[],[f250237]) ).
fof(f429112,plain,
~ v4(sK27356),
inference(cnf_transformation,[],[f250235]) ).
fof(f429113,plain,
! [X0] :
( v133774(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f174754]) ).
fof(f429114,plain,
! [X0] :
( ~ v133775(X0)
| ~ v133774(X0) ),
inference(cnf_transformation,[],[f174755]) ).
fof(f429115,plain,
! [X0] :
( v133775(X0)
| ~ v133777(X0)
| ~ v133789(X0) ),
inference(cnf_transformation,[],[f174757]) ).
fof(f429116,plain,
! [X0] :
( v133789(X0)
| ~ v133779(X0,bitIndex1) ),
inference(cnf_transformation,[],[f174758]) ).
fof(f429118,plain,
! [X0] :
( v133777(X0)
| v133778(X0) ),
inference(cnf_transformation,[],[f174759]) ).
fof(f429120,plain,
! [X0] :
( ~ v133778(X0)
| v133779(X0,bitIndex0) ),
inference(cnf_transformation,[],[f174760]) ).
fof(f429121,plain,
! [X0] :
( ~ v133779(X0,bitIndex0)
| v133780(X0) ),
inference(cnf_transformation,[],[f250236]) ).
fof(f429123,plain,
! [X0] : v133779(X0,bitIndex1),
inference(cnf_transformation,[],[f134685]) ).
fof(f429124,plain,
! [X0] :
( v133786(X0,bitIndex5)
| ~ v133780(X0) ),
inference(cnf_transformation,[],[f250238]) ).
fof(f429145,plain,
! [X0] : ~ v133786(X0,bitIndex5),
inference(cnf_transformation,[],[f633]) ).
fof(f826135,plain,
v133774(sK27356),
inference(unit_resulting_resolution,[],[f429113,f429112]) ).
fof(f826136,plain,
~ v133775(sK27356),
inference(unit_resulting_resolution,[],[f429114,f826135]) ).
fof(f850625,plain,
! [X0] : v133789(X0),
inference(forward_subsumption_resolution,[],[f429116,f429123]) ).
fof(f851460,plain,
! [X0] : ~ v133780(X0),
inference(forward_subsumption_resolution,[],[f429124,f429145]) ).
fof(f851461,plain,
! [X0] : ~ v133779(X0,bitIndex0),
inference(unit_resulting_resolution,[],[f429121,f851460]) ).
fof(f851463,plain,
! [X0] : ~ v133778(X0),
inference(unit_resulting_resolution,[],[f429120,f851461]) ).
fof(f851464,plain,
! [X0] : v133777(X0),
inference(unit_resulting_resolution,[],[f429118,f851463]) ).
fof(f900845,plain,
! [X0] :
( v133775(X0)
| ~ v133789(X0) ),
inference(forward_subsumption_resolution,[],[f429115,f851464]) ).
fof(f900846,plain,
! [X0] : v133775(X0),
inference(forward_subsumption_resolution,[],[f900845,f850625]) ).
fof(f900851,plain,
$false,
inference(resolution,[],[f900846,f826136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV096+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.11 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.51 % Computer : n005.cluster.edu
% 0.17/0.51 % Model : x86_64 x86_64
% 0.17/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.51 % Memory : 8046.5625MB
% 0.17/0.51 % OS : Linux 6.8.0-71-generic
% 0.17/0.51 % CPULimit : 300
% 0.17/0.51 % WCLimit : 300
% 0.17/0.51 % DateTime : Sun Sep 27 11:30:03 UTC 2026
% 0.17/0.51 % CPUTime :
% 0.17/0.51 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.22/0.58 Running first-order model finding
% 0.22/0.58 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
% 25.45/6.89 % (3839836)Will run a generic schedule for satisfiability detection.
% 25.45/6.89 % (3839842)% WARNING: option uhcvi not known.
% 25.45/6.89 % (3839841)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1090602195_2969 on theBenchmark for (2969ds/0Mi)
% 25.45/6.89 % (3839844)dis+10_1_sil=32000:sp=arity:random_seed=527353310:i=103:fgj=on_2969 on theBenchmark for (2969ds/103Mi)
% 25.45/6.89 % (3839842)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=429224798:i=135531:add=off:rawr=on_2969 on theBenchmark for (2969ds/135531Mi)
% 25.45/6.89 % (3839843)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3014224956:i=88024:add=on:rawr=on_2969 on theBenchmark for (2969ds/88024Mi)
% 25.45/6.89 % (3839845)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1906096638:i=116_2969 on theBenchmark for (2969ds/116Mi)
% 25.45/6.89 % (3839847)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1449339917:i=131_2969 on theBenchmark for (2969ds/131Mi)
% 25.45/6.89 % (3839850)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3235644204:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2969 on theBenchmark for (2969ds/159Mi)
% 25.45/6.89 % (3839844)Instruction limit reached!
% 25.45/6.89 % (3839844)------------------------------
% 25.45/6.89 % (3839844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.45/6.89 % (3839844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/6.89 % (3839844)CaDiCaL version: 2.1.3
% 25.45/6.89 % (3839844)Termination reason: Instruction limit
% 25.45/6.89 % (3839844)Termination phase: Preprocessing 1
% 25.45/6.89 % (3839844)Time elapsed: 0.048 s
% 25.45/6.89 % (3839844)Peak memory usage: 193 MB
% 25.45/6.89 % (3839844)Instructions burned: 103 (million)
% 25.45/6.89 % (3839855)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=728503216:i=714:nm=2_2968 on theBenchmark for (2968ds/714Mi)
% 25.45/6.89 % (3839845)Instruction limit reached!
% 25.45/6.89 % (3839845)------------------------------
% 25.45/6.89 % (3839845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.45/6.89 % (3839845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/6.89 % (3839845)CaDiCaL version: 2.1.3
% 25.45/6.89 % (3839845)Termination reason: Instruction limit
% 25.45/6.89 % (3839845)Termination phase: Preprocessing 1
% 25.45/6.89 % (3839845)Time elapsed: 0.089 s
% 25.45/6.89 % (3839845)Peak memory usage: 192 MB
% 25.45/6.89 % (3839845)Instructions burned: 116 (million)
% 25.45/6.89 % (3839847)Instruction limit reached!
% 25.45/6.89 % (3839847)------------------------------
% 25.45/6.89 % (3839847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.45/6.89 % (3839847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/6.89 % (3839847)CaDiCaL version: 2.1.3
% 25.45/6.89 % (3839847)Termination reason: Instruction limit
% 25.45/6.89 % (3839847)Termination phase: Preprocessing 1
% 25.45/6.89 % (3839847)Time elapsed: 0.098 s
% 25.45/6.89 % (3839847)Peak memory usage: 193 MB
% 25.45/6.89 % (3839847)Instructions burned: 131 (million)
% 25.45/6.89 % (3839857)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2568266175:i=131:bd=preordered:fsd=on_2967 on theBenchmark for (2967ds/131Mi)
% 25.45/6.89 % (3839850)Instruction limit reached!
% 25.45/6.89 % (3839850)------------------------------
% 25.45/6.89 % (3839850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.45/6.89 % (3839850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.45/6.89 % (3839850)CaDiCaL version: 2.1.3
% 25.45/6.89 % (3839850)Termination reason: Instruction limit
% 25.45/6.89 % (3839850)Termination phase: Preprocessing 1
% 25.45/6.89 % (3839850)Time elapsed: 0.120 s
% 25.45/6.89 % (3839850)Peak memory usage: 194 MB
% 25.45/6.89 % (3839850)Instructions burned: 160 (million)
% 25.45/6.89 % (3839858)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=246309407:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2967 on theBenchmark for (2967ds/684Mi)
% 25.45/6.89 % (3839861)ott-21_1_sil=16000:fs=off:random_seed=3664538777:i=180:av=off:fsr=off_2967 on theBenchmark for (2967ds/180Mi)
% 25.45/6.89 % (3839857)Instruction limit reached!
% 25.45/6.89 % (3839857)------------------------------
% 25.45/6.89 % (3839857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 25.45/6.89 % (3839857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839857)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839857)Termination reason: Instruction limit
% 57.42/11.35 % (3839857)Termination phase: Preprocessing 1
% 57.42/11.35 % (3839857)Time elapsed: 0.096 s
% 57.42/11.35 % (3839857)Peak memory usage: 193 MB
% 57.42/11.35 % (3839857)Instructions burned: 131 (million)
% 57.42/11.35 % (3839863)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3448493432:i=477:bd=all_2966 on theBenchmark for (2966ds/477Mi)
% 57.42/11.35 % (3839861)Instruction limit reached!
% 57.42/11.35 % (3839861)------------------------------
% 57.42/11.35 % (3839861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839861)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839861)Termination reason: Instruction limit
% 57.42/11.35 % (3839861)Termination phase: Preprocessing 1
% 57.42/11.35 % (3839861)Time elapsed: 0.134 s
% 57.42/11.35 % (3839861)Peak memory usage: 195 MB
% 57.42/11.35 % (3839861)Instructions burned: 182 (million)
% 57.42/11.35 % (3839865)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2045460265:fmbsr=1.3:i=865:ins=25_2965 on theBenchmark for (2965ds/865Mi)
% 57.42/11.35 % (3839858)Instruction limit reached!
% 57.42/11.35 % (3839858)------------------------------
% 57.42/11.35 % (3839858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839858)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839858)Termination reason: Instruction limit
% 57.42/11.35 % (3839858)Termination phase: SInE selection
% 57.42/11.35 % (3839858)Time elapsed: 0.220 s
% 57.42/11.35 % (3839858)Peak memory usage: 192 MB
% 57.42/11.35 % (3839858)Instructions burned: 684 (million)
% 57.42/11.35 % (3839867)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=83613512:i=1179_2965 on theBenchmark for (2965ds/1179Mi)
% 57.42/11.35 % (3839855)Instruction limit reached!
% 57.42/11.35 % (3839855)------------------------------
% 57.42/11.35 % (3839855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839855)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839855)Termination reason: Instruction limit
% 57.42/11.35 % (3839855)Termination phase: Unused predicate definition removal
% 57.42/11.35 % (3839855)Time elapsed: 0.349 s
% 57.42/11.35 % (3839855)Peak memory usage: 259 MB
% 57.42/11.35 % (3839855)Instructions burned: 716 (million)
% 57.42/11.35 % (3839869)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1581695555:i=889:ins=1_2964 on theBenchmark for (2964ds/889Mi)
% 57.42/11.35 % (3839863)Instruction limit reached!
% 57.42/11.35 % (3839863)------------------------------
% 57.42/11.35 % (3839863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839863)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839863)Termination reason: Instruction limit
% 57.42/11.35 % (3839863)Termination phase: Preprocessing 1
% 57.42/11.35 % (3839863)Time elapsed: 0.356 s
% 57.42/11.35 % (3839863)Peak memory usage: 205 MB
% 57.42/11.35 % (3839863)Instructions burned: 477 (million)
% 57.42/11.35 % (3839871)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=1756360547:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2962 on theBenchmark for (2962ds/692Mi)
% 57.42/11.35 % (3839869)Instruction limit reached!
% 57.42/11.35 % (3839869)------------------------------
% 57.42/11.35 % (3839869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839869)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839869)Termination reason: Instruction limit
% 57.42/11.35 % (3839869)Termination phase: Preprocessing 2
% 57.42/11.35 % (3839869)Time elapsed: 0.426 s
% 57.42/11.35 % (3839869)Peak memory usage: 259 MB
% 57.42/11.35 % (3839869)Instructions burned: 892 (million)
% 57.42/11.35 % (3839871)Instruction limit reached!
% 57.42/11.35 % (3839871)------------------------------
% 57.42/11.35 % (3839871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.42/11.35 % (3839871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.42/11.35 % (3839871)CaDiCaL version: 2.1.3
% 57.42/11.35 % (3839871)Termination reason: Instruction limit
% 57.42/11.35 % (3839871)Termination phase: SInE selection
% 138.98/22.83 % (3839871)Time elapsed: 0.222 s
% 138.98/22.83 % (3839871)Peak memory usage: 192 MB
% 138.98/22.83 % (3839871)Instructions burned: 694 (million)
% 138.98/22.83 % (3839873)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=617017224:i=879:kws=inv_precedence:fsr=off_2960 on theBenchmark for (2960ds/879Mi)
% 138.98/22.83 % (3839874)fmb+10_1_sil=64000:random_seed=617319408:i=22061:nm=2:gsp=on_2960 on theBenchmark for (2960ds/22061Mi)
% 138.98/22.83 % (3839865)Instruction limit reached!
% 138.98/22.83 % (3839865)------------------------------
% 138.98/22.83 % (3839865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839865)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839865)Termination reason: Instruction limit
% 138.98/22.83 % (3839865)Termination phase: Naming
% 138.98/22.83 % (3839865)Time elapsed: 0.588 s
% 138.98/22.83 % (3839865)Peak memory usage: 228 MB
% 138.98/22.83 % (3839865)Instructions burned: 865 (million)
% 138.98/22.83 % (3839877)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2534190902:i=9515:nm=5_2959 on theBenchmark for (2959ds/9515Mi)
% 138.98/22.83 % (3839867)Instruction limit reached!
% 138.98/22.83 % (3839867)------------------------------
% 138.98/22.83 % (3839867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839867)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839867)Termination reason: Instruction limit
% 138.98/22.83 % (3839867)Termination phase: Naming
% 138.98/22.83 % (3839867)Time elapsed: 0.842 s
% 138.98/22.83 % (3839867)Peak memory usage: 259 MB
% 138.98/22.83 % (3839867)Instructions burned: 1179 (million)
% 138.98/22.83 % (3839879)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1772764676:fmbsr=1.7:i=920_2956 on theBenchmark for (2956ds/920Mi)
% 138.98/22.83 % (3839873)Instruction limit reached!
% 138.98/22.83 % (3839873)------------------------------
% 138.98/22.83 % (3839873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839873)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839873)Termination reason: Instruction limit
% 138.98/22.83 % (3839873)Termination phase: NewCNF
% 138.98/22.83 % (3839873)Time elapsed: 0.402 s
% 138.98/22.83 % (3839873)Peak memory usage: 244 MB
% 138.98/22.83 % (3839873)Instructions burned: 886 (million)
% 138.98/22.83 % (3839881)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=506554910:i=5131_2955 on theBenchmark for (2955ds/5131Mi)
% 138.98/22.83 % (3839879)Instruction limit reached!
% 138.98/22.83 % (3839879)------------------------------
% 138.98/22.83 % (3839879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839879)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839879)Termination reason: Instruction limit
% 138.98/22.83 % (3839879)Termination phase: Preprocessing 2
% 138.98/22.83 % (3839879)Time elapsed: 0.679 s
% 138.98/22.83 % (3839879)Peak memory usage: 259 MB
% 138.98/22.83 % (3839879)Instructions burned: 921 (million)
% 138.98/22.83 % (3839883)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3708567622:i=1472:ins=7:fdi=8:gsp=on_2949 on theBenchmark for (2949ds/1472Mi)
% 138.98/22.83 % (3839883)Instruction limit reached!
% 138.98/22.83 % (3839883)------------------------------
% 138.98/22.83 % (3839883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839883)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839883)Termination reason: Instruction limit
% 138.98/22.83 % (3839883)Termination phase: Naming
% 138.98/22.83 % (3839883)Time elapsed: 0.993 s
% 138.98/22.83 % (3839883)Peak memory usage: 277 MB
% 138.98/22.83 % (3839883)Instructions burned: 1474 (million)
% 138.98/22.83 % (3839885)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2886566816:i=6324_2938 on theBenchmark for (2938ds/6324Mi)
% 138.98/22.83 % (3839881)Instruction limit reached!
% 138.98/22.83 % (3839881)------------------------------
% 138.98/22.83 % (3839881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.98/22.83 % (3839881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.98/22.83 % (3839881)CaDiCaL version: 2.1.3
% 138.98/22.83 % (3839881)Termination reason: Instruction limit
% 138.98/22.83 % (3839881)Termination phase: Property scanning
% 108.05/27.22 % (3839881)Time elapsed: 1.849 s
% 108.05/27.22 % (3839881)Peak memory usage: 415 MB
% 108.05/27.22 % (3839881)Instructions burned: 5136 (million)
% 108.05/27.22 % (3839887)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1736165194:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 108.05/27.22 % (3839887)Instruction limit reached!
% 108.05/27.22 % (3839887)------------------------------
% 108.05/27.22 % (3839887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839887)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839887)Termination reason: Instruction limit
% 108.05/27.22 % (3839887)Termination phase: Preprocessing 3
% 108.05/27.22 % (3839887)Time elapsed: 0.822 s
% 108.05/27.22 % (3839887)Peak memory usage: 303 MB
% 108.05/27.22 % (3839887)Instructions burned: 2177 (million)
% 108.05/27.22 % (3839889)ott-2_1_sil=16000:newcnf=on:random_seed=4225535994:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2928 on theBenchmark for (2928ds/869Mi)
% 108.05/27.22 % (3839889)Instruction limit reached!
% 108.05/27.22 % (3839889)------------------------------
% 108.05/27.22 % (3839889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839889)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839889)Termination reason: Instruction limit
% 108.05/27.22 % (3839889)Termination phase: NewCNF
% 108.05/27.22 % (3839889)Time elapsed: 0.394 s
% 108.05/27.22 % (3839889)Peak memory usage: 244 MB
% 108.05/27.22 % (3839889)Instructions burned: 872 (million)
% 108.05/27.22 % (3839891)ott+10_1_sil=32000:tgt=ground:random_seed=1603088165:i=5114:av=off_2923 on theBenchmark for (2923ds/5114Mi)
% 108.05/27.22 % (3839877)Instruction limit reached!
% 108.05/27.22 % (3839877)------------------------------
% 108.05/27.22 % (3839877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839877)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839877)Termination reason: Instruction limit
% 108.05/27.22 % (3839877)Termination phase: Finite model building preprocessing
% 108.05/27.22 % (3839877)Time elapsed: 4.989 s
% 108.05/27.22 % (3839877)Peak memory usage: 481 MB
% 108.05/27.22 % (3839877)Instructions burned: 9516 (million)
% 108.05/27.22 % (3839893)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1336094372:i=54282_2908 on theBenchmark for (2908ds/54282Mi)
% 108.05/27.22 % (3839891)Instruction limit reached!
% 108.05/27.22 % (3839891)------------------------------
% 108.05/27.22 % (3839891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839891)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839891)Termination reason: Instruction limit
% 108.05/27.22 % (3839891)Termination phase: Property scanning
% 108.05/27.22 % (3839891)Time elapsed: 1.794 s
% 108.05/27.22 % (3839891)Peak memory usage: 447 MB
% 108.05/27.22 % (3839891)Instructions burned: 5118 (million)
% 108.05/27.22 % (3839895)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2634367196:i=3512:aac=none_2905 on theBenchmark for (2905ds/3512Mi)
% 108.05/27.22 % (3839885)Instruction limit reached!
% 108.05/27.22 % (3839885)------------------------------
% 108.05/27.22 % (3839885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839885)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839885)Termination reason: Instruction limit
% 108.05/27.22 % (3839885)Termination phase: Blocked clause elimination
% 108.05/27.22 % (3839885)Time elapsed: 3.930 s
% 108.05/27.22 % (3839885)Peak memory usage: 532 MB
% 108.05/27.22 % (3839885)Instructions burned: 6326 (million)
% 108.05/27.22 % (3839897)dis+21_1_sil=32000:sas=cadical:random_seed=2233233942:i=3773:amm=off_2898 on theBenchmark for (2898ds/3773Mi)
% 108.05/27.22 % (3839895)Instruction limit reached!
% 108.05/27.22 % (3839895)------------------------------
% 108.05/27.22 % (3839895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 108.05/27.22 % (3839895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 108.05/27.22 % (3839895)CaDiCaL version: 2.1.3
% 108.05/27.22 % (3839895)Termination reason: Instruction limit
% 108.05/27.22 % (3839895)Termination phase: Clausification
% 108.05/27.22 % (3839895)Time elapsed: 1.288 s
% 108.05/27.22 % (3839895)Peak memory usage: 416 MB
% 108.05/27.22 % (3839895)Instructions burned: 3514 (million)
% 169.16/27.45 % (3839899)ott+11_1_sil=16000:gs=on:random_seed=2384766442:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2892 on theBenchmark for (2892ds/2251Mi)
% 169.16/27.45 % (3839899)Instruction limit reached!
% 169.16/27.45 % (3839899)------------------------------
% 169.16/27.45 % (3839899)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839899)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839899)Termination reason: Instruction limit
% 169.16/27.45 % (3839899)Termination phase: SInE selection
% 169.16/27.45 % (3839899)Time elapsed: 0.371 s
% 169.16/27.45 % (3839899)Peak memory usage: 198 MB
% 169.16/27.45 % (3839899)Instructions burned: 2258 (million)
% 169.16/27.45 % (3839901)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4204488528:fmbsr=1.6:i=67534_2888 on theBenchmark for (2888ds/67534Mi)
% 169.16/27.45 % (3839897)Instruction limit reached!
% 169.16/27.45 % (3839897)------------------------------
% 169.16/27.45 % (3839897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839897)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839897)Termination reason: Instruction limit
% 169.16/27.45 % (3839897)Termination phase: Property scanning
% 169.16/27.45 % (3839897)Time elapsed: 2.492 s
% 169.16/27.45 % (3839897)Peak memory usage: 446 MB
% 169.16/27.45 % (3839897)Instructions burned: 3775 (million)
% 169.16/27.45 % (3839903)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3866227655:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2872 on theBenchmark for (2872ds/4591Mi)
% 169.16/27.45 % (3839874)Instruction limit reached!
% 169.16/27.45 % (3839874)------------------------------
% 169.16/27.45 % (3839874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839874)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839874)Termination reason: Instruction limit
% 169.16/27.45 % (3839874)Termination phase: Finite model building preprocessing
% 169.16/27.45 % (3839874)Time elapsed: 10.602 s
% 169.16/27.45 % (3839874)Peak memory usage: 642 MB
% 169.16/27.45 % (3839874)Instructions burned: 22062 (million)
% 169.16/27.45 % (3839905)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3469704739:i=29340_2852 on theBenchmark for (2852ds/29340Mi)
% 169.16/27.45 % (3839903)Instruction limit reached!
% 169.16/27.45 % (3839903)------------------------------
% 169.16/27.45 % (3839903)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839903)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839903)Termination reason: Instruction limit
% 169.16/27.45 % (3839903)Termination phase: Property scanning
% 169.16/27.45 % (3839903)Time elapsed: 2.821 s
% 169.16/27.45 % (3839903)Peak memory usage: 446 MB
% 169.16/27.45 % (3839903)Instructions burned: 4592 (million)
% 169.16/27.45 % (3839908)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1719396307:i=5211_2843 on theBenchmark for (2843ds/5211Mi)
% 169.16/27.45 % (3839908)Instruction limit reached!
% 169.16/27.45 % (3839908)------------------------------
% 169.16/27.45 % (3839908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839908)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839908)Termination reason: Instruction limit
% 169.16/27.45 % (3839908)Termination phase: Property scanning
% 169.16/27.45 % (3839908)Time elapsed: 3.147 s
% 169.16/27.45 % (3839908)Peak memory usage: 447 MB
% 169.16/27.45 % (3839908)Instructions burned: 5214 (million)
% 169.16/27.45 % (3839910)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2190404202:i=5497:nm=2_2811 on theBenchmark for (2811ds/5497Mi)
% 169.16/27.45 % Detected minimum model sizes of [1]
% 169.16/27.45 % Detected maximum model sizes of [2319]
% 169.16/27.45 % TRYING [7]
% 169.16/27.45 % (3839910)Instruction limit reached!
% 169.16/27.45 % (3839910)------------------------------
% 169.16/27.45 % (3839910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839910)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839910)Termination reason: Instruction limit
% 169.16/27.45 % (3839910)Termination phase: Property scanning
% 169.16/27.45 % (3839910)Time elapsed: 3.332 s
% 169.16/27.45 % (3839910)Peak memory usage: 457 MB
% 169.16/27.45 % (3839910)Instructions burned: 5499 (million)
% 169.16/27.45 % (3839912)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3291809192:fmbsr=2:i=46332_2777 on theBenchmark for (2777ds/46332Mi)
% 169.16/27.45 % (3839905) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3839836-3839905"...
% 169.16/27.45 % (3839905)...printing done.
% 169.16/27.45 % (3839905)Refutation found. Thanks to Tanya!
% 169.16/27.45 % SZS status Theorem for theBenchmark
% 169.16/27.45 % SZS output start Proof for theBenchmark
% See solution above
% 169.16/27.45 % (3839905)------------------------------
% 169.16/27.45 % (3839905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 169.16/27.45 % (3839905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.16/27.45 % (3839905)CaDiCaL version: 2.1.3
% 169.16/27.45 % (3839905)Termination reason: Refutation
% 169.16/27.45 % (3839905)Time elapsed: 11.220 s
% 169.16/27.45 % (3839905)Peak memory usage: 623 MB
% 169.16/27.45 % (3839905)Instructions burned: 18071 (million)
% 169.16/27.45 % (3839836)Success in time 26.629 s
% 169.16/27.45 % Vampire exiting
%------------------------------------------------------------------------------