%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP322_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 11:39:21 AM UTC 2026
% Result : Satisfiable 7.91s 2.40s
% Output : FiniteModel 7.91s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] : ( X = 'fmb_$i_1' ) ).
tff('declare_B_bool_fun_b_bool_fun_fun$',type,
'B_bool_fun_b_bool_fun_fun$': $tType ).
tff('declare_B_bool_fun_b_bool_fun_fun$1',type,
'fmb_B_bool_fun_b_bool_fun_fun$_1': 'B_bool_fun_b_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_fun$2',type,
'fmb_B_bool_fun_b_bool_fun_fun$_2': 'B_bool_fun_b_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_fun$3',type,
'fmb_B_bool_fun_b_bool_fun_fun$_3': 'B_bool_fun_b_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_fun$4',type,
'fmb_B_bool_fun_b_bool_fun_fun$_4': 'B_bool_fun_b_bool_fun_fun$' ).
tff('finite_domain_B_bool_fun_b_bool_fun_fun$',axiom,
! [X: 'B_bool_fun_b_bool_fun_fun$'] :
( ( X = 'fmb_B_bool_fun_b_bool_fun_fun$_1' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_fun$_2' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_fun$_3' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_B_bool_fun_b_bool_fun_fun$',axiom,
( ( 'fmb_B_bool_fun_b_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_fun$_2' )
& ( 'fmb_B_bool_fun_b_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_fun$_3' != 'fmb_B_bool_fun_b_bool_fun_fun$_4' ) ) ).
tff('declare_B_bool_fun_b_bool_fun_bool_fun_fun$',type,
'B_bool_fun_b_bool_fun_bool_fun_fun$': $tType ).
tff('declare_B_bool_fun_b_bool_fun_bool_fun_fun$1',type,
'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_bool_fun_fun$2',type,
'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_bool_fun_fun$3',type,
'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_bool_fun_fun$4',type,
'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('finite_domain_B_bool_fun_b_bool_fun_bool_fun_fun$',axiom,
! [X: 'B_bool_fun_b_bool_fun_bool_fun_fun$'] :
( ( X = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_B_bool_fun_b_bool_fun_bool_fun_fun$',axiom,
( ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2' )
& ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3' != 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4' ) ) ).
tff('declare_B_bool_fun_bool_fun$',type,
'B_bool_fun_bool_fun$': $tType ).
tff('declare_B_bool_fun_bool_fun$1',type,
'fmb_B_bool_fun_bool_fun$_1': 'B_bool_fun_bool_fun$' ).
tff('declare_B_bool_fun_bool_fun$2',type,
'fmb_B_bool_fun_bool_fun$_2': 'B_bool_fun_bool_fun$' ).
tff('declare_B_bool_fun_bool_fun$3',type,
'fmb_B_bool_fun_bool_fun$_3': 'B_bool_fun_bool_fun$' ).
tff('declare_B_bool_fun_bool_fun$4',type,
'fmb_B_bool_fun_bool_fun$_4': 'B_bool_fun_bool_fun$' ).
tff('finite_domain_B_bool_fun_bool_fun$',axiom,
! [X: 'B_bool_fun_bool_fun$'] :
( ( X = 'fmb_B_bool_fun_bool_fun$_1' )
| ( X = 'fmb_B_bool_fun_bool_fun$_2' )
| ( X = 'fmb_B_bool_fun_bool_fun$_3' )
| ( X = 'fmb_B_bool_fun_bool_fun$_4' ) ) ).
tff('distinct_domain_B_bool_fun_bool_fun$',axiom,
( ( 'fmb_B_bool_fun_bool_fun$_1' != 'fmb_B_bool_fun_bool_fun$_2' )
& ( 'fmb_B_bool_fun_bool_fun$_1' != 'fmb_B_bool_fun_bool_fun$_3' )
& ( 'fmb_B_bool_fun_bool_fun$_1' != 'fmb_B_bool_fun_bool_fun$_4' )
& ( 'fmb_B_bool_fun_bool_fun$_2' != 'fmb_B_bool_fun_bool_fun$_3' )
& ( 'fmb_B_bool_fun_bool_fun$_2' != 'fmb_B_bool_fun_bool_fun$_4' )
& ( 'fmb_B_bool_fun_bool_fun$_3' != 'fmb_B_bool_fun_bool_fun$_4' ) ) ).
tff('declare_B$',type,
'B$': $tType ).
tff('declare_B$1',type,
'fmb_B$_1': 'B$' ).
tff('finite_domain_B$',axiom,
! [X: 'B$'] : ( X = 'fmb_B$_1' ) ).
tff('declare_B_bool_fun_b_set_fun$',type,
'B_bool_fun_b_set_fun$': $tType ).
tff('declare_B_bool_fun_b_set_fun$1',type,
'fmb_B_bool_fun_b_set_fun$_1': 'B_bool_fun_b_set_fun$' ).
tff('declare_B_bool_fun_b_set_fun$2',type,
'fmb_B_bool_fun_b_set_fun$_2': 'B_bool_fun_b_set_fun$' ).
tff('declare_B_bool_fun_b_set_fun$3',type,
'fmb_B_bool_fun_b_set_fun$_3': 'B_bool_fun_b_set_fun$' ).
tff('declare_B_bool_fun_b_set_fun$4',type,
'fmb_B_bool_fun_b_set_fun$_4': 'B_bool_fun_b_set_fun$' ).
tff('finite_domain_B_bool_fun_b_set_fun$',axiom,
! [X: 'B_bool_fun_b_set_fun$'] :
( ( X = 'fmb_B_bool_fun_b_set_fun$_1' )
| ( X = 'fmb_B_bool_fun_b_set_fun$_2' )
| ( X = 'fmb_B_bool_fun_b_set_fun$_3' )
| ( X = 'fmb_B_bool_fun_b_set_fun$_4' ) ) ).
tff('distinct_domain_B_bool_fun_b_set_fun$',axiom,
( ( 'fmb_B_bool_fun_b_set_fun$_1' != 'fmb_B_bool_fun_b_set_fun$_2' )
& ( 'fmb_B_bool_fun_b_set_fun$_1' != 'fmb_B_bool_fun_b_set_fun$_3' )
& ( 'fmb_B_bool_fun_b_set_fun$_1' != 'fmb_B_bool_fun_b_set_fun$_4' )
& ( 'fmb_B_bool_fun_b_set_fun$_2' != 'fmb_B_bool_fun_b_set_fun$_3' )
& ( 'fmb_B_bool_fun_b_set_fun$_2' != 'fmb_B_bool_fun_b_set_fun$_4' )
& ( 'fmb_B_bool_fun_b_set_fun$_3' != 'fmb_B_bool_fun_b_set_fun$_4' ) ) ).
tff('declare_B_set_b_set_bool_fun_fun$',type,
'B_set_b_set_bool_fun_fun$': $tType ).
tff('declare_B_set_b_set_bool_fun_fun$1',type,
'fmb_B_set_b_set_bool_fun_fun$_1': 'B_set_b_set_bool_fun_fun$' ).
tff('declare_B_set_b_set_bool_fun_fun$2',type,
'fmb_B_set_b_set_bool_fun_fun$_2': 'B_set_b_set_bool_fun_fun$' ).
tff('declare_B_set_b_set_bool_fun_fun$3',type,
'fmb_B_set_b_set_bool_fun_fun$_3': 'B_set_b_set_bool_fun_fun$' ).
tff('declare_B_set_b_set_bool_fun_fun$4',type,
'fmb_B_set_b_set_bool_fun_fun$_4': 'B_set_b_set_bool_fun_fun$' ).
tff('finite_domain_B_set_b_set_bool_fun_fun$',axiom,
! [X: 'B_set_b_set_bool_fun_fun$'] :
( ( X = 'fmb_B_set_b_set_bool_fun_fun$_1' )
| ( X = 'fmb_B_set_b_set_bool_fun_fun$_2' )
| ( X = 'fmb_B_set_b_set_bool_fun_fun$_3' )
| ( X = 'fmb_B_set_b_set_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_B_set_b_set_bool_fun_fun$',axiom,
( ( 'fmb_B_set_b_set_bool_fun_fun$_1' != 'fmb_B_set_b_set_bool_fun_fun$_2' )
& ( 'fmb_B_set_b_set_bool_fun_fun$_1' != 'fmb_B_set_b_set_bool_fun_fun$_3' )
& ( 'fmb_B_set_b_set_bool_fun_fun$_1' != 'fmb_B_set_b_set_bool_fun_fun$_4' )
& ( 'fmb_B_set_b_set_bool_fun_fun$_2' != 'fmb_B_set_b_set_bool_fun_fun$_3' )
& ( 'fmb_B_set_b_set_bool_fun_fun$_2' != 'fmb_B_set_b_set_bool_fun_fun$_4' )
& ( 'fmb_B_set_b_set_bool_fun_fun$_3' != 'fmb_B_set_b_set_bool_fun_fun$_4' ) ) ).
tff('declare_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$',type,
'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$': $tType ).
tff('declare_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$1',type,
'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$2',type,
'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$3',type,
'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('declare_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$4',type,
'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('finite_domain_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$',axiom,
! [X: 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$'] :
( ( X = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3' )
| ( X = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4' ) ) ).
tff('distinct_domain_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$',axiom,
( ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2' )
& ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3' )
& ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4' )
& ( 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3' != 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4' ) ) ).
tff(declare_tlbool,type,
tlbool: $tType ).
tff(declare_tlbool1,type,
fmb_tlbool_1: tlbool ).
tff(declare_tlbool2,type,
fmb_tlbool_2: tlbool ).
tff(finite_domain_tlbool,axiom,
! [X: tlbool] :
( ( X = fmb_tlbool_1 )
| ( X = fmb_tlbool_2 ) ) ).
tff(distinct_domain_tlbool,axiom,
fmb_tlbool_1 != fmb_tlbool_2 ).
tff('declare_B_set_b_set_b_set_fun_fun$',type,
'B_set_b_set_b_set_fun_fun$': $tType ).
tff('declare_B_set_b_set_b_set_fun_fun$1',type,
'fmb_B_set_b_set_b_set_fun_fun$_1': 'B_set_b_set_b_set_fun_fun$' ).
tff('declare_B_set_b_set_b_set_fun_fun$2',type,
'fmb_B_set_b_set_b_set_fun_fun$_2': 'B_set_b_set_b_set_fun_fun$' ).
tff('declare_B_set_b_set_b_set_fun_fun$3',type,
'fmb_B_set_b_set_b_set_fun_fun$_3': 'B_set_b_set_b_set_fun_fun$' ).
tff('declare_B_set_b_set_b_set_fun_fun$4',type,
'fmb_B_set_b_set_b_set_fun_fun$_4': 'B_set_b_set_b_set_fun_fun$' ).
tff('finite_domain_B_set_b_set_b_set_fun_fun$',axiom,
! [X: 'B_set_b_set_b_set_fun_fun$'] :
( ( X = 'fmb_B_set_b_set_b_set_fun_fun$_1' )
| ( X = 'fmb_B_set_b_set_b_set_fun_fun$_2' )
| ( X = 'fmb_B_set_b_set_b_set_fun_fun$_3' )
| ( X = 'fmb_B_set_b_set_b_set_fun_fun$_4' ) ) ).
tff('distinct_domain_B_set_b_set_b_set_fun_fun$',axiom,
( ( 'fmb_B_set_b_set_b_set_fun_fun$_1' != 'fmb_B_set_b_set_b_set_fun_fun$_2' )
& ( 'fmb_B_set_b_set_b_set_fun_fun$_1' != 'fmb_B_set_b_set_b_set_fun_fun$_3' )
& ( 'fmb_B_set_b_set_b_set_fun_fun$_1' != 'fmb_B_set_b_set_b_set_fun_fun$_4' )
& ( 'fmb_B_set_b_set_b_set_fun_fun$_2' != 'fmb_B_set_b_set_b_set_fun_fun$_3' )
& ( 'fmb_B_set_b_set_b_set_fun_fun$_2' != 'fmb_B_set_b_set_b_set_fun_fun$_4' )
& ( 'fmb_B_set_b_set_b_set_fun_fun$_3' != 'fmb_B_set_b_set_b_set_fun_fun$_4' ) ) ).
tff('declare_B_b_bool_fun_fun$',type,
'B_b_bool_fun_fun$': $tType ).
tff('declare_B_b_bool_fun_fun$1',type,
'fmb_B_b_bool_fun_fun$_1': 'B_b_bool_fun_fun$' ).
tff('declare_B_b_bool_fun_fun$2',type,
'fmb_B_b_bool_fun_fun$_2': 'B_b_bool_fun_fun$' ).
tff('declare_B_b_bool_fun_fun$3',type,
'fmb_B_b_bool_fun_fun$_3': 'B_b_bool_fun_fun$' ).
tff('declare_B_b_bool_fun_fun$4',type,
'fmb_B_b_bool_fun_fun$_4': 'B_b_bool_fun_fun$' ).
tff('finite_domain_B_b_bool_fun_fun$',axiom,
! [X: 'B_b_bool_fun_fun$'] :
( ( X = 'fmb_B_b_bool_fun_fun$_1' )
| ( X = 'fmb_B_b_bool_fun_fun$_2' )
| ( X = 'fmb_B_b_bool_fun_fun$_3' )
| ( X = 'fmb_B_b_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_B_b_bool_fun_fun$',axiom,
( ( 'fmb_B_b_bool_fun_fun$_1' != 'fmb_B_b_bool_fun_fun$_2' )
& ( 'fmb_B_b_bool_fun_fun$_1' != 'fmb_B_b_bool_fun_fun$_3' )
& ( 'fmb_B_b_bool_fun_fun$_1' != 'fmb_B_b_bool_fun_fun$_4' )
& ( 'fmb_B_b_bool_fun_fun$_2' != 'fmb_B_b_bool_fun_fun$_3' )
& ( 'fmb_B_b_bool_fun_fun$_2' != 'fmb_B_b_bool_fun_fun$_4' )
& ( 'fmb_B_b_bool_fun_fun$_3' != 'fmb_B_b_bool_fun_fun$_4' ) ) ).
tff('declare_B_set$',type,
'B_set$': $tType ).
tff('declare_B_set$1',type,
'fmb_B_set$_1': 'B_set$' ).
tff('declare_B_set$2',type,
'fmb_B_set$_2': 'B_set$' ).
tff('finite_domain_B_set$',axiom,
! [X: 'B_set$'] :
( ( X = 'fmb_B_set$_1' )
| ( X = 'fmb_B_set$_2' ) ) ).
tff('distinct_domain_B_set$',axiom,
'fmb_B_set$_1' != 'fmb_B_set$_2' ).
tff('declare_B_set_b_bool_fun_fun$',type,
'B_set_b_bool_fun_fun$': $tType ).
tff('declare_B_set_b_bool_fun_fun$1',type,
'fmb_B_set_b_bool_fun_fun$_1': 'B_set_b_bool_fun_fun$' ).
tff('declare_B_set_b_bool_fun_fun$2',type,
'fmb_B_set_b_bool_fun_fun$_2': 'B_set_b_bool_fun_fun$' ).
tff('declare_B_set_b_bool_fun_fun$3',type,
'fmb_B_set_b_bool_fun_fun$_3': 'B_set_b_bool_fun_fun$' ).
tff('declare_B_set_b_bool_fun_fun$4',type,
'fmb_B_set_b_bool_fun_fun$_4': 'B_set_b_bool_fun_fun$' ).
tff('finite_domain_B_set_b_bool_fun_fun$',axiom,
! [X: 'B_set_b_bool_fun_fun$'] :
( ( X = 'fmb_B_set_b_bool_fun_fun$_1' )
| ( X = 'fmb_B_set_b_bool_fun_fun$_2' )
| ( X = 'fmb_B_set_b_bool_fun_fun$_3' )
| ( X = 'fmb_B_set_b_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_B_set_b_bool_fun_fun$',axiom,
( ( 'fmb_B_set_b_bool_fun_fun$_1' != 'fmb_B_set_b_bool_fun_fun$_2' )
& ( 'fmb_B_set_b_bool_fun_fun$_1' != 'fmb_B_set_b_bool_fun_fun$_3' )
& ( 'fmb_B_set_b_bool_fun_fun$_1' != 'fmb_B_set_b_bool_fun_fun$_4' )
& ( 'fmb_B_set_b_bool_fun_fun$_2' != 'fmb_B_set_b_bool_fun_fun$_3' )
& ( 'fmb_B_set_b_bool_fun_fun$_2' != 'fmb_B_set_b_bool_fun_fun$_4' )
& ( 'fmb_B_set_b_bool_fun_fun$_3' != 'fmb_B_set_b_bool_fun_fun$_4' ) ) ).
tff('declare_B_set_bool_fun$',type,
'B_set_bool_fun$': $tType ).
tff('declare_B_set_bool_fun$1',type,
'fmb_B_set_bool_fun$_1': 'B_set_bool_fun$' ).
tff('declare_B_set_bool_fun$2',type,
'fmb_B_set_bool_fun$_2': 'B_set_bool_fun$' ).
tff('declare_B_set_bool_fun$3',type,
'fmb_B_set_bool_fun$_3': 'B_set_bool_fun$' ).
tff('declare_B_set_bool_fun$4',type,
'fmb_B_set_bool_fun$_4': 'B_set_bool_fun$' ).
tff('finite_domain_B_set_bool_fun$',axiom,
! [X: 'B_set_bool_fun$'] :
( ( X = 'fmb_B_set_bool_fun$_1' )
| ( X = 'fmb_B_set_bool_fun$_2' )
| ( X = 'fmb_B_set_bool_fun$_3' )
| ( X = 'fmb_B_set_bool_fun$_4' ) ) ).
tff('distinct_domain_B_set_bool_fun$',axiom,
( ( 'fmb_B_set_bool_fun$_1' != 'fmb_B_set_bool_fun$_2' )
& ( 'fmb_B_set_bool_fun$_1' != 'fmb_B_set_bool_fun$_3' )
& ( 'fmb_B_set_bool_fun$_1' != 'fmb_B_set_bool_fun$_4' )
& ( 'fmb_B_set_bool_fun$_2' != 'fmb_B_set_bool_fun$_3' )
& ( 'fmb_B_set_bool_fun$_2' != 'fmb_B_set_bool_fun$_4' )
& ( 'fmb_B_set_bool_fun$_3' != 'fmb_B_set_bool_fun$_4' ) ) ).
tff('declare_Bool_bool_fun$',type,
'Bool_bool_fun$': $tType ).
tff('declare_Bool_bool_fun$1',type,
'fmb_Bool_bool_fun$_1': 'Bool_bool_fun$' ).
tff('declare_Bool_bool_fun$2',type,
'fmb_Bool_bool_fun$_2': 'Bool_bool_fun$' ).
tff('declare_Bool_bool_fun$3',type,
'fmb_Bool_bool_fun$_3': 'Bool_bool_fun$' ).
tff('declare_Bool_bool_fun$4',type,
'fmb_Bool_bool_fun$_4': 'Bool_bool_fun$' ).
tff('finite_domain_Bool_bool_fun$',axiom,
! [X: 'Bool_bool_fun$'] :
( ( X = 'fmb_Bool_bool_fun$_1' )
| ( X = 'fmb_Bool_bool_fun$_2' )
| ( X = 'fmb_Bool_bool_fun$_3' )
| ( X = 'fmb_Bool_bool_fun$_4' ) ) ).
tff('distinct_domain_Bool_bool_fun$',axiom,
( ( 'fmb_Bool_bool_fun$_1' != 'fmb_Bool_bool_fun$_2' )
& ( 'fmb_Bool_bool_fun$_1' != 'fmb_Bool_bool_fun$_3' )
& ( 'fmb_Bool_bool_fun$_1' != 'fmb_Bool_bool_fun$_4' )
& ( 'fmb_Bool_bool_fun$_2' != 'fmb_Bool_bool_fun$_3' )
& ( 'fmb_Bool_bool_fun$_2' != 'fmb_Bool_bool_fun$_4' )
& ( 'fmb_Bool_bool_fun$_3' != 'fmb_Bool_bool_fun$_4' ) ) ).
tff('declare_B_set_b_set_fun$',type,
'B_set_b_set_fun$': $tType ).
tff('declare_B_set_b_set_fun$1',type,
'fmb_B_set_b_set_fun$_1': 'B_set_b_set_fun$' ).
tff('declare_B_set_b_set_fun$2',type,
'fmb_B_set_b_set_fun$_2': 'B_set_b_set_fun$' ).
tff('declare_B_set_b_set_fun$3',type,
'fmb_B_set_b_set_fun$_3': 'B_set_b_set_fun$' ).
tff('declare_B_set_b_set_fun$4',type,
'fmb_B_set_b_set_fun$_4': 'B_set_b_set_fun$' ).
tff('finite_domain_B_set_b_set_fun$',axiom,
! [X: 'B_set_b_set_fun$'] :
( ( X = 'fmb_B_set_b_set_fun$_1' )
| ( X = 'fmb_B_set_b_set_fun$_2' )
| ( X = 'fmb_B_set_b_set_fun$_3' )
| ( X = 'fmb_B_set_b_set_fun$_4' ) ) ).
tff('distinct_domain_B_set_b_set_fun$',axiom,
( ( 'fmb_B_set_b_set_fun$_1' != 'fmb_B_set_b_set_fun$_2' )
& ( 'fmb_B_set_b_set_fun$_1' != 'fmb_B_set_b_set_fun$_3' )
& ( 'fmb_B_set_b_set_fun$_1' != 'fmb_B_set_b_set_fun$_4' )
& ( 'fmb_B_set_b_set_fun$_2' != 'fmb_B_set_b_set_fun$_3' )
& ( 'fmb_B_set_b_set_fun$_2' != 'fmb_B_set_b_set_fun$_4' )
& ( 'fmb_B_set_b_set_fun$_3' != 'fmb_B_set_b_set_fun$_4' ) ) ).
tff('declare_B_bool_fun$',type,
'B_bool_fun$': $tType ).
tff('declare_B_bool_fun$1',type,
'fmb_B_bool_fun$_1': 'B_bool_fun$' ).
tff('declare_B_bool_fun$2',type,
'fmb_B_bool_fun$_2': 'B_bool_fun$' ).
tff('finite_domain_B_bool_fun$',axiom,
! [X: 'B_bool_fun$'] :
( ( X = 'fmb_B_bool_fun$_1' )
| ( X = 'fmb_B_bool_fun$_2' ) ) ).
tff('distinct_domain_B_bool_fun$',axiom,
'fmb_B_bool_fun$_1' != 'fmb_B_bool_fun$_2' ).
tff('declare_Bool_bool_bool_fun_fun$',type,
'Bool_bool_bool_fun_fun$': $tType ).
tff('declare_Bool_bool_bool_fun_fun$1',type,
'fmb_Bool_bool_bool_fun_fun$_1': 'Bool_bool_bool_fun_fun$' ).
tff('declare_Bool_bool_bool_fun_fun$2',type,
'fmb_Bool_bool_bool_fun_fun$_2': 'Bool_bool_bool_fun_fun$' ).
tff('declare_Bool_bool_bool_fun_fun$3',type,
'fmb_Bool_bool_bool_fun_fun$_3': 'Bool_bool_bool_fun_fun$' ).
tff('declare_Bool_bool_bool_fun_fun$4',type,
'fmb_Bool_bool_bool_fun_fun$_4': 'Bool_bool_bool_fun_fun$' ).
tff('finite_domain_Bool_bool_bool_fun_fun$',axiom,
! [X: 'Bool_bool_bool_fun_fun$'] :
( ( X = 'fmb_Bool_bool_bool_fun_fun$_1' )
| ( X = 'fmb_Bool_bool_bool_fun_fun$_2' )
| ( X = 'fmb_Bool_bool_bool_fun_fun$_3' )
| ( X = 'fmb_Bool_bool_bool_fun_fun$_4' ) ) ).
tff('distinct_domain_Bool_bool_bool_fun_fun$',axiom,
( ( 'fmb_Bool_bool_bool_fun_fun$_1' != 'fmb_Bool_bool_bool_fun_fun$_2' )
& ( 'fmb_Bool_bool_bool_fun_fun$_1' != 'fmb_Bool_bool_bool_fun_fun$_3' )
& ( 'fmb_Bool_bool_bool_fun_fun$_1' != 'fmb_Bool_bool_bool_fun_fun$_4' )
& ( 'fmb_Bool_bool_bool_fun_fun$_2' != 'fmb_Bool_bool_bool_fun_fun$_3' )
& ( 'fmb_Bool_bool_bool_fun_fun$_2' != 'fmb_Bool_bool_bool_fun_fun$_4' )
& ( 'fmb_Bool_bool_bool_fun_fun$_3' != 'fmb_Bool_bool_bool_fun_fun$_4' ) ) ).
tff(declare_def_12,type,
def_12: tlbool ).
tff(def_12_definition,axiom,
def_12 = fmb_tlbool_1 ).
tff(declare_def_17,type,
def_17: tlbool ).
tff(def_17_definition,axiom,
def_17 = fmb_tlbool_1 ).
tff('declare_less_eq$a',type,
'less_eq$a': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('less_eq$a_definition',axiom,
'less_eq$a' = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1' ).
tff('declare_a$',type,
'a$': 'B$' ).
tff('a$_definition',axiom,
'a$' = 'fmb_B$_1' ).
tff(declare_def_6,type,
def_6: tlbool ).
tff(def_6_definition,axiom,
def_6 = fmb_tlbool_1 ).
tff('declare_collect$',type,
'collect$': 'B_bool_fun_b_set_fun$' ).
tff('collect$_definition',axiom,
'collect$' = 'fmb_B_bool_fun_b_set_fun$_1' ).
tff(declare_def_29,type,
def_29: tlbool ).
tff(def_29_definition,axiom,
def_29 = fmb_tlbool_1 ).
tff(declare_def_4,type,
def_4: tlbool ).
tff(def_4_definition,axiom,
def_4 = fmb_tlbool_2 ).
tff(declare_def_5,type,
def_5: tlbool ).
tff(def_5_definition,axiom,
def_5 = fmb_tlbool_1 ).
tff('declare_top$b',type,
'top$b': 'B_bool_fun$' ).
tff('top$b_definition',axiom,
'top$b' = 'fmb_B_bool_fun$_1' ).
tff(declare_def_32,type,
def_32: tlbool ).
tff(def_32_definition,axiom,
def_32 = fmb_tlbool_2 ).
tff('declare_uminus$',type,
'uminus$': 'B_set_b_set_fun$' ).
tff('uminus$_definition',axiom,
'uminus$' = 'fmb_B_set_b_set_fun$_1' ).
tff(declare_def_3,type,
def_3: tlbool ).
tff(def_3_definition,axiom,
def_3 = fmb_tlbool_2 ).
tff('declare_top$',type,
'top$': 'B_set$' ).
tff('top$_definition',axiom,
'top$' = 'fmb_B_set$_1' ).
tff(declare_tltrue,type,
tltrue: tlbool ).
tff(tltrue_definition,axiom,
tltrue = fmb_tlbool_2 ).
tff('declare_inf$',type,
'inf$': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('inf$_definition',axiom,
'inf$' = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1' ).
tff('declare_minus$',type,
'minus$': 'B_set_b_set_b_set_fun_fun$' ).
tff('minus$_definition',axiom,
'minus$' = 'fmb_B_set_b_set_b_set_fun_fun$_1' ).
tff(declare_def_18,type,
def_18: tlbool ).
tff(def_18_definition,axiom,
def_18 = fmb_tlbool_1 ).
tff(declare_def_2,type,
def_2: tlbool ).
tff(def_2_definition,axiom,
def_2 = fmb_tlbool_2 ).
tff('declare_less$',type,
'less$': 'B_set_b_set_bool_fun_fun$' ).
tff('less$_definition',axiom,
'less$' = 'fmb_B_set_b_set_bool_fun_fun$_1' ).
tff('declare_sup$b',type,
'sup$b': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('sup$b_definition',axiom,
'sup$b' = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2' ).
tff(declare_def_27,type,
def_27: tlbool ).
tff(def_27_definition,axiom,
def_27 = fmb_tlbool_1 ).
tff('declare_sup$',type,
'sup$': 'B_set_b_set_b_set_fun_fun$' ).
tff('sup$_definition',axiom,
'sup$' = 'fmb_B_set_b_set_b_set_fun_fun$_2' ).
tff(declare_def_34,type,
def_34: tlbool ).
tff(def_34_definition,axiom,
def_34 = fmb_tlbool_2 ).
tff('declare_uu$',type,
'uu$': 'B_set_b_bool_fun_fun$' ).
tff('uu$_definition',axiom,
'uu$' = 'fmb_B_set_b_bool_fun_fun$_1' ).
tff(declare_def_1,type,
def_1: tlbool ).
tff(def_1_definition,axiom,
def_1 = fmb_tlbool_2 ).
tff('declare_uminus$a',type,
'uminus$a': 'B_bool_fun_b_bool_fun_fun$' ).
tff('uminus$a_definition',axiom,
'uminus$a' = 'fmb_B_bool_fun_b_bool_fun_fun$_1' ).
tff('declare_bot$b',type,
'bot$b': 'B_bool_fun$' ).
tff('bot$b_definition',axiom,
'bot$b' = 'fmb_B_bool_fun$_2' ).
tff(declare_def_7,type,
def_7: tlbool ).
tff(def_7_definition,axiom,
def_7 = fmb_tlbool_1 ).
tff('declare_minus$a',type,
'minus$a': 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' ).
tff('minus$a_definition',axiom,
'minus$a' = 'fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3' ).
tff(declare_tlfalse,type,
tlfalse: tlbool ).
tff(tlfalse_definition,axiom,
tlfalse = fmb_tlbool_1 ).
tff('declare_inf$a',type,
'inf$a': 'B_set_b_set_b_set_fun_fun$' ).
tff('inf$a_definition',axiom,
'inf$a' = 'fmb_B_set_b_set_b_set_fun_fun$_3' ).
tff(declare_def_31,type,
def_31: tlbool ).
tff(def_31_definition,axiom,
def_31 = fmb_tlbool_2 ).
tff(declare_def_28,type,
def_28: tlbool ).
tff(def_28_definition,axiom,
def_28 = fmb_tlbool_1 ).
tff('declare_bot$',type,
'bot$': 'B_set$' ).
tff('bot$_definition',axiom,
'bot$' = 'fmb_B_set$_2' ).
tff(declare_def_30,type,
def_30: tlbool ).
tff(def_30_definition,axiom,
def_30 = fmb_tlbool_2 ).
tff('declare_b$',type,
'b$': 'B$' ).
tff('b$_definition',axiom,
'b$' = 'fmb_B$_1' ).
tff('declare_less$a',type,
'less$a': 'B_bool_fun_b_bool_fun_bool_fun_fun$' ).
tff('less$a_definition',axiom,
'less$a' = 'fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2' ).
tff('declare_less_eq$',type,
'less_eq$': 'B_set_b_set_bool_fun_fun$' ).
tff('less_eq$_definition',axiom,
'less_eq$' = 'fmb_B_set_b_set_bool_fun_fun$_2' ).
tff(declare_def_35,type,
def_35: tlbool ).
tff(def_35_definition,axiom,
def_35 = fmb_tlbool_1 ).
tff('declare_sup$a',type,
'sup$a': 'Bool_bool_bool_fun_fun$' ).
tff('sup$a_definition',axiom,
'sup$a' = 'fmb_Bool_bool_bool_fun_fun$_1' ).
tff(declare_def_33,type,
def_33: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_33,axiom,
( ( def_33('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_33('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_15,type,
def_15: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_15,axiom,
( ( def_15('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_15('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_39,type,
def_39: tlbool > tlbool ).
tff(function_def_39,axiom,
( ( def_39(fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_39(fmb_tlbool_2) = fmb_tlbool_1 ) ) ).
tff('declare_fun_app$b',type,
'fun_app$b': ( 'B_set_b_set_fun$' * 'B_set$' ) > 'B_set$' ).
tff('function_fun_app$b',axiom,
( ( 'fun_app$b'('fmb_B_set_b_set_fun$_1','fmb_B_set$_1') = 'fmb_B_set$_2' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_1','fmb_B_set$_2') = 'fmb_B_set$_1' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_2','fmb_B_set$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_2','fmb_B_set$_2') = 'fmb_B_set$_2' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_3','fmb_B_set$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_3','fmb_B_set$_2') = 'fmb_B_set$_1' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_4','fmb_B_set$_1') = 'fmb_B_set$_2' )
& ( 'fun_app$b'('fmb_B_set_b_set_fun$_4','fmb_B_set$_2') = 'fmb_B_set$_2' ) ) ).
tff(declare_def_36,type,
def_36: tlbool > tlbool ).
tff(function_def_36,axiom,
( ( def_36(fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_36(fmb_tlbool_2) = fmb_tlbool_1 ) ) ).
tff(declare_def_21,type,
def_21: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_21,axiom,
( ( def_21('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_21('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_8,type,
def_8: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_8,axiom,
( ( def_8('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_8('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff('declare_fun_app$j',type,
'fun_app$j': ( 'B_set_b_set_bool_fun_fun$' * 'B_set$' ) > 'B_set_bool_fun$' ).
tff('function_fun_app$j',axiom,
( ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1') = 'fmb_B_set_bool_fun$_4' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2') = 'fmb_B_set_bool_fun$_3' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1') = 'fmb_B_set_bool_fun$_2' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2') = 'fmb_B_set_bool_fun$_1' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1') = 'fmb_B_set_bool_fun$_4' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2') = 'fmb_B_set_bool_fun$_3' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1') = 'fmb_B_set_bool_fun$_4' )
& ( 'fun_app$j'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2') = 'fmb_B_set_bool_fun$_3' ) ) ).
tff('declare_fun_app$f',type,
'fun_app$f': ( 'Bool_bool_bool_fun_fun$' * tlbool ) > 'Bool_bool_fun$' ).
tff('function_fun_app$f',axiom,
( ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_1',fmb_tlbool_1) = 'fmb_Bool_bool_fun$_2' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_1',fmb_tlbool_2) = 'fmb_Bool_bool_fun$_1' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_2',fmb_tlbool_1) = 'fmb_Bool_bool_fun$_2' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_2',fmb_tlbool_2) = 'fmb_Bool_bool_fun$_1' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_3',fmb_tlbool_1) = 'fmb_Bool_bool_fun$_2' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_3',fmb_tlbool_2) = 'fmb_Bool_bool_fun$_1' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_4',fmb_tlbool_1) = 'fmb_Bool_bool_fun$_2' )
& ( 'fun_app$f'('fmb_Bool_bool_bool_fun_fun$_4',fmb_tlbool_2) = 'fmb_Bool_bool_fun$_1' ) ) ).
tff('declare_fun_app$a',type,
'fun_app$a': ( 'B_set_b_bool_fun_fun$' * 'B_set$' ) > 'B_bool_fun$' ).
tff('function_fun_app$a',axiom,
( ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_1','fmb_B_set$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_1','fmb_B_set$_2') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_2','fmb_B_set$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_2','fmb_B_set$_2') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_3','fmb_B_set$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_3','fmb_B_set$_2') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_4','fmb_B_set$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$a'('fmb_B_set_b_bool_fun_fun$_4','fmb_B_set$_2') = 'fmb_B_bool_fun$_2' ) ) ).
tff('declare_fun_app$c',type,
'fun_app$c': ( 'B_set_b_set_b_set_fun_fun$' * 'B_set$' ) > 'B_set_b_set_fun$' ).
tff('function_fun_app$c',axiom,
( ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_1','fmb_B_set$_1') = 'fmb_B_set_b_set_fun$_1' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_1','fmb_B_set$_2') = 'fmb_B_set_b_set_fun$_4' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_2','fmb_B_set$_1') = 'fmb_B_set_b_set_fun$_3' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_2','fmb_B_set$_2') = 'fmb_B_set_b_set_fun$_2' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_3','fmb_B_set$_1') = 'fmb_B_set_b_set_fun$_2' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_3','fmb_B_set$_2') = 'fmb_B_set_b_set_fun$_4' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_4','fmb_B_set$_1') = 'fmb_B_set_b_set_fun$_1' )
& ( 'fun_app$c'('fmb_B_set_b_set_b_set_fun_fun$_4','fmb_B_set$_2') = 'fmb_B_set_b_set_fun$_4' ) ) ).
tff(declare_def_22,type,
def_22: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_22,axiom,
( ( def_22('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_22('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_40,type,
def_40: tlbool > tlbool ).
tff(function_def_40,axiom,
( ( def_40(fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_40(fmb_tlbool_2) = fmb_tlbool_1 ) ) ).
tff('declare_insert$',type,
'insert$': 'B$' > 'B_set_b_set_fun$' ).
tff('function_insert$',axiom,
'insert$'('fmb_B$_1') = 'fmb_B_set_b_set_fun$_3' ).
tff('declare_fun_app$m',type,
'fun_app$m': ( 'B_bool_fun_b_bool_fun_bool_fun_fun$' * 'B_bool_fun$' ) > 'B_bool_fun_bool_fun$' ).
tff('function_fun_app$m',axiom,
( ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_bool_fun$_2' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_bool_fun$_1' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_bool_fun$_4' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_bool_fun$_3' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_bool_fun$_2' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_bool_fun$_1' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_bool_fun$_2' )
& ( 'fun_app$m'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_bool_fun$_1' ) ) ).
tff(declare_def_37,type,
def_37: ( tlbool * tlbool ) > tlbool ).
tff(function_def_37,axiom,
( ( def_37(fmb_tlbool_1,fmb_tlbool_1) = fmb_tlbool_1 )
& ( def_37(fmb_tlbool_1,fmb_tlbool_2) = fmb_tlbool_2 )
& ( def_37(fmb_tlbool_2,fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_37(fmb_tlbool_2,fmb_tlbool_2) = fmb_tlbool_2 ) ) ).
tff(declare_def_19,type,
def_19: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_19,axiom,
( ( def_19('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_19('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_24,type,
def_24: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_24,axiom,
( ( def_24('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_24('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_26,type,
def_26: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_26,axiom,
( ( def_26('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_26('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff('declare_remove$',type,
'remove$': 'B$' > 'B_set_b_set_fun$' ).
tff('function_remove$',axiom,
'remove$'('fmb_B$_1') = 'fmb_B_set_b_set_fun$_4' ).
tff(declare_def_16,type,
def_16: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_16,axiom,
( ( def_16('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_16('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_14,type,
def_14: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_14,axiom,
( ( def_14('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_14('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff('declare_fun_app$k',type,
'fun_app$k': ( 'B_b_bool_fun_fun$' * 'B$' ) > 'B_bool_fun$' ).
tff('function_fun_app$k',axiom,
( ( 'fun_app$k'('fmb_B_b_bool_fun_fun$_1','fmb_B$_1') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$k'('fmb_B_b_bool_fun_fun$_2','fmb_B$_1') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$k'('fmb_B_b_bool_fun_fun$_3','fmb_B$_1') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$k'('fmb_B_b_bool_fun_fun$_4','fmb_B$_1') = 'fmb_B_bool_fun$_2' ) ) ).
tff(declare_def_9,type,
def_9: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_9,axiom,
( ( def_9('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_9('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_20,type,
def_20: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_20,axiom,
( ( def_20('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_20('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_10,type,
def_10: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_10,axiom,
( ( def_10('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_10('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_25,type,
def_25: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_25,axiom,
( ( def_25('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_25('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_13,type,
def_13: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_13,axiom,
( ( def_13('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_13('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_41,type,
def_41: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_41,axiom,
( ( def_41('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_41('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff(declare_def_38,type,
def_38: ( tlbool * tlbool ) > tlbool ).
tff(function_def_38,axiom,
( ( def_38(fmb_tlbool_1,fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_38(fmb_tlbool_1,fmb_tlbool_2) = fmb_tlbool_2 )
& ( def_38(fmb_tlbool_2,fmb_tlbool_1) = fmb_tlbool_1 )
& ( def_38(fmb_tlbool_2,fmb_tlbool_2) = fmb_tlbool_2 ) ) ).
tff('declare_the_elem$',type,
'the_elem$': 'B_set$' > 'B$' ).
tff('function_the_elem$',axiom,
( ( 'the_elem$'('fmb_B_set$_1') = 'fmb_B$_1' )
& ( 'the_elem$'('fmb_B_set$_2') = 'fmb_B$_1' ) ) ).
tff(declare_def_42,type,
def_42: tlbool > tlbool ).
tff(function_def_42,axiom,
( ( def_42(fmb_tlbool_1) = fmb_tlbool_2 )
& ( def_42(fmb_tlbool_2) = fmb_tlbool_1 ) ) ).
tff(declare_def_23,type,
def_23: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_23,axiom,
( ( def_23('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_23('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff('declare_fun_app$h',type,
'fun_app$h': ( 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' * 'B_bool_fun$' ) > 'B_bool_fun_b_bool_fun_fun$' ).
tff('function_fun_app$h',axiom,
( ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_b_bool_fun_fun$_2' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_b_bool_fun_fun$_3' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_b_bool_fun_fun$_4' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_b_bool_fun_fun$_2' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_b_bool_fun_fun$_1' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_b_bool_fun_fun$_3' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun_b_bool_fun_fun$_2' )
& ( 'fun_app$h'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun_b_bool_fun_fun$_3' ) ) ).
tff('declare_fun_app$g',type,
'fun_app$g': ( 'B_bool_fun_b_bool_fun_fun$' * 'B_bool_fun$' ) > 'B_bool_fun$' ).
tff('function_fun_app$g',axiom,
( ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_1','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_1','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_2','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_2','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_3','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_3','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun$_2' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_4','fmb_B_bool_fun$_1') = 'fmb_B_bool_fun$_1' )
& ( 'fun_app$g'('fmb_B_bool_fun_b_bool_fun_fun$_4','fmb_B_bool_fun$_2') = 'fmb_B_bool_fun$_1' ) ) ).
tff('declare_fun_app$d',type,
'fun_app$d': ( 'B_bool_fun_b_set_fun$' * 'B_bool_fun$' ) > 'B_set$' ).
tff('function_fun_app$d',axiom,
( ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_1','fmb_B_bool_fun$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_1','fmb_B_bool_fun$_2') = 'fmb_B_set$_2' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_2','fmb_B_bool_fun$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_2','fmb_B_bool_fun$_2') = 'fmb_B_set$_2' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_3','fmb_B_bool_fun$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_3','fmb_B_bool_fun$_2') = 'fmb_B_set$_2' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_4','fmb_B_bool_fun$_1') = 'fmb_B_set$_1' )
& ( 'fun_app$d'('fmb_B_bool_fun_b_set_fun$_4','fmb_B_bool_fun$_2') = 'fmb_B_set$_2' ) ) ).
tff(declare_def_11,type,
def_11: ( 'B_bool_fun$' * 'B$' ) > tlbool ).
tff(function_def_11,axiom,
( ( def_11('fmb_B_bool_fun$_1','fmb_B$_1') = fmb_tlbool_2 )
& ( def_11('fmb_B_bool_fun$_2','fmb_B$_1') = fmb_tlbool_1 ) ) ).
tff('declare_bot$a',type,
'bot$a': $o ).
tff('bot$a_definition',axiom,
~ 'bot$a' ).
tff('declare_top$a',type,
'top$a': $o ).
tff('top$a_definition',axiom,
'top$a' ).
tff('declare_semilattice_neutr$',type,
'semilattice_neutr$': ( 'Bool_bool_bool_fun_fun$' * tlbool ) > $o ).
tff('predicate_semilattice_neutr$',axiom,
( 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_1',fmb_tlbool_1)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_1',fmb_tlbool_2)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_2',fmb_tlbool_1)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_2',fmb_tlbool_2)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_3',fmb_tlbool_1)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_3',fmb_tlbool_2)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_4',fmb_tlbool_1)
& 'semilattice_neutr$'('fmb_Bool_bool_bool_fun_fun$_4',fmb_tlbool_2) ) ).
tff('declare_fun_app$i',type,
'fun_app$i': ( 'B_set_bool_fun$' * 'B_set$' ) > $o ).
tff('predicate_fun_app$i',axiom,
( 'fun_app$i'('fmb_B_set_bool_fun$_1','fmb_B_set$_1')
& 'fun_app$i'('fmb_B_set_bool_fun$_1','fmb_B_set$_2')
& 'fun_app$i'('fmb_B_set_bool_fun$_2','fmb_B_set$_1')
& ~ 'fun_app$i'('fmb_B_set_bool_fun$_2','fmb_B_set$_2')
& 'fun_app$i'('fmb_B_set_bool_fun$_3','fmb_B_set$_1')
& ~ 'fun_app$i'('fmb_B_set_bool_fun$_3','fmb_B_set$_2')
& ~ 'fun_app$i'('fmb_B_set_bool_fun$_4','fmb_B_set$_1')
& ~ 'fun_app$i'('fmb_B_set_bool_fun$_4','fmb_B_set$_2') ) ).
tff('declare_semilattice_neutr$b',type,
'semilattice_neutr$b': ( 'B_set_b_set_b_set_fun_fun$' * 'B_set$' ) > $o ).
tff('predicate_semilattice_neutr$b',axiom,
( 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_1','fmb_B_set$_1')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_1','fmb_B_set$_2')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_2','fmb_B_set$_1')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_2','fmb_B_set$_2')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_3','fmb_B_set$_1')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_3','fmb_B_set$_2')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_4','fmb_B_set$_1')
& 'semilattice_neutr$b'('fmb_B_set_b_set_b_set_fun_fun$_4','fmb_B_set$_2') ) ).
tff('declare_less_eq$b',type,
'less_eq$b': ( tlbool * tlbool ) > $o ).
tff('predicate_less_eq$b',axiom,
( 'less_eq$b'(fmb_tlbool_1,fmb_tlbool_1)
& 'less_eq$b'(fmb_tlbool_1,fmb_tlbool_2)
& ~ 'less_eq$b'(fmb_tlbool_2,fmb_tlbool_1)
& 'less_eq$b'(fmb_tlbool_2,fmb_tlbool_2) ) ).
tff('declare_member$',type,
'member$': ( 'B$' * 'B_set$' ) > $o ).
tff('predicate_member$',axiom,
( 'member$'('fmb_B$_1','fmb_B_set$_1')
& ~ 'member$'('fmb_B$_1','fmb_B_set$_2') ) ).
tff('declare_uminus$b',type,
'uminus$b': tlbool > $o ).
tff('predicate_uminus$b',axiom,
( 'uminus$b'(fmb_tlbool_1)
& ~ 'uminus$b'(fmb_tlbool_2) ) ).
tff('declare_is_empty$',type,
'is_empty$': 'B_set$' > $o ).
tff('predicate_is_empty$',axiom,
( ~ 'is_empty$'('fmb_B_set$_1')
& 'is_empty$'('fmb_B_set$_2') ) ).
tff('declare_semilattice_neutr$a',type,
'semilattice_neutr$a': ( 'B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$' * 'B_bool_fun$' ) > $o ).
tff('predicate_semilattice_neutr$a',axiom,
( 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1','fmb_B_bool_fun$_1')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_1','fmb_B_bool_fun$_2')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2','fmb_B_bool_fun$_1')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_2','fmb_B_bool_fun$_2')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3','fmb_B_bool_fun$_1')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_3','fmb_B_bool_fun$_2')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4','fmb_B_bool_fun$_1')
& 'semilattice_neutr$a'('fmb_B_bool_fun_b_bool_fun_b_bool_fun_fun_fun$_4','fmb_B_bool_fun$_2') ) ).
tff('declare_is_singleton$',type,
'is_singleton$': 'B_set$' > $o ).
tff('predicate_is_singleton$',axiom,
( 'is_singleton$'('fmb_B_set$_1')
& ~ 'is_singleton$'('fmb_B_set$_2') ) ).
tff('declare_fun_app$e',type,
'fun_app$e': ( 'Bool_bool_fun$' * tlbool ) > $o ).
tff('predicate_fun_app$e',axiom,
( 'fun_app$e'('fmb_Bool_bool_fun$_1',fmb_tlbool_1)
& 'fun_app$e'('fmb_Bool_bool_fun$_1',fmb_tlbool_2)
& ~ 'fun_app$e'('fmb_Bool_bool_fun$_2',fmb_tlbool_1)
& 'fun_app$e'('fmb_Bool_bool_fun$_2',fmb_tlbool_2)
& ~ 'fun_app$e'('fmb_Bool_bool_fun$_3',fmb_tlbool_1)
& ~ 'fun_app$e'('fmb_Bool_bool_fun$_3',fmb_tlbool_2)
& ~ 'fun_app$e'('fmb_Bool_bool_fun$_4',fmb_tlbool_1)
& ~ 'fun_app$e'('fmb_Bool_bool_fun$_4',fmb_tlbool_2) ) ).
tff('declare_pairwise$',type,
'pairwise$': ( 'B_b_bool_fun_fun$' * 'B_set$' ) > $o ).
tff('predicate_pairwise$',axiom,
( 'pairwise$'('fmb_B_b_bool_fun_fun$_1','fmb_B_set$_1')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_1','fmb_B_set$_2')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_2','fmb_B_set$_1')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_2','fmb_B_set$_2')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_3','fmb_B_set$_1')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_3','fmb_B_set$_2')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_4','fmb_B_set$_1')
& 'pairwise$'('fmb_B_b_bool_fun_fun$_4','fmb_B_set$_2') ) ).
tff('declare_ordering_top$',type,
'ordering_top$': ( 'B_bool_fun_b_bool_fun_bool_fun_fun$' * 'B_bool_fun_b_bool_fun_bool_fun_fun$' * 'B_bool_fun$' ) > $o ).
tff('predicate_ordering_top$',axiom,
( 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_1','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_2','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_3','fmb_B_bool_fun$_2')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_1')
& 'ordering_top$'('fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun_b_bool_fun_bool_fun_fun$_4','fmb_B_bool_fun$_2') ) ).
tff('declare_ordering_top$a',type,
'ordering_top$a': ( 'B_set_b_set_bool_fun_fun$' * 'B_set_b_set_bool_fun_fun$' * 'B_set$' ) > $o ).
tff('predicate_ordering_top$a',axiom,
( ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2')
& 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2')
& 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2')
& 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1')
& ~ 'ordering_top$a'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2') ) ).
tff('declare_fun_app$',type,
'fun_app$': ( 'B_bool_fun$' * 'B$' ) > $o ).
tff('predicate_fun_app$',axiom,
( 'fun_app$'('fmb_B_bool_fun$_1','fmb_B$_1')
& ~ 'fun_app$'('fmb_B_bool_fun$_2','fmb_B$_1') ) ).
tff('declare_fun_app$l',type,
'fun_app$l': ( 'B_bool_fun_bool_fun$' * 'B_bool_fun$' ) > $o ).
tff('predicate_fun_app$l',axiom,
( 'fun_app$l'('fmb_B_bool_fun_bool_fun$_1','fmb_B_bool_fun$_1')
& 'fun_app$l'('fmb_B_bool_fun_bool_fun$_1','fmb_B_bool_fun$_2')
& 'fun_app$l'('fmb_B_bool_fun_bool_fun$_2','fmb_B_bool_fun$_1')
& ~ 'fun_app$l'('fmb_B_bool_fun_bool_fun$_2','fmb_B_bool_fun$_2')
& 'fun_app$l'('fmb_B_bool_fun_bool_fun$_3','fmb_B_bool_fun$_1')
& ~ 'fun_app$l'('fmb_B_bool_fun_bool_fun$_3','fmb_B_bool_fun$_2')
& ~ 'fun_app$l'('fmb_B_bool_fun_bool_fun$_4','fmb_B_bool_fun$_1')
& ~ 'fun_app$l'('fmb_B_bool_fun_bool_fun$_4','fmb_B_bool_fun$_2') ) ).
tff('declare_minus$b',type,
'minus$b': ( tlbool * tlbool ) > $o ).
tff('predicate_minus$b',axiom,
( ~ 'minus$b'(fmb_tlbool_1,fmb_tlbool_1)
& ~ 'minus$b'(fmb_tlbool_1,fmb_tlbool_2)
& 'minus$b'(fmb_tlbool_2,fmb_tlbool_1)
& ~ 'minus$b'(fmb_tlbool_2,fmb_tlbool_2) ) ).
tff('declare_ordering_top_axioms$',type,
'ordering_top_axioms$': ( 'B_set_b_set_bool_fun_fun$' * 'B_set$' ) > $o ).
tff('predicate_ordering_top_axioms$',axiom,
( 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_1')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_1','fmb_B_set$_2')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_1')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_2','fmb_B_set$_2')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_1')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_3','fmb_B_set$_2')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_1')
& 'ordering_top_axioms$'('fmb_B_set_b_set_bool_fun_fun$_4','fmb_B_set$_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP322_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.41 % Computer : n007.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 27 12:52:25 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.15/0.47 Running first-order model finding
% 0.15/0.47 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.91/2.40 % (1390060)Will run a generic schedule for satisfiability detection.
% 7.91/2.40 % (1390069)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=309505015:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.91/2.40 % (1390065)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1537023837_2999 on theBenchmark for (2999ds/0Mi)
% 7.91/2.40 % (1390066)% WARNING: option uhcvi not known.
% 7.91/2.40 % (1390071)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=727699246:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.91/2.40 % (1390068)dis+10_1_sil=32000:sp=arity:random_seed=2659520968:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.91/2.40 % (1390067)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3177918399:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.91/2.40 % (1390070)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3839696389:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.91/2.40 % (1390066)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3821065376:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.91/2.40 % (1390069)Instruction limit reached!
% 7.91/2.40 % (1390069)------------------------------
% 7.91/2.40 % (1390069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390069)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390069)Termination reason: Instruction limit
% 7.91/2.40 % (1390069)Termination phase: Saturation
% 7.91/2.40 % (1390069)Time elapsed: 0.057 s
% 7.91/2.40 % (1390069)Peak memory usage: 14 MB
% 7.91/2.40 % (1390069)Instructions burned: 116 (million)
% 7.91/2.40 % (1390079)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3565098344:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.91/2.40 % (1390068)Instruction limit reached!
% 7.91/2.40 % (1390068)------------------------------
% 7.91/2.40 % (1390068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390068)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390068)Termination reason: Instruction limit
% 7.91/2.40 % (1390068)Termination phase: Saturation
% 7.91/2.40 % (1390068)Time elapsed: 0.102 s
% 7.91/2.40 % (1390068)Peak memory usage: 14 MB
% 7.91/2.40 % (1390068)Instructions burned: 103 (million)
% 7.91/2.40 % (1390070)Instruction limit reached!
% 7.91/2.40 % (1390070)------------------------------
% 7.91/2.40 % (1390070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390070)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390070)Termination reason: Instruction limit
% 7.91/2.40 % (1390070)Termination phase: Saturation
% 7.91/2.40 % (1390070)Time elapsed: 0.124 s
% 7.91/2.40 % (1390070)Peak memory usage: 14 MB
% 7.91/2.40 % (1390070)Instructions burned: 131 (million)
% 7.91/2.40 % (1390081)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=242670395:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.91/2.40 % (1390071)Instruction limit reached!
% 7.91/2.40 % (1390071)------------------------------
% 7.91/2.40 % (1390071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390071)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390071)Termination reason: Instruction limit
% 7.91/2.40 % (1390071)Termination phase: Saturation
% 7.91/2.40 % (1390071)Time elapsed: 0.155 s
% 7.91/2.40 % (1390071)Peak memory usage: 14 MB
% 7.91/2.40 % (1390071)Instructions burned: 159 (million)
% 7.91/2.40 % (1390082)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2028854765:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.91/2.40 % (1390084)ott-21_1_sil=16000:fs=off:random_seed=3216667623:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.91/2.40 % TRYING [1]
% 7.91/2.40 % TRYING [2]
% 7.91/2.40 % (1390081)Instruction limit reached!
% 7.91/2.40 % (1390081)------------------------------
% 7.91/2.40 % (1390081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390081)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390081)Termination reason: Instruction limit
% 7.91/2.40 % (1390081)Termination phase: Saturation
% 7.91/2.40 % (1390081)Time elapsed: 0.127 s
% 7.91/2.40 % (1390081)Peak memory usage: 14 MB
% 7.91/2.40 % (1390081)Instructions burned: 132 (million)
% 7.91/2.40 % (1390087)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2438034792:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 7.91/2.40 % TRYING [3]
% 7.91/2.40 % (1390084)Instruction limit reached!
% 7.91/2.40 % (1390084)------------------------------
% 7.91/2.40 % (1390084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390084)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390084)Termination reason: Instruction limit
% 7.91/2.40 % (1390084)Termination phase: Saturation
% 7.91/2.40 % (1390084)Time elapsed: 0.166 s
% 7.91/2.40 % (1390084)Peak memory usage: 14 MB
% 7.91/2.40 % (1390084)Instructions burned: 180 (million)
% 7.91/2.40 % (1390090)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1717018676:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 7.91/2.40 % (1390079)Instruction limit reached!
% 7.91/2.40 % (1390079)------------------------------
% 7.91/2.40 % (1390079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390079)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390079)Termination reason: Instruction limit
% 7.91/2.40 % (1390079)Termination phase: Finite model building constraint generation
% 7.91/2.40 % (1390079)Time elapsed: 0.318 s
% 7.91/2.40 % (1390079)Peak memory usage: 35 MB
% 7.91/2.40 % (1390079)Instructions burned: 714 (million)
% 7.91/2.40 % (1390092)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4096334768:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 7.91/2.40 % (1390082)Instruction limit reached!
% 7.91/2.40 % (1390082)------------------------------
% 7.91/2.40 % (1390082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390082)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390082)Termination reason: Instruction limit
% 7.91/2.40 % (1390082)Termination phase: Saturation
% 7.91/2.40 % (1390082)Time elapsed: 0.561 s
% 7.91/2.40 % (1390082)Peak memory usage: 18 MB
% 7.91/2.40 % (1390082)Instructions burned: 684 (million)
% 7.91/2.40 % Detected minimum model sizes of [1,1,1,1,1]
% 7.91/2.40 % Detected maximum model sizes of [2,max,max,max,max]
% 7.91/2.40 % TRYING [1,1,1,1,1]
% 7.91/2.40 % (1390095)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3658080897:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 7.91/2.40 % TRYING [1,1,1,1,2]
% 7.91/2.40 % TRYING [1,1,1,2,2]
% 7.91/2.40 % (1390087)Instruction limit reached!
% 7.91/2.40 % (1390087)------------------------------
% 7.91/2.40 % (1390087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390087)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390087)Termination reason: Instruction limit
% 7.91/2.40 % (1390087)Termination phase: Saturation
% 7.91/2.40 % (1390087)Time elapsed: 0.518 s
% 7.91/2.40 % (1390087)Peak memory usage: 15 MB
% 7.91/2.40 % (1390087)Instructions burned: 477 (million)
% 7.91/2.40 % (1390097)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=867429221:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 7.91/2.40 % TRYING [1,1,1,3,2]
% 7.91/2.40 % (1390092)Instruction limit reached!
% 7.91/2.40 % (1390092)------------------------------
% 7.91/2.40 % (1390092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390092)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390092)Termination reason: Instruction limit
% 7.91/2.40 % (1390092)Termination phase: Saturation
% 7.91/2.40 % (1390092)Time elapsed: 0.607 s
% 7.91/2.40 % (1390092)Peak memory usage: 23 MB
% 7.91/2.40 % (1390092)Instructions burned: 1181 (million)
% 7.91/2.40 % (1390099)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3208563574:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 7.91/2.40 % TRYING [1,2,1,3,2]
% 7.91/2.40 % (1390090)Instruction limit reached!
% 7.91/2.40 % (1390090)------------------------------
% 7.91/2.40 % (1390090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390090)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390090)Termination reason: Instruction limit
% 7.91/2.40 % (1390090)Termination phase: Finite model building preprocessing
% 7.91/2.40 % (1390090)Time elapsed: 0.692 s
% 7.91/2.40 % (1390090)Peak memory usage: 22 MB
% 7.91/2.40 % (1390090)Instructions burned: 865 (million)
% 7.91/2.40 % (1390101)fmb+10_1_sil=64000:random_seed=3361829452:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 7.91/2.40 % TRYING [2,2,1,3,2]
% 7.91/2.40 % TRYING [2,2,1,4,2]
% 7.91/2.40 % (1390095)Instruction limit reached!
% 7.91/2.40 % (1390095)------------------------------
% 7.91/2.40 % (1390095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390095)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390095)Termination reason: Instruction limit
% 7.91/2.40 % (1390095)Termination phase: Finite model building preprocessing
% 7.91/2.40 % (1390095)Time elapsed: 0.711 s
% 7.91/2.40 % (1390095)Peak memory usage: 22 MB
% 7.91/2.40 % (1390095)Instructions burned: 889 (million)
% 7.91/2.40 % (1390099)Instruction limit reached!
% 7.91/2.40 % (1390099)------------------------------
% 7.91/2.40 % (1390099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390099)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390099)Termination reason: Instruction limit
% 7.91/2.40 % (1390099)Termination phase: Saturation
% 7.91/2.40 % (1390099)Time elapsed: 0.444 s
% 7.91/2.40 % (1390099)Peak memory usage: 20 MB
% 7.91/2.40 % (1390099)Instructions burned: 879 (million)
% 7.91/2.40 % (1390103)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1134500315:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 7.91/2.40 % (1390104)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4057935868:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 7.91/2.40 % (1390097)Instruction limit reached!
% 7.91/2.40 % (1390097)------------------------------
% 7.91/2.40 % (1390097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.40 % (1390097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.40 % (1390097)CaDiCaL version: 2.1.3
% 7.91/2.40 % (1390097)Termination reason: Instruction limit
% 7.91/2.40 % (1390097)Termination phase: Saturation
% 7.91/2.40 % (1390097)Time elapsed: 0.678 s
% 7.91/2.40 % (1390097)Peak memory usage: 19 MB
% 7.91/2.40 % (1390097)Instructions burned: 692 (million)
% 7.91/2.40 % (1390107)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1092623372:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 7.91/2.40 % Finite Model Found!
% 7.91/2.40 % SZS status Satisfiable for theBenchmark
% 7.91/2.40 % Detected minimum model sizes of [1,1,1,1,1]
% 7.91/2.40 % Detected maximum model sizes of [2,max,max,max,max]
% 7.91/2.40 % TRYING [1,1,1,1,1]
% 7.91/2.40 % (1390065) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1390060-1390065"...
% 7.91/2.40 % (1390065)...printing done.
% 7.91/2.40 % TRYING [1,1,1,1,2]
% 7.91/2.40 % SZS output start FiniteModel for theBenchmark
% See solution above
% 7.91/2.41 % (1390065)------------------------------
% 7.91/2.41 % (1390065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.91/2.41 % (1390065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.91/2.41 % (1390065)CaDiCaL version: 2.1.3
% 7.91/2.41 % (1390065)Termination reason: Satisfiable
% 7.91/2.41 % (1390065)Time elapsed: 1.819 s
% 7.91/2.41 % (1390065)Peak memory usage: 48 MB
% 7.91/2.41 % (1390065)Instructions burned: 2291 (million)
% 7.91/2.41 % (1390060)Success in time 1.922 s
% 7.91/2.41 % Vampire exiting
%------------------------------------------------------------------------------