%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN431+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:07:52 PM UTC 2026
% Result : CounterSatisfiable 0.20s 0.27s
% Output : FiniteModel 0.20s
% 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_a132,type,
a132: $i ).
tff(a132_definition,axiom,
a132 = 'fmb_$i_1' ).
tff(declare_a133,type,
a133: $i ).
tff(a133_definition,axiom,
a133 = 'fmb_$i_2' ).
tff(declare_a135,type,
a135: $i ).
tff(a135_definition,axiom,
a135 = 'fmb_$i_3' ).
tff(declare_a136,type,
a136: $i ).
tff(a136_definition,axiom,
a136 = 'fmb_$i_3' ).
tff(declare_a137,type,
a137: $i ).
tff(a137_definition,axiom,
a137 = 'fmb_$i_3' ).
tff(declare_a139,type,
a139: $i ).
tff(a139_definition,axiom,
a139 = 'fmb_$i_3' ).
tff(declare_a140,type,
a140: $i ).
tff(a140_definition,axiom,
a140 = 'fmb_$i_3' ).
tff(declare_a141,type,
a141: $i ).
tff(a141_definition,axiom,
a141 = 'fmb_$i_3' ).
tff(declare_a142,type,
a142: $i ).
tff(a142_definition,axiom,
a142 = 'fmb_$i_3' ).
tff(declare_a145,type,
a145: $i ).
tff(a145_definition,axiom,
a145 = 'fmb_$i_3' ).
tff(declare_a146,type,
a146: $i ).
tff(a146_definition,axiom,
a146 = 'fmb_$i_3' ).
tff(declare_a151,type,
a151: $i ).
tff(a151_definition,axiom,
a151 = 'fmb_$i_3' ).
tff(declare_a154,type,
a154: $i ).
tff(a154_definition,axiom,
a154 = 'fmb_$i_3' ).
tff(declare_a156,type,
a156: $i ).
tff(a156_definition,axiom,
a156 = 'fmb_$i_3' ).
tff(declare_a159,type,
a159: $i ).
tff(a159_definition,axiom,
a159 = 'fmb_$i_3' ).
tff(declare_a160,type,
a160: $i ).
tff(a160_definition,axiom,
a160 = 'fmb_$i_3' ).
tff(declare_a161,type,
a161: $i ).
tff(a161_definition,axiom,
a161 = 'fmb_$i_3' ).
tff(declare_a134,type,
a134: $i ).
tff(a134_definition,axiom,
a134 = 'fmb_$i_3' ).
tff(declare_a138,type,
a138: $i ).
tff(a138_definition,axiom,
a138 = 'fmb_$i_3' ).
tff(declare_a143,type,
a143: $i ).
tff(a143_definition,axiom,
a143 = 'fmb_$i_3' ).
tff(declare_a144,type,
a144: $i ).
tff(a144_definition,axiom,
a144 = 'fmb_$i_2' ).
tff(declare_a147,type,
a147: $i ).
tff(a147_definition,axiom,
a147 = 'fmb_$i_3' ).
tff(declare_a148,type,
a148: $i ).
tff(a148_definition,axiom,
a148 = 'fmb_$i_3' ).
tff(declare_a149,type,
a149: $i ).
tff(a149_definition,axiom,
a149 = 'fmb_$i_1' ).
tff(declare_a150,type,
a150: $i ).
tff(a150_definition,axiom,
a150 = 'fmb_$i_3' ).
tff(declare_a152,type,
a152: $i ).
tff(a152_definition,axiom,
a152 = 'fmb_$i_2' ).
tff(declare_a153,type,
a153: $i ).
tff(a153_definition,axiom,
a153 = 'fmb_$i_3' ).
tff(declare_a157,type,
a157: $i ).
tff(a157_definition,axiom,
a157 = 'fmb_$i_2' ).
tff(declare_a158,type,
a158: $i ).
tff(a158_definition,axiom,
a158 = 'fmb_$i_3' ).
tff(declare_hskp0,type,
hskp0: $o ).
tff(hskp0_definition,axiom,
~ hskp0 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_hskp1,type,
hskp1: $o ).
tff(hskp1_definition,axiom,
~ hskp1 ).
tff(declare_hskp2,type,
hskp2: $o ).
tff(hskp2_definition,axiom,
~ hskp2 ).
tff(declare_hskp3,type,
hskp3: $o ).
tff(hskp3_definition,axiom,
~ hskp3 ).
tff(declare_hskp4,type,
hskp4: $o ).
tff(hskp4_definition,axiom,
~ hskp4 ).
tff(declare_hskp5,type,
hskp5: $o ).
tff(hskp5_definition,axiom,
hskp5 ).
tff(declare_hskp6,type,
hskp6: $o ).
tff(hskp6_definition,axiom,
~ hskp6 ).
tff(declare_hskp7,type,
hskp7: $o ).
tff(hskp7_definition,axiom,
~ hskp7 ).
tff(declare_hskp8,type,
hskp8: $o ).
tff(hskp8_definition,axiom,
~ hskp8 ).
tff(declare_hskp9,type,
hskp9: $o ).
tff(hskp9_definition,axiom,
~ hskp9 ).
tff(declare_hskp10,type,
hskp10: $o ).
tff(hskp10_definition,axiom,
~ hskp10 ).
tff(declare_hskp11,type,
hskp11: $o ).
tff(hskp11_definition,axiom,
~ hskp11 ).
tff(declare_hskp12,type,
hskp12: $o ).
tff(hskp12_definition,axiom,
~ hskp12 ).
tff(declare_hskp13,type,
hskp13: $o ).
tff(hskp13_definition,axiom,
~ hskp13 ).
tff(declare_hskp14,type,
hskp14: $o ).
tff(hskp14_definition,axiom,
~ hskp14 ).
tff(declare_hskp15,type,
hskp15: $o ).
tff(hskp15_definition,axiom,
~ hskp15 ).
tff(declare_hskp16,type,
hskp16: $o ).
tff(hskp16_definition,axiom,
hskp16 ).
tff(declare_hskp17,type,
hskp17: $o ).
tff(hskp17_definition,axiom,
~ hskp17 ).
tff(declare_hskp18,type,
hskp18: $o ).
tff(hskp18_definition,axiom,
~ hskp18 ).
tff(declare_hskp19,type,
hskp19: $o ).
tff(hskp19_definition,axiom,
~ hskp19 ).
tff(declare_hskp20,type,
hskp20: $o ).
tff(hskp20_definition,axiom,
hskp20 ).
tff(declare_hskp21,type,
hskp21: $o ).
tff(hskp21_definition,axiom,
~ hskp21 ).
tff(declare_hskp22,type,
hskp22: $o ).
tff(hskp22_definition,axiom,
~ hskp22 ).
tff(declare_hskp23,type,
hskp23: $o ).
tff(hskp23_definition,axiom,
hskp23 ).
tff(declare_hskp24,type,
hskp24: $o ).
tff(hskp24_definition,axiom,
~ hskp24 ).
tff(declare_hskp25,type,
hskp25: $o ).
tff(hskp25_definition,axiom,
hskp25 ).
tff(declare_hskp26,type,
hskp26: $o ).
tff(hskp26_definition,axiom,
~ hskp26 ).
tff(declare_hskp27,type,
hskp27: $o ).
tff(hskp27_definition,axiom,
hskp27 ).
tff(declare_hskp28,type,
hskp28: $o ).
tff(hskp28_definition,axiom,
~ hskp28 ).
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_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_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_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.03 % Problem : SYN431+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n020.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 15:57:35 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 0.20/0.27 % (272083)Will run a generic schedule for satisfiability detection.
% 0.20/0.27 % (272088)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=95665744_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.27 % Detected minimum model sizes of [1]
% 0.20/0.27 % Detected maximum model sizes of [29]
% 0.20/0.27 % TRYING [1]
% 0.20/0.27 % TRYING [2]
% 0.20/0.27 % TRYING [3]
% 0.20/0.27 % Finite Model Found!
% 0.20/0.27 % SZS status CounterSatisfiable for theBenchmark
% 0.20/0.27 % (272088) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-272083-272088"...
% 0.20/0.27 % (272089)% WARNING: option uhcvi not known.
% 0.20/0.27 % (272088)...printing done.
% 0.20/0.27 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.20/0.27 % (272088)------------------------------
% 0.20/0.27 % (272088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.27 % (272088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.27 % (272088)CaDiCaL version: 2.1.3
% 0.20/0.27 % (272088)Termination reason: Satisfiable
% 0.20/0.27 % (272088)Time elapsed: 0.004 s
% 0.20/0.27 % (272088)Peak memory usage: 11 MB
% 0.20/0.27 % (272088)Instructions burned: 12 (million)
% 0.20/0.27 % (272083)Success in time 0.042 s
% 0.20/0.27 % Vampire exiting
%------------------------------------------------------------------------------