Finite Model Found!
% SZS status CounterSatisfiable for SOT_juffGX
% (2355823)First to succeed.
% (2355823)Solution written to "/tmp/tmp.L13SxJZKuk/vampire-proof-2355822"
% (2355822)Running in auto input_syntax mode. Trying TPTP
% SZS output start FiniteModel for SOT_juffGX
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('declare_$i8',type,'fmb_$i_8':$i).
tff('declare_$i9',type,'fmb_$i_9':$i).
tff('declare_$i10',type,'fmb_$i_10':$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' | X = 'fmb_$i_8' | X = 'fmb_$i_9' | X = 'fmb_$i_10'
      ) ).

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_1' != 'fmb_$i_8' & 'fmb_$i_1' != 'fmb_$i_9' & 'fmb_$i_1' != 'fmb_$i_10' & '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_2' != 'fmb_$i_8' & 
         'fmb_$i_2' != 'fmb_$i_9' & 'fmb_$i_2' != 'fmb_$i_10' & '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_3' != 'fmb_$i_8' & 'fmb_$i_3' != 'fmb_$i_9' & 'fmb_$i_3' != 'fmb_$i_10' & 'fmb_$i_4' != 'fmb_$i_5' & 
         'fmb_$i_4' != 'fmb_$i_6' & 'fmb_$i_4' != 'fmb_$i_7' & 'fmb_$i_4' != 'fmb_$i_8' & 'fmb_$i_4' != 'fmb_$i_9' & 'fmb_$i_4' != 'fmb_$i_10' & 
         'fmb_$i_5' != 'fmb_$i_6' & 'fmb_$i_5' != 'fmb_$i_7' & 'fmb_$i_5' != 'fmb_$i_8' & 'fmb_$i_5' != 'fmb_$i_9' & 'fmb_$i_5' != 'fmb_$i_10' & 
         'fmb_$i_6' != 'fmb_$i_7' & 'fmb_$i_6' != 'fmb_$i_8' & 'fmb_$i_6' != 'fmb_$i_9' & 'fmb_$i_6' != 'fmb_$i_10' & 'fmb_$i_7' != 'fmb_$i_8' & 
         'fmb_$i_7' != 'fmb_$i_9' & 'fmb_$i_7' != 'fmb_$i_10' & 'fmb_$i_8' != 'fmb_$i_9' & 'fmb_$i_8' != 'fmb_$i_10' & 'fmb_$i_9' != 'fmb_$i_10'
).

tff(declare_m,type,m: ($i * $i) > $i).
tff(function_m,axiom,
           m('fmb_$i_1','fmb_$i_1') = 'fmb_$i_5'
         & m('fmb_$i_1','fmb_$i_2') = 'fmb_$i_10'
         & m('fmb_$i_1','fmb_$i_3') = 'fmb_$i_3'
         & m('fmb_$i_1','fmb_$i_4') = 'fmb_$i_8'
         & m('fmb_$i_1','fmb_$i_5') = 'fmb_$i_1'
         & m('fmb_$i_1','fmb_$i_6') = 'fmb_$i_6'
         & m('fmb_$i_1','fmb_$i_7') = 'fmb_$i_2'
         & m('fmb_$i_1','fmb_$i_8') = 'fmb_$i_4'
         & m('fmb_$i_1','fmb_$i_9') = 'fmb_$i_7'
         & m('fmb_$i_1','fmb_$i_10') = 'fmb_$i_9'
         & m('fmb_$i_2','fmb_$i_1') = 'fmb_$i_4'
         & m('fmb_$i_2','fmb_$i_2') = 'fmb_$i_5'
         & m('fmb_$i_2','fmb_$i_3') = 'fmb_$i_1'
         & m('fmb_$i_2','fmb_$i_4') = 'fmb_$i_7'
         & m('fmb_$i_2','fmb_$i_5') = 'fmb_$i_2'
         & m('fmb_$i_2','fmb_$i_6') = 'fmb_$i_8'
         & m('fmb_$i_2','fmb_$i_7') = 'fmb_$i_9'
         & m('fmb_$i_2','fmb_$i_8') = 'fmb_$i_6'
         & m('fmb_$i_2','fmb_$i_9') = 'fmb_$i_10'
         & m('fmb_$i_2','fmb_$i_10') = 'fmb_$i_3'
         & m('fmb_$i_3','fmb_$i_1') = 'fmb_$i_7'
         & m('fmb_$i_3','fmb_$i_2') = 'fmb_$i_8'
         & m('fmb_$i_3','fmb_$i_3') = 'fmb_$i_5'
         & m('fmb_$i_3','fmb_$i_4') = 'fmb_$i_2'
         & m('fmb_$i_3','fmb_$i_5') = 'fmb_$i_3'
         & m('fmb_$i_3','fmb_$i_6') = 'fmb_$i_4'
         & m('fmb_$i_3','fmb_$i_7') = 'fmb_$i_1'
         & m('fmb_$i_3','fmb_$i_8') = 'fmb_$i_9'
         & m('fmb_$i_3','fmb_$i_9') = 'fmb_$i_6'
         & m('fmb_$i_3','fmb_$i_10') = 'fmb_$i_10'
         & m('fmb_$i_4','fmb_$i_1') = 'fmb_$i_1'
         & m('fmb_$i_4','fmb_$i_2') = 'fmb_$i_3'
         & m('fmb_$i_4','fmb_$i_3') = 'fmb_$i_6'
         & m('fmb_$i_4','fmb_$i_4') = 'fmb_$i_5'
         & m('fmb_$i_4','fmb_$i_5') = 'fmb_$i_4'
         & m('fmb_$i_4','fmb_$i_6') = 'fmb_$i_9'
         & m('fmb_$i_4','fmb_$i_7') = 'fmb_$i_10'
         & m('fmb_$i_4','fmb_$i_8') = 'fmb_$i_2'
         & m('fmb_$i_4','fmb_$i_9') = 'fmb_$i_8'
         & m('fmb_$i_4','fmb_$i_10') = 'fmb_$i_7'
         & m('fmb_$i_5','fmb_$i_1') = 'fmb_$i_8'
         & m('fmb_$i_5','fmb_$i_2') = 'fmb_$i_6'
         & m('fmb_$i_5','fmb_$i_3') = 'fmb_$i_7'
         & m('fmb_$i_5','fmb_$i_4') = 'fmb_$i_10'
         & m('fmb_$i_5','fmb_$i_5') = 'fmb_$i_5'
         & m('fmb_$i_5','fmb_$i_6') = 'fmb_$i_2'
         & m('fmb_$i_5','fmb_$i_7') = 'fmb_$i_3'
         & m('fmb_$i_5','fmb_$i_8') = 'fmb_$i_1'
         & m('fmb_$i_5','fmb_$i_9') = 'fmb_$i_9'
         & m('fmb_$i_5','fmb_$i_10') = 'fmb_$i_4'
         & m('fmb_$i_6','fmb_$i_1') = 'fmb_$i_2'
         & m('fmb_$i_6','fmb_$i_2') = 'fmb_$i_1'
         & m('fmb_$i_6','fmb_$i_3') = 'fmb_$i_10'
         & m('fmb_$i_6','fmb_$i_4') = 'fmb_$i_9'
         & m('fmb_$i_6','fmb_$i_5') = 'fmb_$i_6'
         & m('fmb_$i_6','fmb_$i_6') = 'fmb_$i_5'
         & m('fmb_$i_6','fmb_$i_7') = 'fmb_$i_4'
         & m('fmb_$i_6','fmb_$i_8') = 'fmb_$i_7'
         & m('fmb_$i_6','fmb_$i_9') = 'fmb_$i_3'
         & m('fmb_$i_6','fmb_$i_10') = 'fmb_$i_8'
         & m('fmb_$i_7','fmb_$i_1') = 'fmb_$i_6'
         & m('fmb_$i_7','fmb_$i_2') = 'fmb_$i_9'
         & m('fmb_$i_7','fmb_$i_3') = 'fmb_$i_8'
         & m('fmb_$i_7','fmb_$i_4') = 'fmb_$i_4'
         & m('fmb_$i_7','fmb_$i_5') = 'fmb_$i_7'
         & m('fmb_$i_7','fmb_$i_6') = 'fmb_$i_10'
         & m('fmb_$i_7','fmb_$i_7') = 'fmb_$i_5'
         & m('fmb_$i_7','fmb_$i_8') = 'fmb_$i_3'
         & m('fmb_$i_7','fmb_$i_9') = 'fmb_$i_1'
         & m('fmb_$i_7','fmb_$i_10') = 'fmb_$i_2'
         & m('fmb_$i_8','fmb_$i_1') = 'fmb_$i_10'
         & m('fmb_$i_8','fmb_$i_2') = 'fmb_$i_2'
         & m('fmb_$i_8','fmb_$i_3') = 'fmb_$i_9'
         & m('fmb_$i_8','fmb_$i_4') = 'fmb_$i_6'
         & m('fmb_$i_8','fmb_$i_5') = 'fmb_$i_8'
         & m('fmb_$i_8','fmb_$i_6') = 'fmb_$i_3'
         & m('fmb_$i_8','fmb_$i_7') = 'fmb_$i_7'
         & m('fmb_$i_8','fmb_$i_8') = 'fmb_$i_5'
         & m('fmb_$i_8','fmb_$i_9') = 'fmb_$i_4'
         & m('fmb_$i_8','fmb_$i_10') = 'fmb_$i_1'
         & m('fmb_$i_9','fmb_$i_1') = 'fmb_$i_3'
         & m('fmb_$i_9','fmb_$i_2') = 'fmb_$i_4'
         & m('fmb_$i_9','fmb_$i_3') = 'fmb_$i_2'
         & m('fmb_$i_9','fmb_$i_4') = 'fmb_$i_1'
         & m('fmb_$i_9','fmb_$i_5') = 'fmb_$i_9'
         & m('fmb_$i_9','fmb_$i_6') = 'fmb_$i_7'
         & m('fmb_$i_9','fmb_$i_7') = 'fmb_$i_8'
         & m('fmb_$i_9','fmb_$i_8') = 'fmb_$i_10'
         & m('fmb_$i_9','fmb_$i_9') = 'fmb_$i_5'
         & m('fmb_$i_9','fmb_$i_10') = 'fmb_$i_6'
         & m('fmb_$i_10','fmb_$i_1') = 'fmb_$i_9'
         & m('fmb_$i_10','fmb_$i_2') = 'fmb_$i_7'
         & m('fmb_$i_10','fmb_$i_3') = 'fmb_$i_4'
         & m('fmb_$i_10','fmb_$i_4') = 'fmb_$i_3'
         & m('fmb_$i_10','fmb_$i_5') = 'fmb_$i_10'
         & m('fmb_$i_10','fmb_$i_6') = 'fmb_$i_1'
         & m('fmb_$i_10','fmb_$i_7') = 'fmb_$i_6'
         & m('fmb_$i_10','fmb_$i_8') = 'fmb_$i_8'
         & m('fmb_$i_10','fmb_$i_9') = 'fmb_$i_2'
         & m('fmb_$i_10','fmb_$i_10') = 'fmb_$i_5'

).

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

% (2355823)Memory used [KB]: 2616
% (2355823)Time elapsed: 0.108 s
% (2355823)------------------------------
% (2355823)------------------------------
% (2355822)Success in time 0.154 s
% Vampire exiting

% END OF SYSTEM OUTPUT
% RESULT: SOT_juffGX - Vampire-SAT---4.9 says CounterSatisfiable - CPU = 0.02 WC = 0.18 
% OUTPUT: SOT_juffGX - Vampire-SAT---4.9 says Assurance - CPU = 0.02 WC = 0.18