%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV094+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:21:14 AM UTC 2026
% Result : Theorem 178.33s 28.65s
% Output : Refutation 178.33s
% 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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11138) ).
fof(f618,axiom,
! [X0] :
( ~ v133774(X0)
<=> v133775(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11137) ).
fof(f619,axiom,
! [X0] :
( v133775(X0)
<=> ( v133777(X0)
& v133789(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_26827) ).
fof(f620,axiom,
! [X0] :
( v133789(X0)
<=> ( v133779(X0,bitIndex0)
| v133779(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3137) ).
fof(f621,axiom,
! [X0] :
( ~ v133777(X0)
<=> v133778(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11136) ).
fof(f622,axiom,
! [X0] :
( v133778(X0)
<=> ( v133779(X0,bitIndex0)
& v133779(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3136) ).
fof(f623,axiom,
! [X0] :
( v133779(X0,bitIndex0)
<=> v133780(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_43639) ).
fof(f624,axiom,
! [X0] :
( v133779(X0,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_43638) ).
fof(f625,axiom,
! [X0] :
( v133780(X0)
<=> ( v133782(X0)
& v133786(X0,bitIndex5) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_3135) ).
fof(f633,axiom,
! [X0] : ~ v133786(X0,bitIndex5),
file('/export/starexec/sandbox2/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(f850624,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(f900898,plain,
! [X0] :
( v133775(X0)
| ~ v133789(X0) ),
inference(forward_subsumption_resolution,[],[f429115,f851464]) ).
fof(f900899,plain,
! [X0] : v133775(X0),
inference(forward_subsumption_resolution,[],[f900898,f850624]) ).
fof(f900904,plain,
$false,
inference(resolution,[],[f900899,f826136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV094+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.11 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.18/0.43 % Computer : n004.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 11:29:39 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.22/0.52 Running first-order model finding
% 0.22/0.52 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
% 38.78/8.66 % (3364559)Will run a generic schedule for satisfiability detection.
% 38.78/8.66 % (3364570)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1109641346_2969 on theBenchmark for (2969ds/0Mi)
% 38.78/8.66 % (3364571)% WARNING: option uhcvi not known.
% 38.78/8.66 % (3364571)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2844776054:i=135531:add=off:rawr=on_2969 on theBenchmark for (2969ds/135531Mi)
% 38.78/8.66 % (3364572)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3168646773:i=88024:add=on:rawr=on_2969 on theBenchmark for (2969ds/88024Mi)
% 38.78/8.66 % (3364574)dis+10_1_sil=32000:sp=arity:random_seed=1686528071:i=103:fgj=on_2969 on theBenchmark for (2969ds/103Mi)
% 38.78/8.66 % (3364575)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3183498311:i=116_2969 on theBenchmark for (2969ds/116Mi)
% 38.78/8.66 % (3364576)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=375040821:i=131_2969 on theBenchmark for (2969ds/131Mi)
% 38.78/8.66 % (3364578)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4081455717:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2969 on theBenchmark for (2969ds/159Mi)
% 38.78/8.66 % (3364574)Instruction limit reached!
% 38.78/8.66 % (3364574)------------------------------
% 38.78/8.66 % (3364574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/8.66 % (3364574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/8.66 % (3364574)CaDiCaL version: 2.1.3
% 38.78/8.66 % (3364574)Termination reason: Instruction limit
% 38.78/8.66 % (3364574)Termination phase: Preprocessing 1
% 38.78/8.66 % (3364574)Time elapsed: 0.077 s
% 38.78/8.66 % (3364574)Peak memory usage: 193 MB
% 38.78/8.66 % (3364574)Instructions burned: 104 (million)
% 38.78/8.66 % (3364575)Instruction limit reached!
% 38.78/8.66 % (3364575)------------------------------
% 38.78/8.66 % (3364575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/8.66 % (3364575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/8.66 % (3364575)CaDiCaL version: 2.1.3
% 38.78/8.66 % (3364575)Termination reason: Instruction limit
% 38.78/8.66 % (3364575)Termination phase: Preprocessing 1
% 38.78/8.66 % (3364575)Time elapsed: 0.085 s
% 38.78/8.66 % (3364575)Peak memory usage: 192 MB
% 38.78/8.66 % (3364575)Instructions burned: 116 (million)
% 38.78/8.66 % (3364576)Instruction limit reached!
% 38.78/8.66 % (3364576)------------------------------
% 38.78/8.66 % (3364576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/8.66 % (3364576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/8.66 % (3364576)CaDiCaL version: 2.1.3
% 38.78/8.66 % (3364576)Termination reason: Instruction limit
% 38.78/8.66 % (3364576)Termination phase: Preprocessing 1
% 38.78/8.66 % (3364576)Time elapsed: 0.097 s
% 38.78/8.66 % (3364576)Peak memory usage: 193 MB
% 38.78/8.66 % (3364576)Instructions burned: 131 (million)
% 38.78/8.66 % (3364584)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3748357372:i=714:nm=2_2968 on theBenchmark for (2968ds/714Mi)
% 38.78/8.66 % (3364585)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=115681872:i=131:bd=preordered:fsd=on_2968 on theBenchmark for (2968ds/131Mi)
% 38.78/8.66 % (3364578)Instruction limit reached!
% 38.78/8.66 % (3364578)------------------------------
% 38.78/8.66 % (3364578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/8.66 % (3364578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/8.66 % (3364578)CaDiCaL version: 2.1.3
% 38.78/8.66 % (3364578)Termination reason: Instruction limit
% 38.78/8.66 % (3364578)Termination phase: Preprocessing 1
% 38.78/8.66 % (3364578)Time elapsed: 0.113 s
% 38.78/8.66 % (3364578)Peak memory usage: 194 MB
% 38.78/8.66 % (3364578)Instructions burned: 159 (million)
% 38.78/8.66 % (3364587)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=3401689543:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2967 on theBenchmark for (2967ds/684Mi)
% 38.78/8.66 % (3364590)ott-21_1_sil=16000:fs=off:random_seed=3070899556:i=180:av=off:fsr=off_2967 on theBenchmark for (2967ds/180Mi)
% 38.78/8.66 % (3364585)Instruction limit reached!
% 38.78/8.66 % (3364585)------------------------------
% 38.78/8.66 % (3364585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.78/8.66 % (3364585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364585)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364585)Termination reason: Instruction limit
% 79.97/14.43 % (3364585)Termination phase: Preprocessing 1
% 79.97/14.43 % (3364585)Time elapsed: 0.094 s
% 79.97/14.43 % (3364585)Peak memory usage: 193 MB
% 79.97/14.43 % (3364585)Instructions burned: 132 (million)
% 79.97/14.43 % (3364592)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2299735028:i=477:bd=all_2966 on theBenchmark for (2966ds/477Mi)
% 79.97/14.43 % (3364590)Instruction limit reached!
% 79.97/14.43 % (3364590)------------------------------
% 79.97/14.43 % (3364590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364590)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364590)Termination reason: Instruction limit
% 79.97/14.43 % (3364590)Termination phase: Preprocessing 1
% 79.97/14.43 % (3364590)Time elapsed: 0.129 s
% 79.97/14.43 % (3364590)Peak memory usage: 195 MB
% 79.97/14.43 % (3364590)Instructions burned: 181 (million)
% 79.97/14.43 % (3364594)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3599320700:fmbsr=1.3:i=865:ins=25_2966 on theBenchmark for (2966ds/865Mi)
% 79.97/14.43 % (3364587)Instruction limit reached!
% 79.97/14.43 % (3364587)------------------------------
% 79.97/14.43 % (3364587)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364587)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364587)Termination reason: Instruction limit
% 79.97/14.43 % (3364587)Termination phase: SInE selection
% 79.97/14.43 % (3364587)Time elapsed: 0.243 s
% 79.97/14.43 % (3364587)Peak memory usage: 192 MB
% 79.97/14.43 % (3364587)Instructions burned: 687 (million)
% 79.97/14.43 % (3364596)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=204270885:i=1179_2965 on theBenchmark for (2965ds/1179Mi)
% 79.97/14.43 % (3364592)Instruction limit reached!
% 79.97/14.43 % (3364592)------------------------------
% 79.97/14.43 % (3364592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364592)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364592)Termination reason: Instruction limit
% 79.97/14.43 % (3364592)Termination phase: Preprocessing 1
% 79.97/14.43 % (3364592)Time elapsed: 0.347 s
% 79.97/14.43 % (3364592)Peak memory usage: 205 MB
% 79.97/14.43 % (3364592)Instructions burned: 478 (million)
% 79.97/14.43 % (3364598)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2133299046:i=889:ins=1_2962 on theBenchmark for (2962ds/889Mi)
% 79.97/14.43 % (3364584)Instruction limit reached!
% 79.97/14.43 % (3364584)------------------------------
% 79.97/14.43 % (3364584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364584)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364584)Termination reason: Instruction limit
% 79.97/14.43 % (3364584)Termination phase: Unused predicate definition removal
% 79.97/14.43 % (3364584)Time elapsed: 0.567 s
% 79.97/14.43 % (3364584)Peak memory usage: 259 MB
% 79.97/14.43 % (3364584)Instructions burned: 715 (million)
% 79.97/14.43 % (3364600)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=4265229850: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)
% 79.97/14.43 % (3364594)Instruction limit reached!
% 79.97/14.43 % (3364594)------------------------------
% 79.97/14.43 % (3364594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364594)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364594)Termination reason: Instruction limit
% 79.97/14.43 % (3364594)Termination phase: Naming
% 79.97/14.43 % (3364594)Time elapsed: 0.575 s
% 79.97/14.43 % (3364594)Peak memory usage: 228 MB
% 79.97/14.43 % (3364594)Instructions burned: 867 (million)
% 79.97/14.43 % (3364600)Instruction limit reached!
% 79.97/14.43 % (3364600)------------------------------
% 79.97/14.43 % (3364600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.97/14.43 % (3364600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.97/14.43 % (3364600)CaDiCaL version: 2.1.3
% 79.97/14.43 % (3364600)Termination reason: Instruction limit
% 79.97/14.43 % (3364600)Termination phase: SInE selection
% 156.60/25.29 % (3364600)Time elapsed: 0.220 s
% 156.60/25.29 % (3364600)Peak memory usage: 192 MB
% 156.60/25.29 % (3364600)Instructions burned: 695 (million)
% 156.60/25.29 % (3364602)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=224944996:i=879:kws=inv_precedence:fsr=off_2959 on theBenchmark for (2959ds/879Mi)
% 156.60/25.29 % (3364604)fmb+10_1_sil=64000:random_seed=848947393:i=22061:nm=2:gsp=on_2959 on theBenchmark for (2959ds/22061Mi)
% 156.60/25.29 % (3364596)Instruction limit reached!
% 156.60/25.29 % (3364596)------------------------------
% 156.60/25.29 % (3364596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364596)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364596)Termination reason: Instruction limit
% 156.60/25.29 % (3364596)Termination phase: Naming
% 156.60/25.29 % (3364596)Time elapsed: 0.805 s
% 156.60/25.29 % (3364596)Peak memory usage: 259 MB
% 156.60/25.29 % (3364596)Instructions burned: 1180 (million)
% 156.60/25.29 % (3364598)Instruction limit reached!
% 156.60/25.29 % (3364598)------------------------------
% 156.60/25.29 % (3364598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364598)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364598)Termination reason: Instruction limit
% 156.60/25.29 % (3364598)Termination phase: Preprocessing 2
% 156.60/25.29 % (3364598)Time elapsed: 0.645 s
% 156.60/25.29 % (3364598)Peak memory usage: 259 MB
% 156.60/25.29 % (3364598)Instructions burned: 890 (million)
% 156.60/25.29 % (3364606)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2995565265:i=9515:nm=5_2956 on theBenchmark for (2956ds/9515Mi)
% 156.60/25.29 % (3364608)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1646401866:fmbsr=1.7:i=920_2955 on theBenchmark for (2955ds/920Mi)
% 156.60/25.29 % (3364602)Instruction limit reached!
% 156.60/25.29 % (3364602)------------------------------
% 156.60/25.29 % (3364602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364602)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364602)Termination reason: Instruction limit
% 156.60/25.29 % (3364602)Termination phase: NewCNF
% 156.60/25.29 % (3364602)Time elapsed: 0.623 s
% 156.60/25.29 % (3364602)Peak memory usage: 243 MB
% 156.60/25.29 % (3364602)Instructions burned: 879 (million)
% 156.60/25.29 % (3364610)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2225542227:i=5131_2953 on theBenchmark for (2953ds/5131Mi)
% 156.60/25.29 % (3364608)Instruction limit reached!
% 156.60/25.29 % (3364608)------------------------------
% 156.60/25.29 % (3364608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364608)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364608)Termination reason: Instruction limit
% 156.60/25.29 % (3364608)Termination phase: Preprocessing 2
% 156.60/25.29 % (3364608)Time elapsed: 0.669 s
% 156.60/25.29 % (3364608)Peak memory usage: 259 MB
% 156.60/25.29 % (3364608)Instructions burned: 920 (million)
% 156.60/25.29 % (3364612)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=702233969:i=1472:ins=7:fdi=8:gsp=on_2948 on theBenchmark for (2948ds/1472Mi)
% 156.60/25.29 % (3364612)Instruction limit reached!
% 156.60/25.29 % (3364612)------------------------------
% 156.60/25.29 % (3364612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364612)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364612)Termination reason: Instruction limit
% 156.60/25.29 % (3364612)Termination phase: Naming
% 156.60/25.29 % (3364612)Time elapsed: 0.954 s
% 156.60/25.29 % (3364612)Peak memory usage: 277 MB
% 156.60/25.29 % (3364612)Instructions burned: 1472 (million)
% 156.60/25.29 % (3364614)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3844619542:i=6324_2938 on theBenchmark for (2938ds/6324Mi)
% 156.60/25.29 % (3364610)Instruction limit reached!
% 156.60/25.29 % (3364610)------------------------------
% 156.60/25.29 % (3364610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 156.60/25.29 % (3364610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.60/25.29 % (3364610)CaDiCaL version: 2.1.3
% 156.60/25.29 % (3364610)Termination reason: Instruction limit
% 156.60/25.29 % (3364610)Termination phase: Property scanning
% 127.96/28.46 % (3364610)Time elapsed: 3.429 s
% 127.96/28.46 % (3364610)Peak memory usage: 415 MB
% 127.96/28.46 % (3364610)Instructions burned: 5132 (million)
% 127.96/28.46 % (3364625)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=675935446:fmbsr=2.30978:i=2174_2918 on theBenchmark for (2918ds/2174Mi)
% 127.96/28.46 % (3364625)Instruction limit reached!
% 127.96/28.46 % (3364625)------------------------------
% 127.96/28.46 % (3364625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364625)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364625)Termination reason: Instruction limit
% 127.96/28.46 % (3364625)Termination phase: Preprocessing 3
% 127.96/28.46 % (3364625)Time elapsed: 2.150 s
% 127.96/28.46 % (3364625)Peak memory usage: 303 MB
% 127.96/28.46 % (3364625)Instructions burned: 2175 (million)
% 127.96/28.46 % (3364652)ott-2_1_sil=16000:newcnf=on:random_seed=1703682567:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2895 on theBenchmark for (2895ds/869Mi)
% 127.96/28.46 % (3364614)Instruction limit reached!
% 127.96/28.46 % (3364614)------------------------------
% 127.96/28.46 % (3364614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364614)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364614)Termination reason: Instruction limit
% 127.96/28.46 % (3364614)Termination phase: Blocked clause elimination
% 127.96/28.46 % (3364614)Time elapsed: 4.647 s
% 127.96/28.46 % (3364614)Peak memory usage: 532 MB
% 127.96/28.46 % (3364614)Instructions burned: 6324 (million)
% 127.96/28.46 % (3364655)ott+10_1_sil=32000:tgt=ground:random_seed=1498038544:i=5114:av=off_2891 on theBenchmark for (2891ds/5114Mi)
% 127.96/28.46 % (3364652)Instruction limit reached!
% 127.96/28.46 % (3364652)------------------------------
% 127.96/28.46 % (3364652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364652)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364652)Termination reason: Instruction limit
% 127.96/28.46 % (3364652)Termination phase: NewCNF
% 127.96/28.46 % (3364652)Time elapsed: 0.606 s
% 127.96/28.46 % (3364652)Peak memory usage: 244 MB
% 127.96/28.46 % (3364652)Instructions burned: 870 (million)
% 127.96/28.46 % (3364606)Instruction limit reached!
% 127.96/28.46 % (3364606)------------------------------
% 127.96/28.46 % (3364606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364606)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364606)Termination reason: Instruction limit
% 127.96/28.46 % (3364606)Termination phase: Finite model building preprocessing
% 127.96/28.46 % (3364606)Time elapsed: 6.708 s
% 127.96/28.46 % (3364606)Peak memory usage: 481 MB
% 127.96/28.46 % (3364606)Instructions burned: 9517 (million)
% 127.96/28.46 % (3364730)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3220412377:i=54282_2889 on theBenchmark for (2889ds/54282Mi)
% 127.96/28.46 % (3364755)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3774778190:i=3512:aac=none_2888 on theBenchmark for (2888ds/3512Mi)
% 127.96/28.46 % (3364755)Instruction limit reached!
% 127.96/28.46 % (3364755)------------------------------
% 127.96/28.46 % (3364755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364755)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364755)Termination reason: Instruction limit
% 127.96/28.46 % (3364755)Termination phase: Clausification
% 127.96/28.46 % (3364755)Time elapsed: 2.212 s
% 127.96/28.46 % (3364755)Peak memory usage: 416 MB
% 127.96/28.46 % (3364755)Instructions burned: 3513 (million)
% 127.96/28.46 % (3364813)dis+21_1_sil=32000:sas=cadical:random_seed=1140540873:i=3773:amm=off_2865 on theBenchmark for (2865ds/3773Mi)
% 127.96/28.46 % (3364655)Instruction limit reached!
% 127.96/28.46 % (3364655)------------------------------
% 127.96/28.46 % (3364655)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.96/28.46 % (3364655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.96/28.46 % (3364655)CaDiCaL version: 2.1.3
% 127.96/28.46 % (3364655)Termination reason: Instruction limit
% 127.96/28.46 % (3364655)Termination phase: Property scanning
% 127.96/28.46 % (3364655)Time elapsed: 3.022 s
% 127.96/28.46 % (3364655)Peak memory usage: 447 MB
% 127.96/28.46 % (3364655)Instructions burned: 5115 (million)
% 178.33/28.65 % (3364815)ott+11_1_sil=16000:gs=on:random_seed=1627229251:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2860 on theBenchmark for (2860ds/2251Mi)
% 178.33/28.65 % (3364815)Instruction limit reached!
% 178.33/28.65 % (3364815)------------------------------
% 178.33/28.65 % (3364815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364815)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364815)Termination reason: Instruction limit
% 178.33/28.65 % (3364815)Termination phase: SInE selection
% 178.33/28.65 % (3364815)Time elapsed: 0.683 s
% 178.33/28.65 % (3364815)Peak memory usage: 198 MB
% 178.33/28.65 % (3364815)Instructions burned: 2255 (million)
% 178.33/28.65 % (3364817)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3477588455:fmbsr=1.6:i=67534_2853 on theBenchmark for (2853ds/67534Mi)
% 178.33/28.65 % (3364604)Instruction limit reached!
% 178.33/28.65 % (3364604)------------------------------
% 178.33/28.65 % (3364604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364604)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364604)Termination reason: Instruction limit
% 178.33/28.65 % (3364604)Termination phase: Finite model building preprocessing
% 178.33/28.65 % (3364604)Time elapsed: 11.256 s
% 178.33/28.65 % (3364604)Peak memory usage: 642 MB
% 178.33/28.65 % (3364604)Instructions burned: 22062 (million)
% 178.33/28.65 % (3364819)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=627354169:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2845 on theBenchmark for (2845ds/4591Mi)
% 178.33/28.65 % (3364813)Instruction limit reached!
% 178.33/28.65 % (3364813)------------------------------
% 178.33/28.65 % (3364813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364813)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364813)Termination reason: Instruction limit
% 178.33/28.65 % (3364813)Termination phase: Property scanning
% 178.33/28.65 % (3364813)Time elapsed: 2.463 s
% 178.33/28.65 % (3364813)Peak memory usage: 447 MB
% 178.33/28.65 % (3364813)Instructions burned: 3774 (million)
% 178.33/28.65 % (3364821)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4155129923:i=29340_2840 on theBenchmark for (2840ds/29340Mi)
% 178.33/28.65 % (3364819)Instruction limit reached!
% 178.33/28.65 % (3364819)------------------------------
% 178.33/28.65 % (3364819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364819)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364819)Termination reason: Instruction limit
% 178.33/28.65 % (3364819)Termination phase: Property scanning
% 178.33/28.65 % (3364819)Time elapsed: 2.832 s
% 178.33/28.65 % (3364819)Peak memory usage: 446 MB
% 178.33/28.65 % (3364819)Instructions burned: 4593 (million)
% 178.33/28.65 % (3364823)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=4047444761:i=5211_2816 on theBenchmark for (2816ds/5211Mi)
% 178.33/28.65 % (3364823)Instruction limit reached!
% 178.33/28.65 % (3364823)------------------------------
% 178.33/28.65 % (3364823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364823)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364823)Termination reason: Instruction limit
% 178.33/28.65 % (3364823)Termination phase: Property scanning
% 178.33/28.65 % (3364823)Time elapsed: 3.081 s
% 178.33/28.65 % (3364823)Peak memory usage: 447 MB
% 178.33/28.65 % (3364823)Instructions burned: 5214 (million)
% 178.33/28.65 % (3364825)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4246197569:i=5497:nm=2_2785 on theBenchmark for (2785ds/5497Mi)
% 178.33/28.65 % Detected minimum model sizes of [1]
% 178.33/28.65 % Detected maximum model sizes of [2318]
% 178.33/28.65 % TRYING [1]
% 178.33/28.65 % TRYING [2]
% 178.33/28.65 % (3364825)Instruction limit reached!
% 178.33/28.65 % (3364825)------------------------------
% 178.33/28.65 % (3364825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364825)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364825)Termination reason: Instruction limit
% 178.33/28.65 % (3364825)Termination phase: Property scanning
% 178.33/28.65 % (3364825)Time elapsed: 3.257 s
% 178.33/28.65 % (3364825)Peak memory usage: 457 MB
% 178.33/28.65 % (3364825)Instructions burned: 5499 (million)
% 178.33/28.65 % TRYING [3]
% 178.33/28.65 % (3364827)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1191944225:fmbsr=2:i=46332_2751 on theBenchmark for (2751ds/46332Mi)
% 178.33/28.65 % (3364821) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3364559-3364821"...
% 178.33/28.65 % (3364821)...printing done.
% 178.33/28.65 % (3364821)Refutation found. Thanks to Tanya!
% 178.33/28.65 % SZS status Theorem for theBenchmark
% 178.33/28.65 % SZS output start Proof for theBenchmark
% See solution above
% 178.33/28.65 % (3364821)------------------------------
% 178.33/28.65 % (3364821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 178.33/28.65 % (3364821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.33/28.65 % (3364821)CaDiCaL version: 2.1.3
% 178.33/28.65 % (3364821)Termination reason: Refutation
% 178.33/28.65 % (3364821)Time elapsed: 11.252 s
% 178.33/28.65 % (3364821)Peak memory usage: 623 MB
% 178.33/28.65 % (3364821)Instructions burned: 18133 (million)
% 178.33/28.65 % (3364559)Success in time 27.936 s
% 178.33/28.65 % Vampire exiting
%------------------------------------------------------------------------------