Finite Model Found!
% SZS status CounterSatisfiable for SOT_CKvICm
% (2363504)First to succeed.
% (2363504)Solution written to "/tmp/tmp.Lg1dl8vptR/vampire-proof-2363500"
% (2363500)Running in auto input_syntax mode. Trying TPTP
% SZS output start FiniteModel for SOT_CKvICm
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_m,type,m: ($i * $i) > $i).
tff(function_m,axiom,
           m('fmb_$i_1','fmb_$i_1') = 'fmb_$i_7'
         & m('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2'
         & m('fmb_$i_1','fmb_$i_3') = 'fmb_$i_5'
         & m('fmb_$i_1','fmb_$i_4') = 'fmb_$i_3'
         & m('fmb_$i_1','fmb_$i_5') = 'fmb_$i_6'
         & m('fmb_$i_1','fmb_$i_6') = 'fmb_$i_4'
         & m('fmb_$i_1','fmb_$i_7') = 'fmb_$i_1'
         & m('fmb_$i_2','fmb_$i_1') = 'fmb_$i_1'
         & m('fmb_$i_2','fmb_$i_2') = 'fmb_$i_7'
         & m('fmb_$i_2','fmb_$i_3') = 'fmb_$i_4'
         & m('fmb_$i_2','fmb_$i_4') = 'fmb_$i_6'
         & m('fmb_$i_2','fmb_$i_5') = 'fmb_$i_3'
         & m('fmb_$i_2','fmb_$i_6') = 'fmb_$i_5'
         & m('fmb_$i_2','fmb_$i_7') = 'fmb_$i_2'
         & m('fmb_$i_3','fmb_$i_1') = 'fmb_$i_4'
         & m('fmb_$i_3','fmb_$i_2') = 'fmb_$i_5'
         & m('fmb_$i_3','fmb_$i_3') = 'fmb_$i_7'
         & m('fmb_$i_3','fmb_$i_4') = 'fmb_$i_2'
         & m('fmb_$i_3','fmb_$i_5') = 'fmb_$i_1'
         & m('fmb_$i_3','fmb_$i_6') = 'fmb_$i_6'
         & m('fmb_$i_3','fmb_$i_7') = 'fmb_$i_3'
         & m('fmb_$i_4','fmb_$i_1') = 'fmb_$i_6'
         & m('fmb_$i_4','fmb_$i_2') = 'fmb_$i_3'
         & m('fmb_$i_4','fmb_$i_3') = 'fmb_$i_1'
         & m('fmb_$i_4','fmb_$i_4') = 'fmb_$i_7'
         & m('fmb_$i_4','fmb_$i_5') = 'fmb_$i_5'
         & m('fmb_$i_4','fmb_$i_6') = 'fmb_$i_2'
         & m('fmb_$i_4','fmb_$i_7') = 'fmb_$i_4'
         & m('fmb_$i_5','fmb_$i_1') = 'fmb_$i_3'
         & m('fmb_$i_5','fmb_$i_2') = 'fmb_$i_6'
         & m('fmb_$i_5','fmb_$i_3') = 'fmb_$i_2'
         & m('fmb_$i_5','fmb_$i_4') = 'fmb_$i_4'
         & m('fmb_$i_5','fmb_$i_5') = 'fmb_$i_7'
         & m('fmb_$i_5','fmb_$i_6') = 'fmb_$i_1'
         & m('fmb_$i_5','fmb_$i_7') = 'fmb_$i_5'
         & m('fmb_$i_6','fmb_$i_1') = 'fmb_$i_5'
         & m('fmb_$i_6','fmb_$i_2') = 'fmb_$i_4'
         & m('fmb_$i_6','fmb_$i_3') = 'fmb_$i_3'
         & m('fmb_$i_6','fmb_$i_4') = 'fmb_$i_1'
         & m('fmb_$i_6','fmb_$i_5') = 'fmb_$i_2'
         & m('fmb_$i_6','fmb_$i_6') = 'fmb_$i_7'
         & m('fmb_$i_6','fmb_$i_7') = 'fmb_$i_6'
         & m('fmb_$i_7','fmb_$i_1') = 'fmb_$i_2'
         & m('fmb_$i_7','fmb_$i_2') = 'fmb_$i_1'
         & m('fmb_$i_7','fmb_$i_3') = 'fmb_$i_6'
         & m('fmb_$i_7','fmb_$i_4') = 'fmb_$i_5'
         & m('fmb_$i_7','fmb_$i_5') = 'fmb_$i_4'
         & m('fmb_$i_7','fmb_$i_6') = 'fmb_$i_3'
         & m('fmb_$i_7','fmb_$i_7') = 'fmb_$i_7'

).

% SZS output end FiniteModel for SOT_CKvICm
% (2363504)------------------------------
% (2363504)Version: Vampire 4.9 (commit f514ac064 on 2024-07-12 12:58:46 +0200)
% (2363504)Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d
% (2363504)Termination reason: Satisfiable

% (2363504)Memory used [KB]: 2624
% (2363504)Time elapsed: 1.392 s
% (2363504)------------------------------
% (2363504)------------------------------
% (2363500)Success in time 1.438 s
% Vampire exiting

% END OF SYSTEM OUTPUT
% RESULT: SOT_CKvICm - Vampire-SAT---4.9 says CounterSatisfiable - CPU = 9.50 WC = 1.46 
% OUTPUT: SOT_CKvICm - Vampire-SAT---4.9 says Assurance - CPU = 9.50 WC = 1.46