%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HWV077+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 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 11:20:08 AM UTC 2026
% Result : Satisfiable 50.97s 7.79s
% Output : FiniteModel 50.97s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_true,type,
true: $i ).
tff(true_definition,axiom,
true = 'fmb_$i_1' ).
tff(declare_false,type,
false: $i ).
tff(false_definition,axiom,
false = 'fmb_$i_2' ).
tff(declare_p,type,
p: $i > $o ).
tff(predicate_p,axiom,
( p('fmb_$i_1')
& ~ p('fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV077+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n017.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 11:17:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 8.84/2.03 % (2390276)Will run a generic schedule for satisfiability detection.
% 8.84/2.03 % (2390283)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4228222615:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.84/2.03 % (2390282)% WARNING: option uhcvi not known.
% 8.84/2.03 % (2390281)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1736980429_2999 on theBenchmark for (2999ds/0Mi)
% 8.84/2.03 % (2390282)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2653847258:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.84/2.03 % (2390284)dis+10_1_sil=32000:sp=arity:random_seed=3379267231:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.84/2.03 % (2390287)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1727053476:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.84/2.03 % (2390285)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=244158504:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.84/2.03 % (2390286)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1310923304:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.84/2.03 % (2390284)Instruction limit reached!
% 8.84/2.03 % (2390284)------------------------------
% 8.84/2.03 % (2390284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.84/2.03 % (2390284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/2.03 % (2390284)CaDiCaL version: 2.1.3
% 8.84/2.03 % (2390284)Termination reason: Instruction limit
% 8.84/2.03 % (2390284)Termination phase: Saturation
% 8.84/2.03 % (2390284)Time elapsed: 0.057 s
% 8.84/2.03 % (2390284)Peak memory usage: 17 MB
% 8.84/2.03 % (2390284)Instructions burned: 104 (million)
% 8.84/2.03 % (2390285)Instruction limit reached!
% 8.84/2.03 % (2390285)------------------------------
% 8.84/2.03 % (2390285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.84/2.03 % (2390285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/2.03 % (2390285)CaDiCaL version: 2.1.3
% 8.84/2.03 % (2390285)Termination reason: Instruction limit
% 8.84/2.03 % (2390285)Termination phase: Blocked clause elimination
% 8.84/2.03 % (2390285)Time elapsed: 0.063 s
% 8.84/2.03 % (2390285)Peak memory usage: 16 MB
% 8.84/2.03 % (2390285)Instructions burned: 116 (million)
% 8.84/2.03 % (2390295)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1940875734:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.84/2.03 % (2390286)Instruction limit reached!
% 8.84/2.03 % (2390286)------------------------------
% 8.84/2.03 % (2390286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.84/2.03 % (2390286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/2.03 % (2390286)CaDiCaL version: 2.1.3
% 8.84/2.03 % (2390286)Termination reason: Instruction limit
% 8.84/2.03 % (2390286)Termination phase: Saturation
% 8.84/2.03 % (2390286)Time elapsed: 0.076 s
% 8.84/2.03 % (2390286)Peak memory usage: 18 MB
% 8.84/2.03 % (2390286)Instructions burned: 132 (million)
% 8.84/2.03 % (2390296)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3637341807:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.84/2.03 % (2390287)Instruction limit reached!
% 8.84/2.03 % (2390287)------------------------------
% 8.84/2.03 % (2390287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.84/2.03 % (2390287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.84/2.03 % (2390287)CaDiCaL version: 2.1.3
% 8.84/2.03 % (2390287)Termination reason: Instruction limit
% 8.84/2.03 % (2390287)Termination phase: Saturation
% 8.84/2.03 % (2390287)Time elapsed: 0.093 s
% 8.84/2.03 % (2390287)Peak memory usage: 20 MB
% 8.84/2.03 % (2390287)Instructions burned: 159 (million)
% 8.84/2.03 % (2390298)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=2199734568:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.84/2.03 % (2390300)ott-21_1_sil=16000:fs=off:random_seed=80343982:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 8.84/2.03 % (2390296)Instruction limit reached!
% 8.84/2.03 % (2390296)------------------------------
% 8.84/2.03 % (2390296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.84/2.03 % (2390296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390296)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390296)Termination reason: Instruction limit
% 34.81/5.44 % (2390296)Termination phase: Blocked clause elimination
% 34.81/5.44 % (2390296)Time elapsed: 0.069 s
% 34.81/5.44 % (2390296)Peak memory usage: 17 MB
% 34.81/5.44 % (2390296)Instructions burned: 132 (million)
% 34.81/5.44 % (2390303)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=593894276:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 34.81/5.44 % (2390300)Instruction limit reached!
% 34.81/5.44 % (2390300)------------------------------
% 34.81/5.44 % (2390300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.44 % (2390300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390300)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390300)Termination reason: Instruction limit
% 34.81/5.44 % (2390300)Termination phase: Saturation
% 34.81/5.44 % (2390300)Time elapsed: 0.093 s
% 34.81/5.44 % (2390300)Peak memory usage: 17 MB
% 34.81/5.44 % (2390300)Instructions burned: 180 (million)
% 34.81/5.44 % (2390305)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2204938841:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 34.81/5.44 % TRYING [1]
% 34.81/5.44 % TRYING [2]
% 34.81/5.44 % TRYING [1]
% 34.81/5.44 % (2390295)Instruction limit reached!
% 34.81/5.44 % (2390295)------------------------------
% 34.81/5.44 % (2390295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.44 % (2390295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390295)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390295)Termination reason: Instruction limit
% 34.81/5.44 % (2390295)Termination phase: Finite model building constraint generation
% 34.81/5.44 % (2390295)Time elapsed: 0.319 s
% 34.81/5.44 % (2390295)Peak memory usage: 24 MB
% 34.81/5.44 % (2390295)Instructions burned: 715 (million)
% 34.81/5.44 % (2390307)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=244853946:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 34.81/5.44 % (2390303)Instruction limit reached!
% 34.81/5.44 % (2390303)------------------------------
% 34.81/5.44 % (2390303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.44 % (2390303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390303)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390303)Termination reason: Instruction limit
% 34.81/5.44 % (2390303)Termination phase: Saturation
% 34.81/5.44 % (2390303)Time elapsed: 0.261 s
% 34.81/5.44 % (2390303)Peak memory usage: 20 MB
% 34.81/5.44 % (2390303)Instructions burned: 478 (million)
% 34.81/5.44 % (2390309)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=825481213:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 34.81/5.44 % (2390298)Instruction limit reached!
% 34.81/5.44 % (2390298)------------------------------
% 34.81/5.44 % (2390298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.44 % (2390298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390298)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390298)Termination reason: Instruction limit
% 34.81/5.44 % (2390298)Termination phase: Saturation
% 34.81/5.44 % (2390298)Time elapsed: 0.384 s
% 34.81/5.44 % (2390298)Peak memory usage: 28 MB
% 34.81/5.44 % (2390298)Instructions burned: 685 (million)
% 34.81/5.44 % (2390311)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=3387725566:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 34.81/5.44 % TRYING [1]
% 34.81/5.44 % (2390305)Instruction limit reached!
% 34.81/5.44 % (2390305)------------------------------
% 34.81/5.44 % (2390305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.44 % (2390305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.44 % (2390305)CaDiCaL version: 2.1.3
% 34.81/5.44 % (2390305)Termination reason: Instruction limit
% 34.81/5.44 % (2390305)Termination phase: Finite model building constraint generation
% 34.81/5.44 % (2390305)Time elapsed: 0.389 s
% 34.81/5.44 % (2390305)Peak memory usage: 37 MB
% 34.81/5.44 % (2390305)Instructions burned: 868 (million)
% 34.81/5.44 % (2390313)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1389464552:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 34.81/5.44 % (2390309)Cannot represent all propositional literals internally
% 34.81/5.44 % (2390309)Refutation not found, incomplete strategy
% 34.81/5.44 % (2390309)------------------------------
% 50.97/7.79 % (2390309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390309)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390309)Termination reason: Refutation not found, incomplete strategy
% 50.97/7.79 % (2390309)Time elapsed: 0.348 s
% 50.97/7.79 % (2390309)Peak memory usage: 26 MB
% 50.97/7.79 % (2390309)Instructions burned: 771 (million)
% 50.97/7.79 % (2390309)------------------------------
% 50.97/7.79 % (2390309)------------------------------
% 50.97/7.79 % (2390315)fmb+10_1_sil=64000:random_seed=2653909063:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 50.97/7.79 % (2390311)Instruction limit reached!
% 50.97/7.79 % (2390311)------------------------------
% 50.97/7.79 % (2390311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390311)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390311)Termination reason: Instruction limit
% 50.97/7.79 % (2390311)Termination phase: Saturation
% 50.97/7.79 % (2390311)Time elapsed: 0.420 s
% 50.97/7.79 % (2390311)Peak memory usage: 27 MB
% 50.97/7.79 % (2390311)Instructions burned: 692 (million)
% 50.97/7.79 % (2390317)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2911084686:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 50.97/7.79 % (2390313)Instruction limit reached!
% 50.97/7.79 % (2390313)------------------------------
% 50.97/7.79 % (2390313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390313)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390313)Termination reason: Instruction limit
% 50.97/7.79 % (2390313)Termination phase: Saturation
% 50.97/7.79 % (2390313)Time elapsed: 0.412 s
% 50.97/7.79 % (2390313)Peak memory usage: 25 MB
% 50.97/7.79 % (2390313)Instructions burned: 879 (million)
% 50.97/7.79 % (2390319)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2372651839:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 50.97/7.79 % (2390307)Instruction limit reached!
% 50.97/7.79 % (2390307)------------------------------
% 50.97/7.79 % (2390307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390307)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390307)Termination reason: Instruction limit
% 50.97/7.79 % (2390307)Termination phase: Saturation
% 50.97/7.79 % (2390307)Time elapsed: 0.706 s
% 50.97/7.79 % (2390307)Peak memory usage: 38 MB
% 50.97/7.79 % (2390307)Instructions burned: 1179 (million)
% 50.97/7.79 % (2390321)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3492826753:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 50.97/7.79 % TRYING [1]
% 50.97/7.79 % (2390317)Cannot represent all propositional literals internally
% 50.97/7.79 % (2390317)Refutation not found, incomplete strategy
% 50.97/7.79 % (2390317)------------------------------
% 50.97/7.79 % (2390317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390317)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390317)Termination reason: Refutation not found, incomplete strategy
% 50.97/7.79 % (2390317)Time elapsed: 0.330 s
% 50.97/7.79 % (2390317)Peak memory usage: 26 MB
% 50.97/7.79 % (2390317)Instructions burned: 736 (million)
% 50.97/7.79 % (2390317)------------------------------
% 50.97/7.79 % (2390317)------------------------------
% 50.97/7.79 % TRYING [2]
% 50.97/7.79 % (2390323)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2910995173:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 50.97/7.79 % TRYING [8]
% 50.97/7.79 % (2390319)Instruction limit reached!
% 50.97/7.79 % (2390319)------------------------------
% 50.97/7.79 % (2390319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390319)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390319)Termination reason: Instruction limit
% 50.97/7.79 % (2390319)Termination phase: Finite model building constraint generation
% 50.97/7.79 % (2390319)Time elapsed: 0.394 s
% 50.97/7.79 % (2390319)Peak memory usage: 37 MB
% 50.97/7.79 % (2390319)Instructions burned: 923 (million)
% 50.97/7.79 % (2390325)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1896615498:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 50.97/7.79 % (2390325)Cannot represent all propositional literals internally
% 50.97/7.79 % (2390325)Refutation not found, incomplete strategy
% 50.97/7.79 % (2390325)------------------------------
% 50.97/7.79 % (2390325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390325)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390325)Termination reason: Refutation not found, incomplete strategy
% 50.97/7.79 % (2390325)Time elapsed: 0.348 s
% 50.97/7.79 % (2390325)Peak memory usage: 27 MB
% 50.97/7.79 % (2390325)Instructions burned: 768 (million)
% 50.97/7.79 % (2390325)------------------------------
% 50.97/7.79 % (2390325)------------------------------
% 50.97/7.79 % (2390327)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=572857091:fmbsr=2.30978:i=2174_2980 on theBenchmark for (2980ds/2174Mi)
% 50.97/7.79 % (2390327)Cannot represent all propositional literals internally
% 50.97/7.79 % (2390327)Refutation not found, incomplete strategy
% 50.97/7.79 % (2390327)------------------------------
% 50.97/7.79 % (2390327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390327)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390327)Termination reason: Refutation not found, incomplete strategy
% 50.97/7.79 % (2390327)Time elapsed: 0.302 s
% 50.97/7.79 % (2390327)Peak memory usage: 23 MB
% 50.97/7.79 % (2390327)Instructions burned: 672 (million)
% 50.97/7.79 % (2390327)------------------------------
% 50.97/7.79 % (2390327)------------------------------
% 50.97/7.79 % (2390329)ott-2_1_sil=16000:newcnf=on:random_seed=3039622914:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi)
% 50.97/7.79 % (2390323)Instruction limit reached!
% 50.97/7.79 % (2390323)------------------------------
% 50.97/7.79 % (2390323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390323)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390323)Termination reason: Instruction limit
% 50.97/7.79 % (2390323)Termination phase: Saturation
% 50.97/7.79 % (2390323)Time elapsed: 0.910 s
% 50.97/7.79 % (2390323)Peak memory usage: 51 MB
% 50.97/7.79 % (2390323)Instructions burned: 1473 (million)
% 50.97/7.79 % (2390331)ott+10_1_sil=32000:tgt=ground:random_seed=1673509229:i=5114:av=off_2976 on theBenchmark for (2976ds/5114Mi)
% 50.97/7.79 % (2390329)Instruction limit reached!
% 50.97/7.79 % (2390329)------------------------------
% 50.97/7.79 % (2390329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390329)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390329)Termination reason: Instruction limit
% 50.97/7.79 % (2390329)Termination phase: Saturation
% 50.97/7.79 % (2390329)Time elapsed: 0.514 s
% 50.97/7.79 % (2390329)Peak memory usage: 31 MB
% 50.97/7.79 % (2390329)Instructions burned: 870 (million)
% 50.97/7.79 % (2390333)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1519502385:i=54282_2971 on theBenchmark for (2971ds/54282Mi)
% 50.97/7.79 % TRYING [1]
% 50.97/7.79 % TRYING [2]
% 50.97/7.79 % (2390321)Instruction limit reached!
% 50.97/7.79 % (2390321)------------------------------
% 50.97/7.79 % (2390321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390321)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390321)Termination reason: Instruction limit
% 50.97/7.79 % (2390321)Termination phase: Saturation
% 50.97/7.79 % (2390321)Time elapsed: 3.163 s
% 50.97/7.79 % (2390321)Peak memory usage: 56 MB
% 50.97/7.79 % (2390321)Instructions burned: 5132 (million)
% 50.97/7.79 % (2390335)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=692884224:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi)
% 50.97/7.79 % (2390331)Instruction limit reached!
% 50.97/7.79 % (2390331)------------------------------
% 50.97/7.79 % (2390331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390331)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390331)Termination reason: Instruction limit
% 50.97/7.79 % (2390331)Termination phase: Saturation
% 50.97/7.79 % (2390331)Time elapsed: 2.659 s
% 50.97/7.79 % (2390331)Peak memory usage: 48 MB
% 50.97/7.79 % (2390331)Instructions burned: 5114 (million)
% 50.97/7.79 % (2390337)dis+21_1_sil=32000:sas=cadical:random_seed=3750059599:i=3773:amm=off_2949 on theBenchmark for (2949ds/3773Mi)
% 50.97/7.79 % (2390335)Instruction limit reached!
% 50.97/7.79 % (2390335)------------------------------
% 50.97/7.79 % (2390335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390335)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390335)Termination reason: Instruction limit
% 50.97/7.79 % (2390335)Termination phase: Saturation
% 50.97/7.79 % (2390335)Time elapsed: 1.772 s
% 50.97/7.79 % (2390335)Peak memory usage: 125 MB
% 50.97/7.79 % (2390335)Instructions burned: 3513 (million)
% 50.97/7.79 % (2390339)ott+11_1_sil=16000:gs=on:random_seed=748081525:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 50.97/7.79 % (2390337)Instruction limit reached!
% 50.97/7.79 % (2390337)------------------------------
% 50.97/7.79 % (2390337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390337)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390337)Termination reason: Instruction limit
% 50.97/7.79 % (2390337)Termination phase: Saturation
% 50.97/7.79 % (2390337)Time elapsed: 2.017 s
% 50.97/7.79 % (2390337)Peak memory usage: 183 MB
% 50.97/7.79 % (2390337)Instructions burned: 3774 (million)
% 50.97/7.79 % (2390341)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1364892292:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi)
% 50.97/7.79 % Finite Model Found!
% 50.97/7.79 % SZS status Satisfiable for theBenchmark
% 50.97/7.79 % (2390281) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2390276-2390281"...
% 50.97/7.79 % (2390281)...printing done.
% 50.97/7.79 % SZS output start FiniteModel for theBenchmark
% See solution above
% 50.97/7.79 % (2390281)------------------------------
% 50.97/7.79 % (2390281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.97/7.79 % (2390281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/7.79 % (2390281)CaDiCaL version: 2.1.3
% 50.97/7.79 % (2390281)Termination reason: Satisfiable
% 50.97/7.79 % (2390281)Time elapsed: 7.203 s
% 50.97/7.79 % (2390281)Peak memory usage: 190 MB
% 50.97/7.79 % (2390281)Instructions burned: 14180 (million)
% 50.97/7.79 % (2390276)Success in time 7.367 s
% 50.97/7.79 % Vampire exiting
%------------------------------------------------------------------------------