% ott+10_128_av=off:bs=on:gsp=input_only:irw=on:lcm=predicate:lma=on:nm=0:nwc=1:sp=occurrence:urr=on:updr=off:uhcvi=on_4 on CCC012C3CC2CC4N0N5C50
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 20340
% Time elapsed: 0.800 s
% ------------------------------
% ------------------------------
% fmb+10_1_av=off:bce=on:nm=6_1461 on CCC012C3CC2CC4N0N5C50
TRYING [7]
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Finite model building SAT solving

% Memory used [KB]: 121021
% Time elapsed: 190.100 s
% ------------------------------
% ------------------------------
% dis+10_3_add=large:afp=10000:afq=2.0:amm=sco:anc=none:cond=on:fsr=off:gsp=input_only:lma=on:nm=16:nwc=1:sac=on:updr=off_197 on CCC012C3CC2CC4N0N5C50
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 439182
% Time elapsed: 25.800 s
% ------------------------------
% ------------------------------
% dis+1_3_av=off:cond=on:nm=64:newcnf=on:nwc=1_87 on CCC012C3CC2CC4N0N5C50
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 263663
% Time elapsed: 11.500 s
% ------------------------------
% ------------------------------
% ott-3_5_awrs=decay:awrsf=128:afr=on:afp=40000:afq=1.0:amm=off:anc=none:bce=on:cond=fast:lma=on:nm=64:newcnf=on:nwc=1.1:sas=z3:sp=frequency:updr=off_146 on CCC012C3CC2CC4N0N5C50
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 73303
% Time elapsed: 19.100 s
% ------------------------------
% ------------------------------
% ott+2_5_afp=4000:afq=2.0:anc=none:bce=on:fsr=off:gsp=input_only:lma=on:nm=32:nwc=1:sp=reverse_arity_315 on CCC012C3CC2CC4N0N5C50
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Saturation

% Memory used [KB]: 814400
% Time elapsed: 41.100 s
% ------------------------------
% ------------------------------
% fmb+10_1_av=off:bce=on:fmbes=smt:fmbsr=1.4:fde=none:ile=on:updr=off_600 on CCC012C3CC2CC4N0N5C50
TRYING [7]
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Finite model building SAT solving

% Memory used [KB]: 105669
% Time elapsed: 78.200 s
% ------------------------------
% ------------------------------
% fmb+10_1_av=off:bce=on:fmbsr=1.3:nm=2:newcnf=on_1200 on CCC012C3CC2CC4N0N5C50
TRYING [7]
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Finite model building SAT solving

% Memory used [KB]: 116288
% Time elapsed: 156.200 s
% ------------------------------
% ------------------------------
% fmb+10_1_av=off:fmbsr=1.1:updr=off_300 on CCC012C3CC2CC4N0N5C50
TRYING [7]
% Time limit reached!
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Time limit
% Termination phase: Finite model building SAT solving

% Memory used [KB]: 100808
% Time elapsed: 39.200 s
% ------------------------------
% ------------------------------
% fmb+10_1_av=off:fmbsr=1.6_1200 on CCC012C3CC2CC4N0N5C50
TRYING [7]
Finite Model Found!
% SZS status CounterSatisfiable for CCC012C3CC2CC4N0N5C50
% SZS output start FiniteModel for CCC012C3CC2CC4N0N5C50
tff(declare_$i,type,$i:$tType).
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,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,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_i,type,i: $i * $i > $i).
tff(function_i,axiom,
           i(fmb_$i_1,fmb_$i_1) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_2) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_3) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_4) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_5) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_1,fmb_$i_7) = fmb_$i_6
         & i(fmb_$i_2,fmb_$i_1) = fmb_$i_3
         & i(fmb_$i_2,fmb_$i_2) = fmb_$i_6
         & i(fmb_$i_2,fmb_$i_3) = fmb_$i_3
         & i(fmb_$i_2,fmb_$i_4) = fmb_$i_3
         & i(fmb_$i_2,fmb_$i_5) = fmb_$i_6
         & i(fmb_$i_2,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_2,fmb_$i_7) = fmb_$i_3
         & i(fmb_$i_3,fmb_$i_1) = fmb_$i_2
         & i(fmb_$i_3,fmb_$i_2) = fmb_$i_2
         & i(fmb_$i_3,fmb_$i_3) = fmb_$i_6
         & i(fmb_$i_3,fmb_$i_4) = fmb_$i_6
         & i(fmb_$i_3,fmb_$i_5) = fmb_$i_2
         & i(fmb_$i_3,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_3,fmb_$i_7) = fmb_$i_6
         & i(fmb_$i_4,fmb_$i_1) = fmb_$i_5
         & i(fmb_$i_4,fmb_$i_2) = fmb_$i_5
         & i(fmb_$i_4,fmb_$i_3) = fmb_$i_6
         & i(fmb_$i_4,fmb_$i_4) = fmb_$i_6
         & i(fmb_$i_4,fmb_$i_5) = fmb_$i_6
         & i(fmb_$i_4,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_4,fmb_$i_7) = fmb_$i_6
         & i(fmb_$i_5,fmb_$i_1) = fmb_$i_3
         & i(fmb_$i_5,fmb_$i_2) = fmb_$i_6
         & i(fmb_$i_5,fmb_$i_3) = fmb_$i_3
         & i(fmb_$i_5,fmb_$i_4) = fmb_$i_3
         & i(fmb_$i_5,fmb_$i_5) = fmb_$i_6
         & i(fmb_$i_5,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_5,fmb_$i_7) = fmb_$i_3
         & i(fmb_$i_6,fmb_$i_1) = fmb_$i_1
         & i(fmb_$i_6,fmb_$i_2) = fmb_$i_2
         & i(fmb_$i_6,fmb_$i_3) = fmb_$i_7
         & i(fmb_$i_6,fmb_$i_4) = fmb_$i_3
         & i(fmb_$i_6,fmb_$i_5) = fmb_$i_2
         & i(fmb_$i_6,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_6,fmb_$i_7) = fmb_$i_7
         & i(fmb_$i_7,fmb_$i_1) = fmb_$i_5
         & i(fmb_$i_7,fmb_$i_2) = fmb_$i_2
         & i(fmb_$i_7,fmb_$i_3) = fmb_$i_6
         & i(fmb_$i_7,fmb_$i_4) = fmb_$i_6
         & i(fmb_$i_7,fmb_$i_5) = fmb_$i_6
         & i(fmb_$i_7,fmb_$i_6) = fmb_$i_6
         & i(fmb_$i_7,fmb_$i_7) = fmb_$i_6

).

tff(declare_n,type,n: $i > $i).
tff(function_n,axiom,
           n(fmb_$i_1) = fmb_$i_6
         & n(fmb_$i_2) = fmb_$i_4
         & n(fmb_$i_3) = fmb_$i_2
         & n(fmb_$i_4) = fmb_$i_2
         & n(fmb_$i_5) = fmb_$i_4
         & n(fmb_$i_6) = fmb_$i_1
         & n(fmb_$i_7) = fmb_$i_5

).

tff(declare_t,type,t: $i > $o ).
tff(predicate_t,axiom,
           ~t(fmb_$i_1)
         & ~t(fmb_$i_2)
         & ~t(fmb_$i_3)
         & ~t(fmb_$i_4)
         & ~t(fmb_$i_5)
         & t(fmb_$i_6)
         & ~t(fmb_$i_7)

).

% SZS output end FiniteModel for CCC012C3CC2CC4N0N5C50
% ------------------------------
% Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200)
% Termination reason: Satisfiable

% Memory used [KB]: 68570
% Time elapsed: 27.116 s
% ------------------------------
% ------------------------------
% Success in time 604.42 s