%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV440+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 01:24:17 PM UTC 2026
% Result : CounterSatisfiable 0.20s 0.27s
% Output : FiniteModel 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_unclassified,type,
unclassified: $i ).
tff(unclassified_definition,axiom,
unclassified = 'fmb_$i_1' ).
tff(declare_sbu,type,
sbu: $i ).
tff(sbu_definition,axiom,
sbu = 'fmb_$i_2' ).
tff(declare_confidential,type,
confidential: $i ).
tff(confidential_definition,axiom,
confidential = 'fmb_$i_2' ).
tff(declare_secret,type,
secret: $i ).
tff(secret_definition,axiom,
secret = 'fmb_$i_2' ).
tff(declare_topsecret,type,
topsecret: $i ).
tff(topsecret_definition,axiom,
topsecret = 'fmb_$i_2' ).
tff(declare_system,type,
system: $i ).
tff(system_definition,axiom,
system = 'fmb_$i_1' ).
tff(declare_admin,type,
admin: $i ).
tff(admin_definition,axiom,
admin = 'fmb_$i_1' ).
tff(declare_nil,type,
nil: $i ).
tff(nil_definition,axiom,
nil = 'fmb_$i_1' ).
tff(declare_anycountry,type,
anycountry: $i ).
tff(anycountry_definition,axiom,
anycountry = 'fmb_$i_1' ).
tff(declare_usa,type,
usa: $i ).
tff(usa_definition,axiom,
usa = 'fmb_$i_2' ).
tff(declare_yes,type,
yes: $i ).
tff(yes_definition,axiom,
yes = 'fmb_$i_1' ).
tff(declare_no,type,
no: $i ).
tff(no_definition,axiom,
no = 'fmb_$i_2' ).
tff(declare_read,type,
read: $i ).
tff(read_definition,axiom,
read = 'fmb_$i_1' ).
tff(declare_oca,type,
oca: $i ).
tff(oca_definition,axiom,
oca = 'fmb_$i_1' ).
tff(declare_compartmentb,type,
compartmentb: $i ).
tff(compartmentb_definition,axiom,
compartmentb = 'fmb_$i_1' ).
tff(declare_compartmenta,type,
compartmenta: $i ).
tff(compartmenta_definition,axiom,
compartmenta = 'fmb_$i_2' ).
tff(declare_sso_compartmentb,type,
sso_compartmentb: $i ).
tff(sso_compartmentb_definition,axiom,
sso_compartmentb = 'fmb_$i_1' ).
tff(declare_scg_compartmentb,type,
scg_compartmentb: $i ).
tff(scg_compartmentb_definition,axiom,
scg_compartmentb = 'fmb_$i_1' ).
tff(declare_sso_compartmenta,type,
sso_compartmenta: $i ).
tff(sso_compartmenta_definition,axiom,
sso_compartmenta = 'fmb_$i_2' ).
tff(declare_scg_compartmenta,type,
scg_compartmenta: $i ).
tff(scg_compartmenta_definition,axiom,
scg_compartmenta = 'fmb_$i_2' ).
tff(declare_secretfile,type,
secretfile: $i ).
tff(secretfile_definition,axiom,
secretfile = 'fmb_$i_1' ).
tff(declare_owner_secretfile,type,
owner_secretfile: $i ).
tff(owner_secretfile_definition,axiom,
owner_secretfile = 'fmb_$i_1' ).
tff(declare_not_secretfile,type,
not_secretfile: $i ).
tff(not_secretfile_definition,axiom,
not_secretfile = 'fmb_$i_2' ).
tff(declare_owner_not_secretfile,type,
owner_not_secretfile: $i ).
tff(owner_not_secretfile_definition,axiom,
owner_not_secretfile = 'fmb_$i_2' ).
tff(declare_polygraph_admin,type,
polygraph_admin: $i ).
tff(polygraph_admin_definition,axiom,
polygraph_admin = 'fmb_$i_1' ).
tff(declare_credit_admin,type,
credit_admin: $i ).
tff(credit_admin_definition,axiom,
credit_admin = 'fmb_$i_1' ).
tff(declare_background_admin,type,
background_admin: $i ).
tff(background_admin_definition,axiom,
background_admin = 'fmb_$i_1' ).
tff(declare_hr_admin,type,
hr_admin: $i ).
tff(hr_admin_definition,axiom,
hr_admin = 'fmb_$i_1' ).
tff(declare_level_admin,type,
level_admin: $i ).
tff(level_admin_definition,axiom,
level_admin = 'fmb_$i_1' ).
tff(declare_alice,type,
alice: $i ).
tff(alice_definition,axiom,
alice = 'fmb_$i_1' ).
tff(declare_babu,type,
babu: $i ).
tff(babu_definition,axiom,
babu = 'fmb_$i_2' ).
tff(declare_india,type,
india: $i ).
tff(india_definition,axiom,
india = 'fmb_$i_2' ).
tff(declare_ci,type,
ci: $i ).
tff(ci_definition,axiom,
ci = 'fmb_$i_2' ).
tff(declare_cons,type,
cons: ( $i * $i ) > $i ).
tff(function_cons,axiom,
( ( cons('fmb_$i_1','fmb_$i_1') = 'fmb_$i_2' )
& ( cons('fmb_$i_1','fmb_$i_2') = 'fmb_$i_2' )
& ( cons('fmb_$i_2','fmb_$i_1') = 'fmb_$i_2' )
& ( cons('fmb_$i_2','fmb_$i_2') = 'fmb_$i_2' ) ) ).
tff(declare_loca_level_direct_below,type,
loca_level_direct_below: ( $i * $i * $i ) > $o ).
tff(predicate_loca_level_direct_below,axiom,
( loca_level_direct_below('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& loca_level_direct_below('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& loca_level_direct_below('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& loca_level_direct_below('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& loca_level_direct_below('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& loca_level_direct_below('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& loca_level_direct_below('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& loca_level_direct_below('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_loca_level_below,type,
loca_level_below: ( $i * $i * $i ) > $o ).
tff(predicate_loca_level_below,axiom,
( loca_level_below('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& loca_level_below('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& loca_level_below('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& loca_level_below('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& loca_level_below('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& loca_level_below('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& loca_level_below('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& loca_level_below('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_compartment_has_sso,type,
system_compartment_has_sso: ( $i * $i * $i ) > $o ).
tff(predicate_system_compartment_has_sso,axiom,
( system_compartment_has_sso('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ system_compartment_has_sso('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ system_compartment_has_sso('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_compartment_has_sso('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_compartment_has_sso('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ system_compartment_has_sso('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ system_compartment_has_sso('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_compartment_has_sso('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_compartment_has_sso,type,
admin_compartment_has_sso: ( $i * $i * $i ) > $o ).
tff(predicate_admin_compartment_has_sso,axiom,
( admin_compartment_has_sso('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_compartment_has_sso('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ admin_compartment_has_sso('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_compartment_has_sso('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_compartment_has_sso('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_compartment_has_sso('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ admin_compartment_has_sso('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_compartment_has_sso('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_oca,type,
system_indi_is_oca: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_oca,axiom,
( system_indi_is_oca('fmb_$i_1','fmb_$i_1')
& system_indi_is_oca('fmb_$i_1','fmb_$i_2')
& system_indi_is_oca('fmb_$i_2','fmb_$i_1')
& system_indi_is_oca('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_oca_compartment_has_scg,type,
oca_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(predicate_oca_compartment_has_scg,axiom,
( oca_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ oca_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ oca_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ oca_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ oca_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_sso_compartment_has_scg,type,
sso_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(predicate_sso_compartment_has_scg,axiom,
( sso_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& sso_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& sso_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& sso_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& sso_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& sso_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& sso_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& sso_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_compartment_has_scg,type,
admin_compartment_has_scg: ( $i * $i * $i ) > $o ).
tff(predicate_admin_compartment_has_scg,axiom,
( admin_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_compartment_has_scg('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ admin_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_compartment_has_scg('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_compartment_has_scg('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ admin_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_compartment_has_scg('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_file_needs_compartments,type,
system_file_needs_compartments: ( $i * $i * $i ) > $o ).
tff(predicate_system_file_needs_compartments,axiom,
( system_file_needs_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_file_needs_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& system_file_needs_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_file_needs_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_file_needs_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_file_needs_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& system_file_needs_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_file_needs_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_compartments_h,type,
admin_file_has_compartments_h: ( $i * $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_compartments_h,axiom,
( admin_file_has_compartments_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_compartments_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_compartments_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ admin_file_has_compartments_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_compartments,type,
admin_file_has_compartments: ( $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_compartments,axiom,
( admin_file_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_file_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_file_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_file_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_sso_file_has_compartments,type,
sso_file_has_compartments: ( $i * $i * $i ) > $o ).
tff(predicate_sso_file_has_compartments,axiom,
( ~ sso_file_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& sso_file_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& sso_file_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_file_needs_level,type,
system_file_needs_level: ( $i * $i * $i ) > $o ).
tff(predicate_system_file_needs_level,axiom,
( system_file_needs_level('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_file_needs_level('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& system_file_needs_level('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_file_needs_level('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_file_needs_level('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_file_needs_level('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& system_file_needs_level('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_file_needs_level('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_level_h,type,
admin_file_has_level_h: ( $i * $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_level_h,axiom,
( admin_file_has_level_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_level_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_level_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_level_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ admin_file_has_level_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_level,type,
admin_file_has_level: ( $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_level,axiom,
( admin_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_sso_file_has_level,type,
sso_file_has_level: ( $i * $i * $i * $i ) > $o ).
tff(predicate_sso_file_has_level,axiom,
( ~ sso_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& sso_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& sso_file_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_file_needs_citizenship,type,
system_file_needs_citizenship: ( $i * $i * $i ) > $o ).
tff(predicate_system_file_needs_citizenship,axiom,
( system_file_needs_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_file_needs_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& system_file_needs_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_file_needs_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_file_needs_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_file_needs_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& system_file_needs_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_file_needs_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_citizenship_h,type,
admin_file_has_citizenship_h: ( $i * $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_citizenship_h,axiom,
( admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship_h('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_file_has_citizenship,type,
admin_file_has_citizenship: ( $i * $i * $i ) > $o ).
tff(predicate_admin_file_has_citizenship,axiom,
( admin_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_sso_file_has_citizenship,type,
sso_file_has_citizenship: ( $i * $i * $i * $i ) > $o ).
tff(predicate_sso_file_has_citizenship,axiom,
( ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& sso_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& sso_file_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ sso_file_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_polygraph_admin,type,
system_indi_is_polygraph_admin: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_polygraph_admin,axiom,
( system_indi_is_polygraph_admin('fmb_$i_1','fmb_$i_1')
& system_indi_is_polygraph_admin('fmb_$i_1','fmb_$i_2')
& system_indi_is_polygraph_admin('fmb_$i_2','fmb_$i_1')
& system_indi_is_polygraph_admin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_polygraph_admin_indi_has_polygraph,type,
polygraph_admin_indi_has_polygraph: ( $i * $i ) > $o ).
tff(predicate_polygraph_admin_indi_has_polygraph,axiom,
( polygraph_admin_indi_has_polygraph('fmb_$i_1','fmb_$i_1')
& ~ polygraph_admin_indi_has_polygraph('fmb_$i_1','fmb_$i_2')
& polygraph_admin_indi_has_polygraph('fmb_$i_2','fmb_$i_1')
& ~ polygraph_admin_indi_has_polygraph('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_polygraph,type,
admin_indi_has_polygraph: ( $i * $i ) > $o ).
tff(predicate_admin_indi_has_polygraph,axiom,
( admin_indi_has_polygraph('fmb_$i_1','fmb_$i_1')
& ~ admin_indi_has_polygraph('fmb_$i_1','fmb_$i_2')
& admin_indi_has_polygraph('fmb_$i_2','fmb_$i_1')
& ~ admin_indi_has_polygraph('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_credit_admin,type,
system_indi_is_credit_admin: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_credit_admin,axiom,
( system_indi_is_credit_admin('fmb_$i_1','fmb_$i_1')
& system_indi_is_credit_admin('fmb_$i_1','fmb_$i_2')
& system_indi_is_credit_admin('fmb_$i_2','fmb_$i_1')
& system_indi_is_credit_admin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_credit_admin_indi_has_credit,type,
credit_admin_indi_has_credit: ( $i * $i ) > $o ).
tff(predicate_credit_admin_indi_has_credit,axiom,
( credit_admin_indi_has_credit('fmb_$i_1','fmb_$i_1')
& credit_admin_indi_has_credit('fmb_$i_1','fmb_$i_2')
& credit_admin_indi_has_credit('fmb_$i_2','fmb_$i_1')
& credit_admin_indi_has_credit('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_credit,type,
admin_indi_has_credit: ( $i * $i ) > $o ).
tff(predicate_admin_indi_has_credit,axiom,
( admin_indi_has_credit('fmb_$i_1','fmb_$i_1')
& admin_indi_has_credit('fmb_$i_1','fmb_$i_2')
& admin_indi_has_credit('fmb_$i_2','fmb_$i_1')
& admin_indi_has_credit('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_background,type,
admin_indi_has_background: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_background,axiom,
( admin_indi_has_background('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_background('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_background('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_background('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_background('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_background('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_background('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_background('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_background_admin,type,
system_indi_is_background_admin: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_background_admin,axiom,
( system_indi_is_background_admin('fmb_$i_1','fmb_$i_1')
& system_indi_is_background_admin('fmb_$i_1','fmb_$i_2')
& system_indi_is_background_admin('fmb_$i_2','fmb_$i_1')
& system_indi_is_background_admin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_background_admin_indi_has_background,type,
background_admin_indi_has_background: ( $i * $i * $i ) > $o ).
tff(predicate_background_admin_indi_has_background,axiom,
( ~ background_admin_indi_has_background('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& background_admin_indi_has_background('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ background_admin_indi_has_background('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ background_admin_indi_has_background('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ background_admin_indi_has_background('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& background_admin_indi_has_background('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ background_admin_indi_has_background('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ background_admin_indi_has_background('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_hr_admin,type,
system_indi_is_hr_admin: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_hr_admin,axiom,
( system_indi_is_hr_admin('fmb_$i_1','fmb_$i_1')
& system_indi_is_hr_admin('fmb_$i_1','fmb_$i_2')
& system_indi_is_hr_admin('fmb_$i_2','fmb_$i_1')
& system_indi_is_hr_admin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_hr_admin_indi_has_employment,type,
hr_admin_indi_has_employment: ( $i * $i ) > $o ).
tff(predicate_hr_admin_indi_has_employment,axiom,
( hr_admin_indi_has_employment('fmb_$i_1','fmb_$i_1')
& hr_admin_indi_has_employment('fmb_$i_1','fmb_$i_2')
& hr_admin_indi_has_employment('fmb_$i_2','fmb_$i_1')
& hr_admin_indi_has_employment('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_employment,type,
admin_indi_has_employment: ( $i * $i ) > $o ).
tff(predicate_admin_indi_has_employment,axiom,
( admin_indi_has_employment('fmb_$i_1','fmb_$i_1')
& admin_indi_has_employment('fmb_$i_1','fmb_$i_2')
& admin_indi_has_employment('fmb_$i_2','fmb_$i_1')
& admin_indi_has_employment('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_citizenship,type,
admin_indi_has_citizenship: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_citizenship,axiom,
( admin_indi_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_has_citizenship,type,
system_indi_has_citizenship: ( $i * $i * $i ) > $o ).
tff(predicate_system_indi_has_citizenship,axiom,
( ~ system_indi_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_indi_has_citizenship('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ system_indi_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_indi_has_citizenship('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ system_indi_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_indi_has_citizenship('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ system_indi_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_indi_has_citizenship('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_level,type,
admin_indi_has_level: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_level,axiom,
( admin_indi_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_needs_level,type,
system_indi_needs_level: ( $i * $i * $i ) > $o ).
tff(predicate_system_indi_needs_level,axiom,
( ~ system_indi_needs_level('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_indi_needs_level('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ system_indi_needs_level('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ system_indi_needs_level('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ system_indi_needs_level('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_indi_needs_level('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ system_indi_needs_level('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ system_indi_needs_level('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_level_admin,type,
system_indi_is_level_admin: ( $i * $i ) > $o ).
tff(predicate_system_indi_is_level_admin,axiom,
( system_indi_is_level_admin('fmb_$i_1','fmb_$i_1')
& system_indi_is_level_admin('fmb_$i_1','fmb_$i_2')
& system_indi_is_level_admin('fmb_$i_2','fmb_$i_1')
& system_indi_is_level_admin('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_level_admin_indi_has_level,type,
level_admin_indi_has_level: ( $i * $i * $i ) > $o ).
tff(predicate_level_admin_indi_has_level,axiom,
( level_admin_indi_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& level_admin_indi_has_level('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& level_admin_indi_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& level_admin_indi_has_level('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& level_admin_indi_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& level_admin_indi_has_level('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& level_admin_indi_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& level_admin_indi_has_level('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_compartments,type,
admin_indi_has_compartments: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_compartments,axiom,
( admin_indi_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_compartments('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_compartments('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_compartments('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_compartments('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_needs_compartment,type,
system_indi_needs_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_system_indi_needs_compartment,axiom,
( system_indi_needs_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& system_indi_needs_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ system_indi_needs_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ system_indi_needs_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_indi_needs_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& system_indi_needs_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ system_indi_needs_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& ~ system_indi_needs_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_polygraph_for_compartment,type,
admin_indi_has_polygraph_for_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_polygraph_for_compartment,axiom,
( admin_indi_has_polygraph_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_polygraph_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_polygraph_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_polygraph_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_polygraph_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_polygraph_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_polygraph_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_polygraph_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_credit_for_compartment,type,
admin_indi_has_credit_for_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_credit_for_compartment,axiom,
( admin_indi_has_credit_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_credit_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_credit_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_credit_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_credit_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_credit_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_credit_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_credit_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_sso_indi_has_compartment,type,
sso_indi_has_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_sso_indi_has_compartment,axiom,
( sso_indi_has_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& sso_indi_has_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& sso_indi_has_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& sso_indi_has_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& sso_indi_has_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& sso_indi_has_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& sso_indi_has_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& sso_indi_has_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_background_for_compartment,type,
admin_indi_has_background_for_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_background_for_compartment,axiom,
( admin_indi_has_background_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_background_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_background_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_background_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_background_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_background_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_background_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_background_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_level_for_compartment,type,
admin_indi_has_level_for_compartment: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_level_for_compartment,axiom,
( admin_indi_has_level_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level_for_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level_for_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_level_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level_for_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level_for_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_oca_compartment_is_compartment,type,
oca_compartment_is_compartment: ( $i * $i * $i * $i * $i * $i ) > $o ).
tff(predicate_oca_compartment_is_compartment,axiom,
( oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& oca_compartment_is_compartment('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_compartments_for_file,type,
admin_indi_has_compartments_for_file: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_compartments_for_file,axiom,
( admin_indi_has_compartments_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_compartments_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_compartments_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_compartments_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_compartments_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_compartments_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_compartments_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_compartments_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_level_for_file,type,
admin_indi_has_level_for_file: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_level_for_file,axiom,
( admin_indi_has_level_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_level_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_level_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_level_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_level_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_state_file_has_owner,type,
state_file_has_owner: ( $i * $i ) > $o ).
tff(predicate_state_file_has_owner,axiom,
( state_file_has_owner('fmb_$i_1','fmb_$i_1')
& ~ state_file_has_owner('fmb_$i_1','fmb_$i_2')
& ~ state_file_has_owner('fmb_$i_2','fmb_$i_1')
& state_file_has_owner('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_owner_indi_has_need_to_know,type,
owner_indi_has_need_to_know: ( $i * $i * $i ) > $o ).
tff(predicate_owner_indi_has_need_to_know,axiom,
( owner_indi_has_need_to_know('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& owner_indi_has_need_to_know('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ owner_indi_has_need_to_know('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ owner_indi_has_need_to_know('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& ~ owner_indi_has_need_to_know('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ owner_indi_has_need_to_know('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ owner_indi_has_need_to_know('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& owner_indi_has_need_to_know('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_need_to_know_for_file,type,
admin_indi_has_need_to_know_for_file: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_need_to_know_for_file,axiom,
( admin_indi_has_need_to_know_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ admin_indi_has_need_to_know_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ admin_indi_has_need_to_know_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_need_to_know_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_need_to_know_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ admin_indi_has_need_to_know_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& ~ admin_indi_has_need_to_know_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_need_to_know_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_admin_indi_has_citizenship_for_file,type,
admin_indi_has_citizenship_for_file: ( $i * $i * $i ) > $o ).
tff(predicate_admin_indi_has_citizenship_for_file,axiom,
( admin_indi_has_citizenship_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_has_citizenship_for_file('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& admin_indi_has_citizenship_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& admin_indi_has_citizenship_for_file('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_has_citizenship_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_has_citizenship_for_file('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_has_citizenship_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_has_citizenship_for_file('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_state_file_is_not_working_paper,type,
state_file_is_not_working_paper: $i > $o ).
tff(predicate_state_file_is_not_working_paper,axiom,
( state_file_is_not_working_paper('fmb_$i_1')
& state_file_is_not_working_paper('fmb_$i_2') ) ).
tff(declare_admin_indi_may_file,type,
admin_indi_may_file: ( $i * $i * $i * $i ) > $o ).
tff(predicate_admin_indi_may_file,axiom,
( admin_indi_may_file('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_may_file('fmb_$i_1','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ admin_indi_may_file('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ admin_indi_may_file('fmb_$i_1','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_may_file('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_may_file('fmb_$i_1','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_may_file('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_may_file('fmb_$i_1','fmb_$i_2','fmb_$i_2','fmb_$i_2')
& admin_indi_may_file('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_1')
& admin_indi_may_file('fmb_$i_2','fmb_$i_1','fmb_$i_1','fmb_$i_2')
& ~ admin_indi_may_file('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_1')
& ~ admin_indi_may_file('fmb_$i_2','fmb_$i_1','fmb_$i_2','fmb_$i_2')
& admin_indi_may_file('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_1')
& admin_indi_may_file('fmb_$i_2','fmb_$i_2','fmb_$i_1','fmb_$i_2')
& admin_indi_may_file('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_1')
& admin_indi_may_file('fmb_$i_2','fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
tff(declare_system_indi_is_counterintelligence,type,
system_indi_is_counterintelligence: ( $i * $i * $i ) > $o ).
tff(predicate_system_indi_is_counterintelligence,axiom,
( system_indi_is_counterintelligence('fmb_$i_1','fmb_$i_1','fmb_$i_1')
& ~ system_indi_is_counterintelligence('fmb_$i_1','fmb_$i_1','fmb_$i_2')
& system_indi_is_counterintelligence('fmb_$i_1','fmb_$i_2','fmb_$i_1')
& system_indi_is_counterintelligence('fmb_$i_1','fmb_$i_2','fmb_$i_2')
& system_indi_is_counterintelligence('fmb_$i_2','fmb_$i_1','fmb_$i_1')
& ~ system_indi_is_counterintelligence('fmb_$i_2','fmb_$i_1','fmb_$i_2')
& system_indi_is_counterintelligence('fmb_$i_2','fmb_$i_2','fmb_$i_1')
& system_indi_is_counterintelligence('fmb_$i_2','fmb_$i_2','fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV440+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n009.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:08:15 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.27 % (2964190)Will run a generic schedule for satisfiability detection.
% 0.20/0.27 % (2964201)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=643588202_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.27 % (2964202)% WARNING: option uhcvi not known.
% 0.20/0.27 % TRYING [1]
% 0.20/0.27 % TRYING [2]
% 0.20/0.27 % Finite Model Found!
% 0.20/0.27 % SZS status CounterSatisfiable for theBenchmark
% 0.20/0.27 % (2964201) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2964190-2964201"...
% 0.20/0.27 % (2964201)...printing done.
% 0.20/0.27 % (2964202)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2246490838:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.27 % (2964203)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=114873150:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.27 % (2964205)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=488397636:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.27 % (2964204)dis+10_1_sil=32000:sp=arity:random_seed=3050054694:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.27 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.20/0.28 % (2964201)------------------------------
% 0.20/0.28 % (2964201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.28 % (2964201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.28 % (2964201)CaDiCaL version: 2.1.3
% 0.20/0.28 % (2964201)Termination reason: Satisfiable
% 0.20/0.28 % (2964201)Time elapsed: 0.007 s
% 0.20/0.28 % (2964201)Peak memory usage: 12 MB
% 0.20/0.28 % (2964201)Instructions burned: 24 (million)
% 0.20/0.28 % (2964190)Success in time 0.039 s
% 0.20/0.28 % Vampire exiting
%------------------------------------------------------------------------------