% SZS status Satisfiable for TFF_Finite.s % SZS output start FiniteModel for TFF_Finite.s tff(declare_$i,type,$i:$tType). tff(declare_$i1,type,fmb_$i_1:$i). tff(finite_domain,axiom, ! [X:$i] : ( X = fmb_$i_1 ) ). tff(declare_bool,type,$o:$tType). tff(declare_bool1,type,fmb_bool_1:$o). tff(finite_domain,axiom, ! [X:$o] : ( X = fmb_bool_1 ) ). tff(declare_man,type,man:$tType). tff(declare_man1,type,john:man). tff(declare_man2,type,fmb_man_2:man). tff(finite_domain,axiom, ! [X:man] : ( X = john | X = fmb_man_2 ) ). tff(distinct_domain,axiom, john != fmb_man_2 ). tff(declare_grade,type,grade:$tType). tff(declare_grade1,type,a:grade). tff(declare_grade2,type,f:grade). tff(finite_domain,axiom, ! [X:grade] : ( X = a | X = f ) ). tff(distinct_domain,axiom, a != f ). tff(declare_d_man,type,d_man:$tType). tff(declare_d_man1,type,d_john:d_man). tff(declare_d_man2,type,d_gotA:d_man). tff(finite_domain,axiom, ! [X:d_man] : ( X = d_john | X = d_gotA ) ). tff(distinct_domain,axiom, d_john != d_gotA ). tff(declare_d_grade,type,d_grade:$tType). tff(declare_d_grade1,type,d_a:d_grade). tff(declare_d_grade2,type,d_f:d_grade). tff(finite_domain,axiom, ! [X:d_grade] : ( X = d_a | X = d_f ) ). tff(distinct_domain,axiom, d_a != d_f ). tff(declare_grade_of,type,grade_of: man > grade). tff(function_grade_of,axiom, grade_of(john) = f & grade_of(fmb_man_2) = a ). tff(declare_d2man,type,d2man: d_man > man). tff(function_d2man,axiom, d2man(d_john) = john & d2man(d_gotA) = fmb_man_2 ). tff(declare_d2grade,type,d2grade: d_grade > grade). tff(function_d2grade,axiom, d2grade(d_a) = a & d2grade(d_f) = f ). tff(declare_created_equal,type,created_equal: man * man > $o ). tff(predicate_created_equal,axiom, % created_equal(john,john) undefined in model % created_equal(john,fmb_man_2) undefined in model % created_equal(fmb_man_2,john) undefined in model % created_equal(fmb_man_2,fmb_man_2) undefined in model ). % SZS output end FiniteModel for TFF_Finite.s