%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN543-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 02:17:32 PM UTC 2026
% Result : Satisfiable 0.21s 0.30s
% Output : FiniteModel 0.21s
% 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('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' )
| ( X = 'fmb_$i_3' ) ) ).
tff('distinct_domain_$i',axiom,
( ( 'fmb_$i_1' != 'fmb_$i_2' )
& ( 'fmb_$i_1' != 'fmb_$i_3' )
& ( 'fmb_$i_2' != 'fmb_$i_3' ) ) ).
tff(declare_a153,type,
a153: $i ).
tff(a153_definition,axiom,
a153 = 'fmb_$i_1' ).
tff(declare_a136,type,
a136: $i ).
tff(a136_definition,axiom,
a136 = 'fmb_$i_2' ).
tff(declare_a119,type,
a119: $i ).
tff(a119_definition,axiom,
a119 = 'fmb_$i_3' ).
tff(declare_a102,type,
a102: $i ).
tff(a102_definition,axiom,
a102 = 'fmb_$i_3' ).
tff(declare_a101,type,
a101: $i ).
tff(a101_definition,axiom,
a101 = 'fmb_$i_3' ).
tff(declare_a79,type,
a79: $i ).
tff(a79_definition,axiom,
a79 = 'fmb_$i_3' ).
tff(declare_a78,type,
a78: $i ).
tff(a78_definition,axiom,
a78 = 'fmb_$i_3' ).
tff(declare_a156,type,
a156: $i ).
tff(a156_definition,axiom,
a156 = 'fmb_$i_3' ).
tff(declare_a154,type,
a154: $i ).
tff(a154_definition,axiom,
a154 = 'fmb_$i_3' ).
tff(declare_a152,type,
a152: $i ).
tff(a152_definition,axiom,
a152 = 'fmb_$i_3' ).
tff(declare_a150,type,
a150: $i ).
tff(a150_definition,axiom,
a150 = 'fmb_$i_3' ).
tff(declare_a149,type,
a149: $i ).
tff(a149_definition,axiom,
a149 = 'fmb_$i_3' ).
tff(declare_a148,type,
a148: $i ).
tff(a148_definition,axiom,
a148 = 'fmb_$i_3' ).
tff(declare_a147,type,
a147: $i ).
tff(a147_definition,axiom,
a147 = 'fmb_$i_3' ).
tff(declare_a146,type,
a146: $i ).
tff(a146_definition,axiom,
a146 = 'fmb_$i_3' ).
tff(declare_a145,type,
a145: $i ).
tff(a145_definition,axiom,
a145 = 'fmb_$i_3' ).
tff(declare_a143,type,
a143: $i ).
tff(a143_definition,axiom,
a143 = 'fmb_$i_3' ).
tff(declare_a142,type,
a142: $i ).
tff(a142_definition,axiom,
a142 = 'fmb_$i_1' ).
tff(declare_a140,type,
a140: $i ).
tff(a140_definition,axiom,
a140 = 'fmb_$i_3' ).
tff(declare_a138,type,
a138: $i ).
tff(a138_definition,axiom,
a138 = 'fmb_$i_3' ).
tff(declare_a137,type,
a137: $i ).
tff(a137_definition,axiom,
a137 = 'fmb_$i_3' ).
tff(declare_a133,type,
a133: $i ).
tff(a133_definition,axiom,
a133 = 'fmb_$i_3' ).
tff(declare_a131,type,
a131: $i ).
tff(a131_definition,axiom,
a131 = 'fmb_$i_3' ).
tff(declare_a129,type,
a129: $i ).
tff(a129_definition,axiom,
a129 = 'fmb_$i_3' ).
tff(declare_a128,type,
a128: $i ).
tff(a128_definition,axiom,
a128 = 'fmb_$i_2' ).
tff(declare_a127,type,
a127: $i ).
tff(a127_definition,axiom,
a127 = 'fmb_$i_3' ).
tff(declare_a126,type,
a126: $i ).
tff(a126_definition,axiom,
a126 = 'fmb_$i_1' ).
tff(declare_a125,type,
a125: $i ).
tff(a125_definition,axiom,
a125 = 'fmb_$i_3' ).
tff(declare_a124,type,
a124: $i ).
tff(a124_definition,axiom,
a124 = 'fmb_$i_3' ).
tff(declare_a123,type,
a123: $i ).
tff(a123_definition,axiom,
a123 = 'fmb_$i_3' ).
tff(declare_a121,type,
a121: $i ).
tff(a121_definition,axiom,
a121 = 'fmb_$i_3' ).
tff(declare_a120,type,
a120: $i ).
tff(a120_definition,axiom,
a120 = 'fmb_$i_3' ).
tff(declare_a118,type,
a118: $i ).
tff(a118_definition,axiom,
a118 = 'fmb_$i_3' ).
tff(declare_a117,type,
a117: $i ).
tff(a117_definition,axiom,
a117 = 'fmb_$i_3' ).
tff(declare_a115,type,
a115: $i ).
tff(a115_definition,axiom,
a115 = 'fmb_$i_3' ).
tff(declare_a113,type,
a113: $i ).
tff(a113_definition,axiom,
a113 = 'fmb_$i_3' ).
tff(declare_a111,type,
a111: $i ).
tff(a111_definition,axiom,
a111 = 'fmb_$i_3' ).
tff(declare_a109,type,
a109: $i ).
tff(a109_definition,axiom,
a109 = 'fmb_$i_3' ).
tff(declare_a106,type,
a106: $i ).
tff(a106_definition,axiom,
a106 = 'fmb_$i_2' ).
tff(declare_a105,type,
a105: $i ).
tff(a105_definition,axiom,
a105 = 'fmb_$i_3' ).
tff(declare_a103,type,
a103: $i ).
tff(a103_definition,axiom,
a103 = 'fmb_$i_3' ).
tff(declare_a100,type,
a100: $i ).
tff(a100_definition,axiom,
a100 = 'fmb_$i_3' ).
tff(declare_a99,type,
a99: $i ).
tff(a99_definition,axiom,
a99 = 'fmb_$i_2' ).
tff(declare_a98,type,
a98: $i ).
tff(a98_definition,axiom,
a98 = 'fmb_$i_3' ).
tff(declare_a97,type,
a97: $i ).
tff(a97_definition,axiom,
a97 = 'fmb_$i_3' ).
tff(declare_a96,type,
a96: $i ).
tff(a96_definition,axiom,
a96 = 'fmb_$i_3' ).
tff(declare_a95,type,
a95: $i ).
tff(a95_definition,axiom,
a95 = 'fmb_$i_3' ).
tff(declare_a94,type,
a94: $i ).
tff(a94_definition,axiom,
a94 = 'fmb_$i_3' ).
tff(declare_a93,type,
a93: $i ).
tff(a93_definition,axiom,
a93 = 'fmb_$i_3' ).
tff(declare_a92,type,
a92: $i ).
tff(a92_definition,axiom,
a92 = 'fmb_$i_3' ).
tff(declare_a90,type,
a90: $i ).
tff(a90_definition,axiom,
a90 = 'fmb_$i_3' ).
tff(declare_a89,type,
a89: $i ).
tff(a89_definition,axiom,
a89 = 'fmb_$i_3' ).
tff(declare_a87,type,
a87: $i ).
tff(a87_definition,axiom,
a87 = 'fmb_$i_3' ).
tff(declare_a86,type,
a86: $i ).
tff(a86_definition,axiom,
a86 = 'fmb_$i_3' ).
tff(declare_a85,type,
a85: $i ).
tff(a85_definition,axiom,
a85 = 'fmb_$i_3' ).
tff(declare_a84,type,
a84: $i ).
tff(a84_definition,axiom,
a84 = 'fmb_$i_3' ).
tff(declare_a82,type,
a82: $i ).
tff(a82_definition,axiom,
a82 = 'fmb_$i_3' ).
tff(declare_a80,type,
a80: $i ).
tff(a80_definition,axiom,
a80 = 'fmb_$i_3' ).
tff(declare_a141,type,
a141: $i ).
tff(a141_definition,axiom,
a141 = 'fmb_$i_3' ).
tff(declare_a135,type,
a135: $i ).
tff(a135_definition,axiom,
a135 = 'fmb_$i_3' ).
tff(declare_a116,type,
a116: $i ).
tff(a116_definition,axiom,
a116 = 'fmb_$i_3' ).
tff(declare_a114,type,
a114: $i ).
tff(a114_definition,axiom,
a114 = 'fmb_$i_3' ).
tff(declare_a108,type,
a108: $i ).
tff(a108_definition,axiom,
a108 = 'fmb_$i_3' ).
tff(declare_a91,type,
a91: $i ).
tff(a91_definition,axiom,
a91 = 'fmb_$i_3' ).
tff(declare_a81,type,
a81: $i ).
tff(a81_definition,axiom,
a81 = 'fmb_$i_3' ).
tff(declare_hskp64,type,
hskp64: $o ).
tff(hskp64_definition,axiom,
hskp64 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_hskp63,type,
hskp63: $o ).
tff(hskp63_definition,axiom,
~ hskp63 ).
tff(declare_hskp62,type,
hskp62: $o ).
tff(hskp62_definition,axiom,
~ hskp62 ).
tff(declare_hskp61,type,
hskp61: $o ).
tff(hskp61_definition,axiom,
~ hskp61 ).
tff(declare_hskp60,type,
hskp60: $o ).
tff(hskp60_definition,axiom,
~ hskp60 ).
tff(declare_hskp59,type,
hskp59: $o ).
tff(hskp59_definition,axiom,
~ hskp59 ).
tff(declare_hskp58,type,
hskp58: $o ).
tff(hskp58_definition,axiom,
~ hskp58 ).
tff(declare_hskp57,type,
hskp57: $o ).
tff(hskp57_definition,axiom,
~ hskp57 ).
tff(declare_hskp56,type,
hskp56: $o ).
tff(hskp56_definition,axiom,
~ hskp56 ).
tff(declare_hskp55,type,
hskp55: $o ).
tff(hskp55_definition,axiom,
~ hskp55 ).
tff(declare_hskp54,type,
hskp54: $o ).
tff(hskp54_definition,axiom,
hskp54 ).
tff(declare_hskp53,type,
hskp53: $o ).
tff(hskp53_definition,axiom,
~ hskp53 ).
tff(declare_hskp52,type,
hskp52: $o ).
tff(hskp52_definition,axiom,
~ hskp52 ).
tff(declare_hskp51,type,
hskp51: $o ).
tff(hskp51_definition,axiom,
hskp51 ).
tff(declare_hskp50,type,
hskp50: $o ).
tff(hskp50_definition,axiom,
~ hskp50 ).
tff(declare_hskp49,type,
hskp49: $o ).
tff(hskp49_definition,axiom,
~ hskp49 ).
tff(declare_hskp48,type,
hskp48: $o ).
tff(hskp48_definition,axiom,
~ hskp48 ).
tff(declare_hskp47,type,
hskp47: $o ).
tff(hskp47_definition,axiom,
hskp47 ).
tff(declare_hskp46,type,
hskp46: $o ).
tff(hskp46_definition,axiom,
hskp46 ).
tff(declare_hskp45,type,
hskp45: $o ).
tff(hskp45_definition,axiom,
~ hskp45 ).
tff(declare_hskp44,type,
hskp44: $o ).
tff(hskp44_definition,axiom,
hskp44 ).
tff(declare_hskp43,type,
hskp43: $o ).
tff(hskp43_definition,axiom,
~ hskp43 ).
tff(declare_hskp42,type,
hskp42: $o ).
tff(hskp42_definition,axiom,
hskp42 ).
tff(declare_hskp41,type,
hskp41: $o ).
tff(hskp41_definition,axiom,
~ hskp41 ).
tff(declare_hskp40,type,
hskp40: $o ).
tff(hskp40_definition,axiom,
~ hskp40 ).
tff(declare_hskp39,type,
hskp39: $o ).
tff(hskp39_definition,axiom,
~ hskp39 ).
tff(declare_hskp38,type,
hskp38: $o ).
tff(hskp38_definition,axiom,
hskp38 ).
tff(declare_hskp37,type,
hskp37: $o ).
tff(hskp37_definition,axiom,
~ hskp37 ).
tff(declare_hskp36,type,
hskp36: $o ).
tff(hskp36_definition,axiom,
hskp36 ).
tff(declare_hskp35,type,
hskp35: $o ).
tff(hskp35_definition,axiom,
~ hskp35 ).
tff(declare_hskp34,type,
hskp34: $o ).
tff(hskp34_definition,axiom,
~ hskp34 ).
tff(declare_hskp33,type,
hskp33: $o ).
tff(hskp33_definition,axiom,
hskp33 ).
tff(declare_hskp32,type,
hskp32: $o ).
tff(hskp32_definition,axiom,
~ hskp32 ).
tff(declare_hskp31,type,
hskp31: $o ).
tff(hskp31_definition,axiom,
~ hskp31 ).
tff(declare_hskp30,type,
hskp30: $o ).
tff(hskp30_definition,axiom,
~ hskp30 ).
tff(declare_hskp29,type,
hskp29: $o ).
tff(hskp29_definition,axiom,
~ hskp29 ).
tff(declare_hskp28,type,
hskp28: $o ).
tff(hskp28_definition,axiom,
~ hskp28 ).
tff(declare_hskp27,type,
hskp27: $o ).
tff(hskp27_definition,axiom,
~ hskp27 ).
tff(declare_hskp26,type,
hskp26: $o ).
tff(hskp26_definition,axiom,
~ hskp26 ).
tff(declare_hskp25,type,
hskp25: $o ).
tff(hskp25_definition,axiom,
~ hskp25 ).
tff(declare_hskp24,type,
hskp24: $o ).
tff(hskp24_definition,axiom,
~ hskp24 ).
tff(declare_hskp23,type,
hskp23: $o ).
tff(hskp23_definition,axiom,
~ hskp23 ).
tff(declare_hskp22,type,
hskp22: $o ).
tff(hskp22_definition,axiom,
~ hskp22 ).
tff(declare_hskp21,type,
hskp21: $o ).
tff(hskp21_definition,axiom,
~ hskp21 ).
tff(declare_hskp20,type,
hskp20: $o ).
tff(hskp20_definition,axiom,
~ hskp20 ).
tff(declare_hskp19,type,
hskp19: $o ).
tff(hskp19_definition,axiom,
~ hskp19 ).
tff(declare_hskp18,type,
hskp18: $o ).
tff(hskp18_definition,axiom,
~ hskp18 ).
tff(declare_hskp17,type,
hskp17: $o ).
tff(hskp17_definition,axiom,
hskp17 ).
tff(declare_hskp16,type,
hskp16: $o ).
tff(hskp16_definition,axiom,
~ hskp16 ).
tff(declare_hskp15,type,
hskp15: $o ).
tff(hskp15_definition,axiom,
~ hskp15 ).
tff(declare_hskp14,type,
hskp14: $o ).
tff(hskp14_definition,axiom,
hskp14 ).
tff(declare_hskp13,type,
hskp13: $o ).
tff(hskp13_definition,axiom,
~ hskp13 ).
tff(declare_hskp12,type,
hskp12: $o ).
tff(hskp12_definition,axiom,
~ hskp12 ).
tff(declare_hskp11,type,
hskp11: $o ).
tff(hskp11_definition,axiom,
~ hskp11 ).
tff(declare_hskp10,type,
hskp10: $o ).
tff(hskp10_definition,axiom,
~ hskp10 ).
tff(declare_hskp9,type,
hskp9: $o ).
tff(hskp9_definition,axiom,
~ hskp9 ).
tff(declare_hskp8,type,
hskp8: $o ).
tff(hskp8_definition,axiom,
~ hskp8 ).
tff(declare_hskp7,type,
hskp7: $o ).
tff(hskp7_definition,axiom,
~ hskp7 ).
tff(declare_hskp6,type,
hskp6: $o ).
tff(hskp6_definition,axiom,
~ hskp6 ).
tff(declare_hskp5,type,
hskp5: $o ).
tff(hskp5_definition,axiom,
~ hskp5 ).
tff(declare_hskp4,type,
hskp4: $o ).
tff(hskp4_definition,axiom,
~ hskp4 ).
tff(declare_hskp3,type,
hskp3: $o ).
tff(hskp3_definition,axiom,
~ hskp3 ).
tff(declare_hskp2,type,
hskp2: $o ).
tff(hskp2_definition,axiom,
~ hskp2 ).
tff(declare_hskp1,type,
hskp1: $o ).
tff(hskp1_definition,axiom,
~ hskp1 ).
tff(declare_hskp0,type,
hskp0: $o ).
tff(hskp0_definition,axiom,
~ hskp0 ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( c3_1('fmb_$i_1')
& c3_1('fmb_$i_2')
& ~ c3_1('fmb_$i_3') ) ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
( c4_1('fmb_$i_1')
& c4_1('fmb_$i_2')
& c4_1('fmb_$i_3') ) ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
( c5_1('fmb_$i_1')
& ~ c5_1('fmb_$i_2')
& c5_1('fmb_$i_3') ) ).
tff(declare_c0_1,type,
c0_1: $i > $o ).
tff(predicate_c0_1,axiom,
( c0_1('fmb_$i_1')
& c0_1('fmb_$i_2')
& ~ c0_1('fmb_$i_3') ) ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& ~ c1_1('fmb_$i_2')
& ~ c1_1('fmb_$i_3') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( ~ c2_1('fmb_$i_1')
& c2_1('fmb_$i_2')
& ~ c2_1('fmb_$i_3') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN543-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n007.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:25:10 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 0.21/0.30 % (2534314)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (2534322)dis+10_1_sil=32000:sp=arity:random_seed=4178884416:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (2534320)% WARNING: option uhcvi not known.
% 0.21/0.30 % (2534320)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=871879887:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (2534319)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1230611270_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (2534321)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2182524186:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (2534323)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2150767841:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (2534325)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3658014420:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % (2534324)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3075723110:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % Detected minimum model sizes of [1]
% 0.21/0.30 % Detected maximum model sizes of [65]
% 0.21/0.30 % TRYING [1]
% 0.21/0.30 % TRYING [2]
% 0.21/0.30 % TRYING [3]
% 0.21/0.30 % Finite Model Found!
% 0.21/0.30 % SZS status Satisfiable for theBenchmark
% 0.21/0.30 % (2534319) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2534314-2534319"...
% 0.21/0.30 % (2534319)...printing done.
% 0.21/0.30 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.21/0.31 % (2534319)------------------------------
% 0.21/0.31 % (2534319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (2534319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (2534319)CaDiCaL version: 2.1.3
% 0.21/0.31 % (2534319)Termination reason: Satisfiable
% 0.21/0.31 % (2534319)Time elapsed: 0.020 s
% 0.21/0.31 % (2534319)Peak memory usage: 12 MB
% 0.21/0.31 % (2534319)Instructions burned: 37 (million)
% 0.21/0.31 % (2534314)Success in time 0.067 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------