%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LDA017-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 12:01:30 PM UTC 2026
% Result : Satisfiable 31.51s 12.03s
% Output : FiniteModel 31.51s
% 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('declare_$i3',type,
'fmb_$i_3': $i ).
tff('declare_$i4',type,
'fmb_$i_4': $i ).
tff('declare_$i5',type,
'fmb_$i_5': $i ).
tff('declare_$i6',type,
'fmb_$i_6': $i ).
tff('declare_$i7',type,
'fmb_$i_7': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' )
| ( X = 'fmb_$i_3' )
| ( X = 'fmb_$i_4' )
| ( X = 'fmb_$i_5' )
| ( X = 'fmb_$i_6' )
| ( X = 'fmb_$i_7' ) ) ).
tff('distinct_domain_$i',axiom,
( ( 'fmb_$i_1' != 'fmb_$i_2' )
& ( 'fmb_$i_1' != 'fmb_$i_3' )
& ( 'fmb_$i_1' != 'fmb_$i_4' )
& ( 'fmb_$i_1' != 'fmb_$i_5' )
& ( 'fmb_$i_1' != 'fmb_$i_6' )
& ( 'fmb_$i_1' != 'fmb_$i_7' )
& ( 'fmb_$i_2' != 'fmb_$i_3' )
& ( 'fmb_$i_2' != 'fmb_$i_4' )
& ( 'fmb_$i_2' != 'fmb_$i_5' )
& ( 'fmb_$i_2' != 'fmb_$i_6' )
& ( 'fmb_$i_2' != 'fmb_$i_7' )
& ( 'fmb_$i_3' != 'fmb_$i_4' )
& ( 'fmb_$i_3' != 'fmb_$i_5' )
& ( 'fmb_$i_3' != 'fmb_$i_6' )
& ( 'fmb_$i_3' != 'fmb_$i_7' )
& ( 'fmb_$i_4' != 'fmb_$i_5' )
& ( 'fmb_$i_4' != 'fmb_$i_6' )
& ( 'fmb_$i_4' != 'fmb_$i_7' )
& ( 'fmb_$i_5' != 'fmb_$i_6' )
& ( 'fmb_$i_5' != 'fmb_$i_7' )
& ( 'fmb_$i_6' != 'fmb_$i_7' ) ) ).
tff(declare_x0,type,
x0: $i ).
tff(x0_definition,axiom,
x0 = 'fmb_$i_1' ).
tff(declare_x1,type,
x1: $i ).
tff(x1_definition,axiom,
x1 = 'fmb_$i_2' ).
tff(declare_x2,type,
x2: $i ).
tff(x2_definition,axiom,
x2 = 'fmb_$i_3' ).
tff(declare_product,type,
product: ( $i * $i ) > $i ).
tff(function_product,axiom,
( ( product('fmb_$i_1','fmb_$i_1') = 'fmb_$i_1' )
& ( product('fmb_$i_1','fmb_$i_2') = 'fmb_$i_4' )
& ( product('fmb_$i_1','fmb_$i_3') = 'fmb_$i_5' )
& ( product('fmb_$i_1','fmb_$i_4') = 'fmb_$i_2' )
& ( product('fmb_$i_1','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_1','fmb_$i_6') = 'fmb_$i_5' )
& ( product('fmb_$i_1','fmb_$i_7') = 'fmb_$i_5' )
& ( product('fmb_$i_2','fmb_$i_1') = 'fmb_$i_4' )
& ( product('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' )
& ( product('fmb_$i_2','fmb_$i_3') = 'fmb_$i_7' )
& ( product('fmb_$i_2','fmb_$i_4') = 'fmb_$i_1' )
& ( product('fmb_$i_2','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_2','fmb_$i_6') = 'fmb_$i_5' )
& ( product('fmb_$i_2','fmb_$i_7') = 'fmb_$i_5' )
& ( product('fmb_$i_3','fmb_$i_1') = 'fmb_$i_1' )
& ( product('fmb_$i_3','fmb_$i_2') = 'fmb_$i_2' )
& ( product('fmb_$i_3','fmb_$i_3') = 'fmb_$i_3' )
& ( product('fmb_$i_3','fmb_$i_4') = 'fmb_$i_4' )
& ( product('fmb_$i_3','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_3','fmb_$i_6') = 'fmb_$i_6' )
& ( product('fmb_$i_3','fmb_$i_7') = 'fmb_$i_7' )
& ( product('fmb_$i_4','fmb_$i_1') = 'fmb_$i_2' )
& ( product('fmb_$i_4','fmb_$i_2') = 'fmb_$i_1' )
& ( product('fmb_$i_4','fmb_$i_3') = 'fmb_$i_6' )
& ( product('fmb_$i_4','fmb_$i_4') = 'fmb_$i_4' )
& ( product('fmb_$i_4','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_4','fmb_$i_6') = 'fmb_$i_7' )
& ( product('fmb_$i_4','fmb_$i_7') = 'fmb_$i_5' )
& ( product('fmb_$i_5','fmb_$i_1') = 'fmb_$i_1' )
& ( product('fmb_$i_5','fmb_$i_2') = 'fmb_$i_2' )
& ( product('fmb_$i_5','fmb_$i_3') = 'fmb_$i_3' )
& ( product('fmb_$i_5','fmb_$i_4') = 'fmb_$i_4' )
& ( product('fmb_$i_5','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_5','fmb_$i_6') = 'fmb_$i_6' )
& ( product('fmb_$i_5','fmb_$i_7') = 'fmb_$i_7' )
& ( product('fmb_$i_6','fmb_$i_1') = 'fmb_$i_1' )
& ( product('fmb_$i_6','fmb_$i_2') = 'fmb_$i_2' )
& ( product('fmb_$i_6','fmb_$i_3') = 'fmb_$i_3' )
& ( product('fmb_$i_6','fmb_$i_4') = 'fmb_$i_4' )
& ( product('fmb_$i_6','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_6','fmb_$i_6') = 'fmb_$i_6' )
& ( product('fmb_$i_6','fmb_$i_7') = 'fmb_$i_7' )
& ( product('fmb_$i_7','fmb_$i_1') = 'fmb_$i_1' )
& ( product('fmb_$i_7','fmb_$i_2') = 'fmb_$i_2' )
& ( product('fmb_$i_7','fmb_$i_3') = 'fmb_$i_3' )
& ( product('fmb_$i_7','fmb_$i_4') = 'fmb_$i_4' )
& ( product('fmb_$i_7','fmb_$i_5') = 'fmb_$i_5' )
& ( product('fmb_$i_7','fmb_$i_6') = 'fmb_$i_6' )
& ( product('fmb_$i_7','fmb_$i_7') = 'fmb_$i_7' ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LDA017-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 17:12:34 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.33 Running first-order model finding
% 0.07/0.33 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
% 7.29/1.59 % (2604826)Will run a generic schedule for satisfiability detection.
% 7.29/1.59 % (2604832)% WARNING: option uhcvi not known.
% 7.29/1.59 % (2604835)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2988362565:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.29/1.59 % (2604831)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=906733359_2999 on theBenchmark for (2999ds/0Mi)
% 7.29/1.59 % (2604833)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1237444685:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.29/1.59 % (2604834)dis+10_1_sil=32000:sp=arity:random_seed=845293225:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.29/1.59 % (2604832)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2452585032:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.29/1.59 % (2604836)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1762453458:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.29/1.59 % (2604837)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=785148220:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.29/1.59 % TRYING [1]
% 7.29/1.59 % TRYING [2]
% 7.29/1.59 % TRYING [3]
% 7.29/1.59 % TRYING [4]
% 7.29/1.59 % (2604834)Instruction limit reached!
% 7.29/1.59 % (2604834)------------------------------
% 7.29/1.59 % (2604834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.29/1.59 % (2604834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.59 % (2604834)CaDiCaL version: 2.1.3
% 7.29/1.59 % (2604834)Termination reason: Instruction limit
% 7.29/1.59 % (2604834)Termination phase: Saturation
% 7.29/1.59 % (2604834)Time elapsed: 0.030 s
% 7.29/1.59 % (2604834)Peak memory usage: 12 MB
% 7.29/1.59 % (2604834)Instructions burned: 105 (million)
% 7.29/1.59 % (2604835)Instruction limit reached!
% 7.29/1.59 % (2604835)------------------------------
% 7.29/1.59 % (2604835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.29/1.59 % (2604835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.59 % (2604835)CaDiCaL version: 2.1.3
% 7.29/1.59 % (2604835)Termination reason: Instruction limit
% 7.29/1.59 % (2604835)Termination phase: Saturation
% 7.29/1.59 % (2604835)Time elapsed: 0.039 s
% 7.29/1.59 % (2604835)Peak memory usage: 12 MB
% 7.29/1.59 % (2604835)Instructions burned: 117 (million)
% 7.29/1.59 % (2604845)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3126889486:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.29/1.59 % (2604836)Instruction limit reached!
% 7.29/1.59 % (2604836)------------------------------
% 7.29/1.59 % (2604836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.29/1.59 % (2604836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.59 % (2604836)CaDiCaL version: 2.1.3
% 7.29/1.59 % (2604836)Termination reason: Instruction limit
% 7.29/1.59 % (2604836)Termination phase: Saturation
% 7.29/1.59 % (2604836)Time elapsed: 0.044 s
% 7.29/1.59 % (2604836)Peak memory usage: 12 MB
% 7.29/1.59 % (2604836)Instructions burned: 133 (million)
% 7.29/1.59 % TRYING [1]
% 7.29/1.59 % TRYING [2]
% 7.29/1.59 % TRYING [3]
% 7.29/1.59 % (2604846)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3321876169:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.29/1.59 % (2604837)Instruction limit reached!
% 7.29/1.59 % (2604837)------------------------------
% 7.29/1.59 % (2604837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.29/1.59 % (2604837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.29/1.59 % (2604837)CaDiCaL version: 2.1.3
% 7.29/1.59 % (2604837)Termination reason: Instruction limit
% 7.29/1.59 % (2604837)Termination phase: Saturation
% 7.29/1.59 % (2604837)Time elapsed: 0.050 s
% 7.29/1.59 % (2604837)Peak memory usage: 12 MB
% 7.29/1.59 % (2604837)Instructions burned: 161 (million)
% 7.29/1.59 % (2604848)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=2470445627:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 7.29/1.59 % (2604850)ott-21_1_sil=16000:fs=off:random_seed=2598692712:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 7.29/1.59 % TRYING [4]
% 7.29/1.59 % (2604846)Instruction limit reached!
% 7.29/1.59 % (2604846)------------------------------
% 7.29/1.59 % (2604846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.29/1.59 % (2604846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604846)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604846)Termination reason: Instruction limit
% 23.99/3.91 % (2604846)Termination phase: Saturation
% 23.99/3.91 % (2604846)Time elapsed: 0.044 s
% 23.99/3.91 % (2604846)Peak memory usage: 12 MB
% 23.99/3.91 % (2604846)Instructions burned: 132 (million)
% 23.99/3.91 % (2604853)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3726102820:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 23.99/3.91 % (2604850)Instruction limit reached!
% 23.99/3.91 % (2604850)------------------------------
% 23.99/3.91 % (2604850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.91 % (2604850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604850)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604850)Termination reason: Instruction limit
% 23.99/3.91 % (2604850)Termination phase: Saturation
% 23.99/3.91 % (2604850)Time elapsed: 0.056 s
% 23.99/3.91 % (2604850)Peak memory usage: 12 MB
% 23.99/3.91 % (2604850)Instructions burned: 180 (million)
% 23.99/3.91 % (2604855)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2226583042:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 23.99/3.91 % TRYING [1]
% 23.99/3.91 % TRYING [2]
% 23.99/3.91 % TRYING [3]
% 23.99/3.91 % TRYING [4]
% 23.99/3.91 % (2604853)Instruction limit reached!
% 23.99/3.91 % (2604853)------------------------------
% 23.99/3.91 % (2604853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.91 % (2604853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604853)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604853)Termination reason: Instruction limit
% 23.99/3.91 % (2604853)Termination phase: Saturation
% 23.99/3.91 % (2604853)Time elapsed: 0.133 s
% 23.99/3.91 % (2604853)Peak memory usage: 15 MB
% 23.99/3.91 % (2604853)Instructions burned: 478 (million)
% 23.99/3.91 % (2604848)Instruction limit reached!
% 23.99/3.91 % (2604848)------------------------------
% 23.99/3.91 % (2604848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.91 % (2604848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604848)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604848)Termination reason: Instruction limit
% 23.99/3.91 % (2604848)Termination phase: Saturation
% 23.99/3.91 % (2604848)Time elapsed: 0.191 s
% 23.99/3.91 % (2604848)Peak memory usage: 17 MB
% 23.99/3.91 % (2604848)Instructions burned: 688 (million)
% 23.99/3.91 % (2604857)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=127202509:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 23.99/3.91 % (2604858)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=467767583:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 23.99/3.91 % TRYING [5]
% 23.99/3.91 % (2604845)Instruction limit reached!
% 23.99/3.91 % (2604845)------------------------------
% 23.99/3.91 % (2604845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.91 % (2604845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604845)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604845)Termination reason: Instruction limit
% 23.99/3.91 % (2604845)Termination phase: Finite model building SAT solving
% 23.99/3.91 % (2604845)Time elapsed: 0.258 s
% 23.99/3.91 % (2604845)Peak memory usage: 30 MB
% 23.99/3.91 % (2604845)Instructions burned: 719 (million)
% 23.99/3.91 % (2604861)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=4216628745:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 23.99/3.91 % (2604855)Instruction limit reached!
% 23.99/3.91 % (2604855)------------------------------
% 23.99/3.91 % (2604855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.99/3.91 % (2604855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.99/3.91 % (2604855)CaDiCaL version: 2.1.3
% 23.99/3.91 % (2604855)Termination reason: Instruction limit
% 23.99/3.91 % (2604855)Termination phase: Finite model building SAT solving
% 23.99/3.91 % (2604855)Time elapsed: 0.206 s
% 23.99/3.91 % (2604855)Peak memory usage: 25 MB
% 23.99/3.91 % (2604855)Instructions burned: 866 (million)
% 23.99/3.91 % (2604863)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1745866983:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 23.99/3.91 % (2604858)Instruction limit reached!
% 23.99/3.91 % (2604858)------------------------------
% 23.99/3.91 % (2604858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604858)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604858)Termination reason: Instruction limit
% 80.73/11.88 % (2604858)Termination phase: Finite model building constraint generation
% 80.73/11.88 % (2604858)Time elapsed: 0.240 s
% 80.73/11.88 % (2604858)Peak memory usage: 109 MB
% 80.73/11.88 % (2604858)Instructions burned: 894 (million)
% 80.73/11.88 % (2604865)fmb+10_1_sil=64000:random_seed=3829139095:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 80.73/11.88 % TRYING [1]
% 80.73/11.88 % TRYING [2]
% 80.73/11.88 % TRYING [3]
% 80.73/11.88 % (2604861)Instruction limit reached!
% 80.73/11.88 % (2604861)------------------------------
% 80.73/11.88 % (2604861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604861)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604861)Termination reason: Instruction limit
% 80.73/11.88 % (2604861)Termination phase: Saturation
% 80.73/11.88 % (2604861)Time elapsed: 0.228 s
% 80.73/11.88 % (2604861)Peak memory usage: 17 MB
% 80.73/11.88 % (2604861)Instructions burned: 692 (million)
% 80.73/11.88 % (2604867)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3077728911:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 80.73/11.88 % TRYING [20]
% 80.73/11.88 % TRYING [4]
% 80.73/11.88 % (2604863)Instruction limit reached!
% 80.73/11.88 % (2604863)------------------------------
% 80.73/11.88 % (2604863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604863)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604863)Termination reason: Instruction limit
% 80.73/11.88 % (2604863)Termination phase: Saturation
% 80.73/11.88 % (2604863)Time elapsed: 0.243 s
% 80.73/11.88 % (2604863)Peak memory usage: 17 MB
% 80.73/11.88 % (2604863)Instructions burned: 879 (million)
% 80.73/11.88 % (2604869)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3012870909:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 80.73/11.88 % TRYING [8]
% 80.73/11.88 % (2604857)Instruction limit reached!
% 80.73/11.88 % (2604857)------------------------------
% 80.73/11.88 % (2604857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604857)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604857)Termination reason: Instruction limit
% 80.73/11.88 % (2604857)Termination phase: Saturation
% 80.73/11.88 % (2604857)Time elapsed: 0.404 s
% 80.73/11.88 % (2604857)Peak memory usage: 26 MB
% 80.73/11.88 % (2604857)Instructions burned: 1181 (million)
% 80.73/11.88 % (2604871)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2740029388:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 80.73/11.88 % TRYING [5]
% 80.73/11.88 % (2604869)Instruction limit reached!
% 80.73/11.88 % (2604869)------------------------------
% 80.73/11.88 % (2604869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604869)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604869)Termination reason: Instruction limit
% 80.73/11.88 % (2604869)Termination phase: Finite model building constraint generation
% 80.73/11.88 % (2604869)Time elapsed: 0.179 s
% 80.73/11.88 % (2604869)Peak memory usage: 74 MB
% 80.73/11.88 % (2604869)Instructions burned: 923 (million)
% 80.73/11.88 % (2604873)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1024755271:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 80.73/11.88 % (2604873)Instruction limit reached!
% 80.73/11.88 % (2604873)------------------------------
% 80.73/11.88 % (2604873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 80.73/11.88 % (2604873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.73/11.88 % (2604873)CaDiCaL version: 2.1.3
% 80.73/11.88 % (2604873)Termination reason: Instruction limit
% 80.73/11.88 % (2604873)Termination phase: Saturation
% 80.73/11.88 % (2604873)Time elapsed: 0.405 s
% 80.73/11.88 % (2604873)Peak memory usage: 25 MB
% 80.73/11.88 % (2604873)Instructions burned: 1475 (million)
% 80.73/11.88 % (2604875)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1965181730:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 80.73/11.88 % (2604875)Cannot represent all propositional literals internally
% 80.73/11.88 % (2604875)Refutation not found, incomplete strategy
% 31.51/12.03 % (2604875)------------------------------
% 31.51/12.03 % (2604875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604875)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604875)Termination reason: Refutation not found, incomplete strategy
% 31.51/12.03 % (2604875)Time elapsed: 0.001 s
% 31.51/12.03 % (2604875)Peak memory usage: 10 MB
% 31.51/12.03 % (2604875)Instructions burned: 4 (million)
% 31.51/12.03 % (2604875)------------------------------
% 31.51/12.03 % (2604875)------------------------------
% 31.51/12.03 % (2604877)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4033449168:fmbsr=2.30978:i=2174_2987 on theBenchmark for (2987ds/2174Mi)
% 31.51/12.03 % TRYING [16]
% 31.51/12.03 % (2604877)Instruction limit reached!
% 31.51/12.03 % (2604877)------------------------------
% 31.51/12.03 % (2604877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604877)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604877)Termination reason: Instruction limit
% 31.51/12.03 % (2604877)Termination phase: Finite model building constraint generation
% 31.51/12.03 % (2604877)Time elapsed: 0.410 s
% 31.51/12.03 % (2604877)Peak memory usage: 140 MB
% 31.51/12.03 % (2604877)Instructions burned: 2174 (million)
% 31.51/12.03 % (2604879)ott-2_1_sil=16000:newcnf=on:random_seed=1453648766:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2983 on theBenchmark for (2983ds/869Mi)
% 31.51/12.03 % (2604879)Instruction limit reached!
% 31.51/12.03 % (2604879)------------------------------
% 31.51/12.03 % (2604879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604879)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604879)Termination reason: Instruction limit
% 31.51/12.03 % (2604879)Termination phase: Saturation
% 31.51/12.03 % (2604879)Time elapsed: 0.317 s
% 31.51/12.03 % (2604879)Peak memory usage: 19 MB
% 31.51/12.03 % (2604879)Instructions burned: 869 (million)
% 31.51/12.03 % (2604881)ott+10_1_sil=32000:tgt=ground:random_seed=1880773295:i=5114:av=off_2979 on theBenchmark for (2979ds/5114Mi)
% 31.51/12.03 % (2604871)Instruction limit reached!
% 31.51/12.03 % (2604871)------------------------------
% 31.51/12.03 % (2604871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604871)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604871)Termination reason: Instruction limit
% 31.51/12.03 % (2604871)Termination phase: Saturation
% 31.51/12.03 % (2604871)Time elapsed: 1.445 s
% 31.51/12.03 % (2604871)Peak memory usage: 47 MB
% 31.51/12.03 % (2604871)Instructions burned: 5134 (million)
% 31.51/12.03 % (2604883)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2981071597:i=54282_2978 on theBenchmark for (2978ds/54282Mi)
% 31.51/12.03 % TRYING [1]
% 31.51/12.03 % TRYING [2]
% 31.51/12.03 % TRYING [3]
% 31.51/12.03 % TRYING [4]
% 31.51/12.03 % TRYING [5]
% 31.51/12.03 % (2604867)Instruction limit reached!
% 31.51/12.03 % (2604867)------------------------------
% 31.51/12.03 % (2604867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604867)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604867)Termination reason: Instruction limit
% 31.51/12.03 % (2604867)Termination phase: Finite model building constraint generation
% 31.51/12.03 % (2604867)Time elapsed: 1.910 s
% 31.51/12.03 % (2604867)Peak memory usage: 632 MB
% 31.51/12.03 % (2604867)Instructions burned: 9520 (million)
% 31.51/12.03 % (2604885)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3577075749:i=3512:aac=none_2974 on theBenchmark for (2974ds/3512Mi)
% 31.51/12.03 % TRYING [6]
% 31.51/12.03 % TRYING [6]
% 31.51/12.03 % (2604885)Instruction limit reached!
% 31.51/12.03 % (2604885)------------------------------
% 31.51/12.03 % (2604885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604885)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604885)Termination reason: Instruction limit
% 31.51/12.03 % (2604885)Termination phase: Saturation
% 31.51/12.03 % (2604885)Time elapsed: 1.008 s
% 31.51/12.03 % (2604885)Peak memory usage: 34 MB
% 31.51/12.03 % (2604885)Instructions burned: 3514 (million)
% 31.51/12.03 % (2604887)dis+21_1_sil=32000:sas=cadical:random_seed=1416428159:i=3773:amm=off_2964 on theBenchmark for (2964ds/3773Mi)
% 31.51/12.03 % (2604881)Instruction limit reached!
% 31.51/12.03 % (2604881)------------------------------
% 31.51/12.03 % (2604881)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604881)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604881)Termination reason: Instruction limit
% 31.51/12.03 % (2604881)Termination phase: Saturation
% 31.51/12.03 % (2604881)Time elapsed: 1.931 s
% 31.51/12.03 % (2604881)Peak memory usage: 69 MB
% 31.51/12.03 % (2604881)Instructions burned: 5114 (million)
% 31.51/12.03 % (2604889)ott+11_1_sil=16000:gs=on:random_seed=1736222755:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2960 on theBenchmark for (2960ds/2251Mi)
% 31.51/12.03 % (2604887)Instruction limit reached!
% 31.51/12.03 % (2604887)------------------------------
% 31.51/12.03 % (2604887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604887)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604887)Termination reason: Instruction limit
% 31.51/12.03 % (2604887)Termination phase: Saturation
% 31.51/12.03 % (2604887)Time elapsed: 1.089 s
% 31.51/12.03 % (2604887)Peak memory usage: 36 MB
% 31.51/12.03 % (2604887)Instructions burned: 3780 (million)
% 31.51/12.03 % (2604891)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3624021768:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi)
% 31.51/12.03 % TRYING [7]
% 31.51/12.03 % (2604889)Instruction limit reached!
% 31.51/12.03 % (2604889)------------------------------
% 31.51/12.03 % (2604889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604889)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604889)Termination reason: Instruction limit
% 31.51/12.03 % (2604889)Termination phase: Saturation
% 31.51/12.03 % (2604889)Time elapsed: 0.847 s
% 31.51/12.03 % (2604889)Peak memory usage: 30 MB
% 31.51/12.03 % (2604889)Instructions burned: 2251 (million)
% 31.51/12.03 % (2604893)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1874794366:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2951 on theBenchmark for (2951ds/4591Mi)
% 31.51/12.03 % TRYING [6]
% 31.51/12.03 % (2604893)Instruction limit reached!
% 31.51/12.03 % (2604893)------------------------------
% 31.51/12.03 % (2604893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604893)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604893)Termination reason: Instruction limit
% 31.51/12.03 % (2604893)Termination phase: Saturation
% 31.51/12.03 % (2604893)Time elapsed: 1.036 s
% 31.51/12.03 % (2604893)Peak memory usage: 34 MB
% 31.51/12.03 % (2604893)Instructions burned: 4595 (million)
% 31.51/12.03 % (2604895)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=215342109:i=29340_2941 on theBenchmark for (2941ds/29340Mi)
% 31.51/12.03 % (2604865)Instruction limit reached!
% 31.51/12.03 % (2604865)------------------------------
% 31.51/12.03 % (2604865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604865)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604865)Termination reason: Instruction limit
% 31.51/12.03 % (2604865)Termination phase: Finite model building SAT solving
% 31.51/12.03 % (2604865)Time elapsed: 9.457 s
% 31.51/12.03 % (2604865)Peak memory usage: 184 MB
% 31.51/12.03 % (2604865)Instructions burned: 22062 (million)
% 31.51/12.03 % (2604897)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3459206592:i=5211_2899 on theBenchmark for (2899ds/5211Mi)
% 31.51/12.03 % (2604897)Instruction limit reached!
% 31.51/12.03 % (2604897)------------------------------
% 31.51/12.03 % (2604897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604897)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604897)Termination reason: Instruction limit
% 31.51/12.03 % (2604897)Termination phase: Saturation
% 31.51/12.03 % (2604897)Time elapsed: 1.500 s
% 31.51/12.03 % (2604897)Peak memory usage: 46 MB
% 31.51/12.03 % (2604897)Instructions burned: 5212 (million)
% 31.51/12.03 % Finite Model Found!
% 31.51/12.03 % SZS status Satisfiable for theBenchmark
% 31.51/12.03 % (2604899)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1670909584:i=5497:nm=2_2884 on theBenchmark for (2884ds/5497Mi)
% 31.51/12.03 % TRYING [17]
% 31.51/12.03 % (2604891) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2604826-2604891"...
% 31.51/12.03 % (2604891)...printing done.
% 31.51/12.03 % SZS output start FiniteModel for theBenchmark
% See solution above
% 31.51/12.03 % (2604891)------------------------------
% 31.51/12.03 % (2604891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.51/12.03 % (2604891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.51/12.03 % (2604891)CaDiCaL version: 2.1.3
% 31.51/12.03 % (2604891)Termination reason: Satisfiable
% 31.51/12.03 % (2604891)Time elapsed: 6.946 s
% 31.51/12.03 % (2604891)Peak memory usage: 429 MB
% 31.51/12.03 % (2604891)Instructions burned: 24970 (million)
% 31.51/12.03 % (2604826)Success in time 11.695 s
% 31.51/12.03 % Vampire exiting
%------------------------------------------------------------------------------