lazyCoP---0.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : lazyCoP---0.1
% Problem  : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop

% Computer : n024.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 600s
% DateTime : Wed Jul 20 19:47:06 EDT 2022

% Result   : Theorem 5.92s 1.10s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13  % Command  : vampire -t 0 --mode clausify %d -updr off -nm 2 -erd input_only -icip on | lazycop
% 0.12/0.34  % Computer : n024.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Thu Jun 16 02:22:33 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 5.92/1.10  % SZS status Theorem
% 5.92/1.10  % SZS output begin IncompleteProof
% 5.92/1.10  cnf(c0, axiom,
% 5.92/1.10  	~admin_indi_may_file(admin,alice,secretfile,read)).
% 5.92/1.10  cnf(c1, plain,
% 5.92/1.10  	~admin_indi_may_file(admin,alice,secretfile,read),
% 5.92/1.10  	inference(start, [], [c0])).
% 5.92/1.10  
% 5.92/1.10  cnf(c2, axiom,
% 5.92/1.10  	admin_indi_may_file(admin,X0,X1,read) | ~admin_indi_has_compartments_for_file(admin,X0,X1) | ~admin_indi_has_level_for_file(admin,X0,X1) | ~admin_indi_has_need_to_know_for_file(admin,X0,X1) | ~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1)).
% 5.92/1.10  cnf(a0, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a1, assumption,
% 5.92/1.10  	alice = X0).
% 5.92/1.10  cnf(a2, assumption,
% 5.92/1.10  	secretfile = X1).
% 5.92/1.10  cnf(a3, assumption,
% 5.92/1.10  	read = read).
% 5.92/1.10  cnf(c3, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3])], [c1, c2])).
% 5.92/1.10  cnf(c4, plain,
% 5.92/1.10  	~admin_indi_has_compartments_for_file(admin,X0,X1) | ~admin_indi_has_level_for_file(admin,X0,X1) | ~admin_indi_has_need_to_know_for_file(admin,X0,X1) | ~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a0, a1, a2, a3])], [c1, c2])).
% 5.92/1.10  
% 5.92/1.10  cnf(c5, axiom,
% 5.92/1.10  	admin_indi_has_compartments_for_file(admin,X2,X3) | ~admin_indi_has_compartments(admin,X2,X4) | ~admin_file_has_compartments(admin,X3,X4)).
% 5.92/1.10  cnf(a4, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a5, assumption,
% 5.92/1.10  	X0 = X2).
% 5.92/1.10  cnf(a6, assumption,
% 5.92/1.10  	X1 = X3).
% 5.92/1.10  cnf(c6, plain,
% 5.92/1.10  	~admin_indi_has_level_for_file(admin,X0,X1) | ~admin_indi_has_need_to_know_for_file(admin,X0,X1) | ~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a4, a5, a6])], [c4, c5])).
% 5.92/1.10  cnf(c7, plain,
% 5.92/1.10  	~admin_indi_has_compartments(admin,X2,X4) | ~admin_file_has_compartments(admin,X3,X4),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a4, a5, a6])], [c4, c5])).
% 5.92/1.10  
% 5.92/1.10  cnf(c8, axiom,
% 5.92/1.10  	admin_indi_has_compartments(admin,X5,cons(X6,X7)) | ~admin_indi_has_compartments(admin,X5,X7) | ~admin_indi_has_level_for_compartment(admin,X5,X6) | ~admin_indi_has_background_for_compartment(admin,X5,X6) | ~sso_indi_has_compartment(X8,X5,X6) | ~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6)).
% 5.92/1.10  cnf(a7, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a8, assumption,
% 5.92/1.10  	X2 = X5).
% 5.92/1.10  cnf(a9, assumption,
% 5.92/1.10  	X4 = cons(X6,X7)).
% 5.92/1.10  cnf(c9, plain,
% 5.92/1.10  	~admin_file_has_compartments(admin,X3,X4),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a7, a8, a9])], [c7, c8])).
% 5.92/1.10  cnf(c10, plain,
% 5.92/1.10  	~admin_indi_has_compartments(admin,X5,X7) | ~admin_indi_has_level_for_compartment(admin,X5,X6) | ~admin_indi_has_background_for_compartment(admin,X5,X6) | ~sso_indi_has_compartment(X8,X5,X6) | ~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a7, a8, a9])], [c7, c8])).
% 5.92/1.10  
% 5.92/1.10  cnf(c11, axiom,
% 5.92/1.10  	admin_indi_has_compartments(admin,X9,cons(X10,X11)) | ~admin_indi_has_compartments(admin,X9,X11) | ~admin_indi_has_level_for_compartment(admin,X9,X10) | ~admin_indi_has_background_for_compartment(admin,X9,X10) | ~sso_indi_has_compartment(X12,X9,X10) | ~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10)).
% 5.92/1.10  cnf(a10, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a11, assumption,
% 5.92/1.10  	X5 = X9).
% 5.92/1.10  cnf(a12, assumption,
% 5.92/1.10  	X7 = cons(X10,X11)).
% 5.92/1.10  cnf(c12, plain,
% 5.92/1.10  	~admin_indi_has_level_for_compartment(admin,X5,X6) | ~admin_indi_has_background_for_compartment(admin,X5,X6) | ~sso_indi_has_compartment(X8,X5,X6) | ~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a10, a11, a12])], [c10, c11])).
% 5.92/1.10  cnf(c13, plain,
% 5.92/1.10  	~admin_indi_has_compartments(admin,X9,X11) | ~admin_indi_has_level_for_compartment(admin,X9,X10) | ~admin_indi_has_background_for_compartment(admin,X9,X10) | ~sso_indi_has_compartment(X12,X9,X10) | ~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a10, a11, a12])], [c10, c11])).
% 5.92/1.10  
% 5.92/1.10  cnf(c14, axiom,
% 5.92/1.10  	admin_indi_has_compartments(admin,X13,nil)).
% 5.92/1.10  cnf(a13, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a14, assumption,
% 5.92/1.10  	X9 = X13).
% 5.92/1.10  cnf(a15, assumption,
% 5.92/1.10  	X11 = nil).
% 5.92/1.10  cnf(c15, plain,
% 5.92/1.10  	~admin_indi_has_level_for_compartment(admin,X9,X10) | ~admin_indi_has_background_for_compartment(admin,X9,X10) | ~sso_indi_has_compartment(X12,X9,X10) | ~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a13, a14, a15])], [c13, c14])).
% 5.92/1.10  cnf(c16, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a13, a14, a15])], [c13, c14])).
% 5.92/1.10  
% 5.92/1.10  cnf(c17, axiom,
% 5.92/1.10  	admin_indi_has_level_for_compartment(admin,X14,X15) | ~admin_indi_has_level(admin,X14,X16) | ~oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20) | ~system_indi_is_oca(system,X17)).
% 5.92/1.10  cnf(a16, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a17, assumption,
% 5.92/1.10  	X9 = X14).
% 5.92/1.10  cnf(a18, assumption,
% 5.92/1.10  	X10 = X15).
% 5.92/1.10  cnf(c18, plain,
% 5.92/1.10  	~admin_indi_has_background_for_compartment(admin,X9,X10) | ~sso_indi_has_compartment(X12,X9,X10) | ~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a16, a17, a18])], [c15, c17])).
% 5.92/1.10  cnf(c19, plain,
% 5.92/1.10  	~admin_indi_has_level(admin,X14,X16) | ~oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20) | ~system_indi_is_oca(system,X17),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a16, a17, a18])], [c15, c17])).
% 5.92/1.10  
% 5.92/1.10  cnf(c20, axiom,
% 5.92/1.10  	admin_indi_has_level(admin,X21,X22) | ~admin_indi_has_background(admin,X21,X22) | ~loca_level_below(admin,X22,X23) | ~level_admin_indi_has_level(X24,X21,X23) | ~system_indi_is_level_admin(system,X24) | ~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25)).
% 5.92/1.10  cnf(a19, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a20, assumption,
% 5.92/1.10  	X14 = X21).
% 5.92/1.10  cnf(a21, assumption,
% 5.92/1.10  	X16 = X22).
% 5.92/1.10  cnf(c21, plain,
% 5.92/1.10  	~oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20) | ~system_indi_is_oca(system,X17),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a19, a20, a21])], [c19, c20])).
% 5.92/1.10  cnf(c22, plain,
% 5.92/1.10  	~admin_indi_has_background(admin,X21,X22) | ~loca_level_below(admin,X22,X23) | ~level_admin_indi_has_level(X24,X21,X23) | ~system_indi_is_level_admin(system,X24) | ~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a19, a20, a21])], [c19, c20])).
% 5.92/1.10  
% 5.92/1.10  cnf(c23, axiom,
% 5.92/1.10  	admin_indi_has_background(admin,X26,X27) | ~loca_level_below(admin,X27,X28) | ~background_admin_indi_has_background(X29,X26,X28) | ~system_indi_is_background_admin(system,X29)).
% 5.92/1.10  cnf(a22, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a23, assumption,
% 5.92/1.10  	X21 = X26).
% 5.92/1.10  cnf(a24, assumption,
% 5.92/1.10  	X22 = X27).
% 5.92/1.10  cnf(c24, plain,
% 5.92/1.10  	~loca_level_below(admin,X22,X23) | ~level_admin_indi_has_level(X24,X21,X23) | ~system_indi_is_level_admin(system,X24) | ~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a22, a23, a24])], [c22, c23])).
% 5.92/1.10  cnf(c25, plain,
% 5.92/1.10  	~loca_level_below(admin,X27,X28) | ~background_admin_indi_has_background(X29,X26,X28) | ~system_indi_is_background_admin(system,X29),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a22, a23, a24])], [c22, c23])).
% 5.92/1.10  
% 5.92/1.10  cnf(c26, axiom,
% 5.92/1.10  	loca_level_below(X30,X31,X32) | ~loca_level_below(X30,X31,X33) | ~loca_level_direct_below(X30,X33,X32)).
% 5.92/1.10  cnf(a25, assumption,
% 5.92/1.10  	admin = X30).
% 5.92/1.10  cnf(a26, assumption,
% 5.92/1.10  	X27 = X31).
% 5.92/1.10  cnf(a27, assumption,
% 5.92/1.10  	X28 = X32).
% 5.92/1.10  cnf(c27, plain,
% 5.92/1.10  	~background_admin_indi_has_background(X29,X26,X28) | ~system_indi_is_background_admin(system,X29),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a25, a26, a27])], [c25, c26])).
% 5.92/1.10  cnf(c28, plain,
% 5.92/1.10  	~loca_level_below(X30,X31,X33) | ~loca_level_direct_below(X30,X33,X32),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a25, a26, a27])], [c25, c26])).
% 5.92/1.10  
% 5.92/1.10  cnf(c29, axiom,
% 5.92/1.10  	loca_level_below(X34,X35,X36) | ~loca_level_below(X34,X35,X37) | ~loca_level_direct_below(X34,X37,X36)).
% 5.92/1.10  cnf(a28, assumption,
% 5.92/1.10  	X30 = X34).
% 5.92/1.10  cnf(a29, assumption,
% 5.92/1.10  	X31 = X35).
% 5.92/1.10  cnf(a30, assumption,
% 5.92/1.10  	X33 = X36).
% 5.92/1.10  cnf(c30, plain,
% 5.92/1.10  	~loca_level_direct_below(X30,X33,X32),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a28, a29, a30])], [c28, c29])).
% 5.92/1.10  cnf(c31, plain,
% 5.92/1.10  	~loca_level_below(X34,X35,X37) | ~loca_level_direct_below(X34,X37,X36),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a28, a29, a30])], [c28, c29])).
% 5.92/1.10  
% 5.92/1.10  cnf(c32, axiom,
% 5.92/1.10  	loca_level_below(X38,X39,X40) | ~loca_level_below(X38,X39,X41) | ~loca_level_direct_below(X38,X41,X40)).
% 5.92/1.10  cnf(a31, assumption,
% 5.92/1.10  	X34 = X38).
% 5.92/1.10  cnf(a32, assumption,
% 5.92/1.10  	X35 = X39).
% 5.92/1.10  cnf(a33, assumption,
% 5.92/1.10  	X37 = X40).
% 5.92/1.10  cnf(c33, plain,
% 5.92/1.10  	~loca_level_direct_below(X34,X37,X36),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a31, a32, a33])], [c31, c32])).
% 5.92/1.10  cnf(c34, plain,
% 5.92/1.10  	~loca_level_below(X38,X39,X41) | ~loca_level_direct_below(X38,X41,X40),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a31, a32, a33])], [c31, c32])).
% 5.92/1.10  
% 5.92/1.10  cnf(c35, axiom,
% 5.92/1.10  	loca_level_below(X42,X43,X43)).
% 5.92/1.10  cnf(a34, assumption,
% 5.92/1.10  	X38 = X42).
% 5.92/1.10  cnf(a35, assumption,
% 5.92/1.10  	X39 = X43).
% 5.92/1.10  cnf(a36, assumption,
% 5.92/1.10  	X41 = X43).
% 5.92/1.10  cnf(c36, plain,
% 5.92/1.10  	~loca_level_direct_below(X38,X41,X40),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a34, a35, a36])], [c34, c35])).
% 5.92/1.10  cnf(c37, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a34, a35, a36])], [c34, c35])).
% 5.92/1.10  
% 5.92/1.10  cnf(c38, axiom,
% 5.92/1.10  	loca_level_direct_below(X44,sbu,confidential)).
% 5.92/1.10  cnf(a37, assumption,
% 5.92/1.10  	X38 = X44).
% 5.92/1.10  cnf(a38, assumption,
% 5.92/1.10  	X41 = sbu).
% 5.92/1.10  cnf(a39, assumption,
% 5.92/1.10  	X40 = confidential).
% 5.92/1.10  cnf(c39, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a37, a38, a39])], [c36, c38])).
% 5.92/1.10  cnf(c40, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a37, a38, a39])], [c36, c38])).
% 5.92/1.10  
% 5.92/1.10  cnf(c41, axiom,
% 5.92/1.10  	loca_level_direct_below(X45,confidential,secret)).
% 5.92/1.10  cnf(a40, assumption,
% 5.92/1.10  	X34 = X45).
% 5.92/1.10  cnf(a41, assumption,
% 5.92/1.10  	X37 = confidential).
% 5.92/1.10  cnf(a42, assumption,
% 5.92/1.10  	X36 = secret).
% 5.92/1.10  cnf(c42, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a40, a41, a42])], [c33, c41])).
% 5.92/1.10  cnf(c43, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a40, a41, a42])], [c33, c41])).
% 5.92/1.10  
% 5.92/1.10  cnf(c44, axiom,
% 5.92/1.10  	loca_level_direct_below(X46,secret,topsecret)).
% 5.92/1.10  cnf(a43, assumption,
% 5.92/1.10  	X30 = X46).
% 5.92/1.10  cnf(a44, assumption,
% 5.92/1.10  	X33 = secret).
% 5.92/1.10  cnf(a45, assumption,
% 5.92/1.10  	X32 = topsecret).
% 5.92/1.10  cnf(c45, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a43, a44, a45])], [c30, c44])).
% 5.92/1.10  cnf(c46, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a43, a44, a45])], [c30, c44])).
% 5.92/1.10  
% 5.92/1.10  cnf(c47, axiom,
% 5.92/1.10  	background_admin_indi_has_background(background_admin,alice,topsecret)).
% 5.92/1.10  cnf(a46, assumption,
% 5.92/1.10  	X29 = background_admin).
% 5.92/1.10  cnf(a47, assumption,
% 5.92/1.10  	X26 = alice).
% 5.92/1.10  cnf(a48, assumption,
% 5.92/1.10  	X28 = topsecret).
% 5.92/1.10  cnf(c48, plain,
% 5.92/1.10  	~system_indi_is_background_admin(system,X29),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a46, a47, a48])], [c27, c47])).
% 5.92/1.10  cnf(c49, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a46, a47, a48])], [c27, c47])).
% 5.92/1.10  
% 5.92/1.10  cnf(c50, axiom,
% 5.92/1.10  	system_indi_is_background_admin(system,background_admin)).
% 5.92/1.10  cnf(a49, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a50, assumption,
% 5.92/1.10  	X29 = background_admin).
% 5.92/1.10  cnf(c51, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a49, a50])], [c48, c50])).
% 5.92/1.10  cnf(c52, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a49, a50])], [c48, c50])).
% 5.92/1.10  
% 5.92/1.10  cnf(c53, plain,
% 5.92/1.10  	loca_level_below(admin,X27,X28)).
% 5.92/1.10  cnf(a51, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a52, assumption,
% 5.92/1.10  	X22 = X27).
% 5.92/1.10  cnf(a53, assumption,
% 5.92/1.10  	X23 = X28).
% 5.92/1.10  cnf(c54, plain,
% 5.92/1.10  	~level_admin_indi_has_level(X24,X21,X23) | ~system_indi_is_level_admin(system,X24) | ~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a51, a52, a53])], [c24, c53])).
% 5.92/1.10  
% 5.92/1.10  cnf(c55, axiom,
% 5.92/1.10  	level_admin_indi_has_level(level_admin,alice,topsecret)).
% 5.92/1.10  cnf(a54, assumption,
% 5.92/1.10  	X24 = level_admin).
% 5.92/1.10  cnf(a55, assumption,
% 5.92/1.10  	X21 = alice).
% 5.92/1.10  cnf(a56, assumption,
% 5.92/1.10  	X23 = topsecret).
% 5.92/1.10  cnf(c56, plain,
% 5.92/1.10  	~system_indi_is_level_admin(system,X24) | ~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a54, a55, a56])], [c54, c55])).
% 5.92/1.10  cnf(c57, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a54, a55, a56])], [c54, c55])).
% 5.92/1.10  
% 5.92/1.10  cnf(c58, axiom,
% 5.92/1.10  	system_indi_is_level_admin(system,level_admin)).
% 5.92/1.10  cnf(a57, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a58, assumption,
% 5.92/1.10  	X24 = level_admin).
% 5.92/1.10  cnf(c59, plain,
% 5.92/1.10  	~loca_level_below(admin,X22,X25) | ~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a57, a58])], [c56, c58])).
% 5.92/1.10  cnf(c60, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a57, a58])], [c56, c58])).
% 5.92/1.10  
% 5.92/1.10  cnf(c61, plain,
% 5.92/1.10  	loca_level_below(X30,X31,X33)).
% 5.92/1.10  cnf(a59, assumption,
% 5.92/1.10  	admin = X30).
% 5.92/1.10  cnf(a60, assumption,
% 5.92/1.10  	X22 = X31).
% 5.92/1.10  cnf(a61, assumption,
% 5.92/1.10  	X25 = X33).
% 5.92/1.10  cnf(c62, plain,
% 5.92/1.10  	~admin_indi_has_credit(admin,X21) | ~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a59, a60, a61])], [c59, c61])).
% 5.92/1.10  
% 5.92/1.10  cnf(c63, axiom,
% 5.92/1.10  	admin_indi_has_credit(admin,X47) | ~credit_admin_indi_has_credit(X48,X47) | ~system_indi_is_credit_admin(system,X48)).
% 5.92/1.10  cnf(a62, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a63, assumption,
% 5.92/1.10  	X21 = X47).
% 5.92/1.10  cnf(c64, plain,
% 5.92/1.10  	~admin_indi_has_employment(admin,X21) | ~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a62, a63])], [c62, c63])).
% 5.92/1.10  cnf(c65, plain,
% 5.92/1.10  	~credit_admin_indi_has_credit(X48,X47) | ~system_indi_is_credit_admin(system,X48),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a62, a63])], [c62, c63])).
% 5.92/1.10  
% 5.92/1.10  cnf(c66, axiom,
% 5.92/1.10  	credit_admin_indi_has_credit(credit_admin,alice)).
% 5.92/1.10  cnf(a64, assumption,
% 5.92/1.10  	X48 = credit_admin).
% 5.92/1.10  cnf(a65, assumption,
% 5.92/1.10  	X47 = alice).
% 5.92/1.10  cnf(c67, plain,
% 5.92/1.10  	~system_indi_is_credit_admin(system,X48),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a64, a65])], [c65, c66])).
% 5.92/1.10  cnf(c68, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a64, a65])], [c65, c66])).
% 5.92/1.10  
% 5.92/1.10  cnf(c69, axiom,
% 5.92/1.10  	system_indi_is_credit_admin(system,credit_admin)).
% 5.92/1.10  cnf(a66, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a67, assumption,
% 5.92/1.10  	X48 = credit_admin).
% 5.92/1.10  cnf(c70, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a66, a67])], [c67, c69])).
% 5.92/1.10  cnf(c71, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a66, a67])], [c67, c69])).
% 5.92/1.10  
% 5.92/1.10  cnf(c72, axiom,
% 5.92/1.10  	admin_indi_has_employment(admin,X49) | ~hr_admin_indi_has_employment(X50,X49) | ~system_indi_is_hr_admin(system,X50)).
% 5.92/1.10  cnf(a68, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a69, assumption,
% 5.92/1.10  	X21 = X49).
% 5.92/1.10  cnf(c73, plain,
% 5.92/1.10  	~admin_indi_has_polygraph(admin,X21) | ~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a68, a69])], [c64, c72])).
% 5.92/1.10  cnf(c74, plain,
% 5.92/1.10  	~hr_admin_indi_has_employment(X50,X49) | ~system_indi_is_hr_admin(system,X50),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a68, a69])], [c64, c72])).
% 5.92/1.10  
% 5.92/1.10  cnf(c75, axiom,
% 5.92/1.10  	hr_admin_indi_has_employment(hr_admin,alice)).
% 5.92/1.10  cnf(a70, assumption,
% 5.92/1.10  	X50 = hr_admin).
% 5.92/1.10  cnf(a71, assumption,
% 5.92/1.10  	X49 = alice).
% 5.92/1.10  cnf(c76, plain,
% 5.92/1.10  	~system_indi_is_hr_admin(system,X50),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a70, a71])], [c74, c75])).
% 5.92/1.10  cnf(c77, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a70, a71])], [c74, c75])).
% 5.92/1.10  
% 5.92/1.10  cnf(c78, axiom,
% 5.92/1.10  	system_indi_is_hr_admin(system,hr_admin)).
% 5.92/1.10  cnf(a72, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a73, assumption,
% 5.92/1.10  	X50 = hr_admin).
% 5.92/1.10  cnf(c79, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a72, a73])], [c76, c78])).
% 5.92/1.10  cnf(c80, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a72, a73])], [c76, c78])).
% 5.92/1.10  
% 5.92/1.10  cnf(c81, axiom,
% 5.92/1.10  	admin_indi_has_polygraph(admin,X51) | ~polygraph_admin_indi_has_polygraph(X52,X51) | ~system_indi_is_polygraph_admin(system,X52)).
% 5.92/1.10  cnf(a74, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a75, assumption,
% 5.92/1.10  	X21 = X51).
% 5.92/1.10  cnf(c82, plain,
% 5.92/1.10  	~admin_indi_has_citizenship(admin,X21,usa) | ~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a74, a75])], [c73, c81])).
% 5.92/1.10  cnf(c83, plain,
% 5.92/1.10  	~polygraph_admin_indi_has_polygraph(X52,X51) | ~system_indi_is_polygraph_admin(system,X52),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a74, a75])], [c73, c81])).
% 5.92/1.10  
% 5.92/1.10  cnf(c84, axiom,
% 5.92/1.10  	polygraph_admin_indi_has_polygraph(polygraph_admin,alice)).
% 5.92/1.10  cnf(a76, assumption,
% 5.92/1.10  	X52 = polygraph_admin).
% 5.92/1.10  cnf(a77, assumption,
% 5.92/1.10  	X51 = alice).
% 5.92/1.10  cnf(c85, plain,
% 5.92/1.10  	~system_indi_is_polygraph_admin(system,X52),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a76, a77])], [c83, c84])).
% 5.92/1.10  cnf(c86, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a76, a77])], [c83, c84])).
% 5.92/1.10  
% 5.92/1.10  cnf(c87, axiom,
% 5.92/1.10  	system_indi_is_polygraph_admin(system,polygraph_admin)).
% 5.92/1.10  cnf(a78, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a79, assumption,
% 5.92/1.10  	X52 = polygraph_admin).
% 5.92/1.10  cnf(c88, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a78, a79])], [c85, c87])).
% 5.92/1.10  cnf(c89, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a78, a79])], [c85, c87])).
% 5.92/1.10  
% 5.92/1.10  cnf(c90, axiom,
% 5.92/1.10  	admin_indi_has_citizenship(admin,X53,X54) | ~system_indi_has_citizenship(system,X53,X54)).
% 5.92/1.10  cnf(a80, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a81, assumption,
% 5.92/1.10  	X21 = X53).
% 5.92/1.10  cnf(a82, assumption,
% 5.92/1.10  	usa = X54).
% 5.92/1.10  cnf(c91, plain,
% 5.92/1.10  	~system_indi_needs_level(system,X21,X25),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a80, a81, a82])], [c82, c90])).
% 5.92/1.10  cnf(c92, plain,
% 5.92/1.10  	~system_indi_has_citizenship(system,X53,X54),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a80, a81, a82])], [c82, c90])).
% 5.92/1.10  
% 5.92/1.10  cnf(c93, axiom,
% 5.92/1.10  	system_indi_has_citizenship(system,alice,usa)).
% 5.92/1.10  cnf(a83, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a84, assumption,
% 5.92/1.10  	X53 = alice).
% 5.92/1.10  cnf(a85, assumption,
% 5.92/1.10  	X54 = usa).
% 5.92/1.10  cnf(c94, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a83, a84, a85])], [c92, c93])).
% 5.92/1.10  cnf(c95, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a83, a84, a85])], [c92, c93])).
% 5.92/1.10  
% 5.92/1.10  cnf(c96, axiom,
% 5.92/1.10  	system_indi_needs_level(system,alice,secret)).
% 5.92/1.10  cnf(a86, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a87, assumption,
% 5.92/1.10  	X21 = alice).
% 5.92/1.10  cnf(a88, assumption,
% 5.92/1.10  	X25 = secret).
% 5.92/1.10  cnf(c97, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a86, a87, a88])], [c91, c96])).
% 5.92/1.10  cnf(c98, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a86, a87, a88])], [c91, c96])).
% 5.92/1.10  
% 5.92/1.10  cnf(c99, axiom,
% 5.92/1.10  	oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)).
% 5.92/1.10  cnf(a89, assumption,
% 5.92/1.10  	X17 = oca).
% 5.92/1.10  cnf(a90, assumption,
% 5.92/1.10  	X15 = compartmenta).
% 5.92/1.10  cnf(a91, assumption,
% 5.92/1.10  	X16 = sbu).
% 5.92/1.10  cnf(a92, assumption,
% 5.92/1.10  	X18 = unclassified).
% 5.92/1.10  cnf(a93, assumption,
% 5.92/1.10  	X19 = no).
% 5.92/1.10  cnf(a94, assumption,
% 5.92/1.10  	X20 = no).
% 5.92/1.10  cnf(c100, plain,
% 5.92/1.10  	~system_indi_is_oca(system,X17),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a89, a90, a91, a92, a93, a94])], [c21, c99])).
% 5.92/1.10  cnf(c101, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a89, a90, a91, a92, a93, a94])], [c21, c99])).
% 5.92/1.10  
% 5.92/1.10  cnf(c102, axiom,
% 5.92/1.10  	system_indi_is_oca(system,oca)).
% 5.92/1.10  cnf(a95, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a96, assumption,
% 5.92/1.10  	X17 = oca).
% 5.92/1.10  cnf(c103, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a95, a96])], [c100, c102])).
% 5.92/1.10  cnf(c104, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a95, a96])], [c100, c102])).
% 5.92/1.10  
% 5.92/1.10  cnf(c105, axiom,
% 5.92/1.10  	admin_indi_has_background_for_compartment(admin,X55,X56) | ~admin_indi_has_background(admin,X55,X57) | ~oca_compartment_is_compartment(X58,X56,X59,X57,X60,X61) | ~system_indi_is_oca(system,X58)).
% 5.92/1.10  cnf(a97, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a98, assumption,
% 5.92/1.10  	X9 = X55).
% 5.92/1.10  cnf(a99, assumption,
% 5.92/1.10  	X10 = X56).
% 5.92/1.10  cnf(c106, plain,
% 5.92/1.10  	~sso_indi_has_compartment(X12,X9,X10) | ~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a97, a98, a99])], [c18, c105])).
% 5.92/1.10  cnf(c107, plain,
% 5.92/1.10  	~admin_indi_has_background(admin,X55,X57) | ~oca_compartment_is_compartment(X58,X56,X59,X57,X60,X61) | ~system_indi_is_oca(system,X58),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a97, a98, a99])], [c18, c105])).
% 5.92/1.10  
% 5.92/1.10  cnf(c108, axiom,
% 5.92/1.10  	admin_indi_has_background(admin,X62,unclassified)).
% 5.92/1.10  cnf(a100, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a101, assumption,
% 5.92/1.10  	X55 = X62).
% 5.92/1.10  cnf(a102, assumption,
% 5.92/1.10  	X57 = unclassified).
% 5.92/1.10  cnf(c109, plain,
% 5.92/1.10  	~oca_compartment_is_compartment(X58,X56,X59,X57,X60,X61) | ~system_indi_is_oca(system,X58),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a100, a101, a102])], [c107, c108])).
% 5.92/1.10  cnf(c110, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a100, a101, a102])], [c107, c108])).
% 5.92/1.10  
% 5.92/1.10  cnf(c111, plain,
% 5.92/1.10  	oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20)).
% 5.92/1.10  cnf(a103, assumption,
% 5.92/1.10  	X58 = X17).
% 5.92/1.10  cnf(a104, assumption,
% 5.92/1.10  	X56 = X15).
% 5.92/1.10  cnf(a105, assumption,
% 5.92/1.10  	X59 = X16).
% 5.92/1.10  cnf(a106, assumption,
% 5.92/1.10  	X57 = X18).
% 5.92/1.10  cnf(a107, assumption,
% 5.92/1.10  	X60 = X19).
% 5.92/1.10  cnf(a108, assumption,
% 5.92/1.10  	X61 = X20).
% 5.92/1.10  cnf(c112, plain,
% 5.92/1.10  	~system_indi_is_oca(system,X58),
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a103, a104, a105, a106, a107, a108])], [c109, c111])).
% 5.92/1.10  
% 5.92/1.10  cnf(c113, plain,
% 5.92/1.10  	system_indi_is_oca(system,X17)).
% 5.92/1.10  cnf(a109, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a110, assumption,
% 5.92/1.10  	X58 = X17).
% 5.92/1.10  cnf(c114, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a109, a110])], [c112, c113])).
% 5.92/1.10  
% 5.92/1.10  cnf(c115, axiom,
% 5.92/1.10  	sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)).
% 5.92/1.10  cnf(a111, assumption,
% 5.92/1.10  	X12 = sso_compartmenta).
% 5.92/1.10  cnf(a112, assumption,
% 5.92/1.10  	X9 = alice).
% 5.92/1.10  cnf(a113, assumption,
% 5.92/1.10  	X10 = compartmenta).
% 5.92/1.10  cnf(c116, plain,
% 5.92/1.10  	~admin_compartment_has_sso(admin,X10,X12) | ~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a111, a112, a113])], [c106, c115])).
% 5.92/1.10  cnf(c117, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a111, a112, a113])], [c106, c115])).
% 5.92/1.10  
% 5.92/1.10  cnf(c118, axiom,
% 5.92/1.10  	admin_compartment_has_sso(admin,X63,X64) | ~system_compartment_has_sso(system,X63,X64)).
% 5.92/1.10  cnf(a114, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a115, assumption,
% 5.92/1.10  	X10 = X63).
% 5.92/1.10  cnf(a116, assumption,
% 5.92/1.10  	X12 = X64).
% 5.92/1.10  cnf(c119, plain,
% 5.92/1.10  	~admin_indi_has_credit_for_compartment(admin,X9,X10) | ~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a114, a115, a116])], [c116, c118])).
% 5.92/1.10  cnf(c120, plain,
% 5.92/1.10  	~system_compartment_has_sso(system,X63,X64),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a114, a115, a116])], [c116, c118])).
% 5.92/1.10  
% 5.92/1.10  cnf(c121, axiom,
% 5.92/1.10  	system_compartment_has_sso(system,compartmenta,sso_compartmenta)).
% 5.92/1.10  cnf(a117, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a118, assumption,
% 5.92/1.10  	X63 = compartmenta).
% 5.92/1.10  cnf(a119, assumption,
% 5.92/1.10  	X64 = sso_compartmenta).
% 5.92/1.10  cnf(c122, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a117, a118, a119])], [c120, c121])).
% 5.92/1.10  cnf(c123, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a117, a118, a119])], [c120, c121])).
% 5.92/1.10  
% 5.92/1.10  cnf(c124, axiom,
% 5.92/1.10  	admin_indi_has_credit_for_compartment(admin,X65,X66) | ~oca_compartment_is_compartment(X67,X66,X68,X69,no,X70) | ~system_indi_is_oca(system,X67)).
% 5.92/1.10  cnf(a120, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a121, assumption,
% 5.92/1.10  	X9 = X65).
% 5.92/1.10  cnf(a122, assumption,
% 5.92/1.10  	X10 = X66).
% 5.92/1.10  cnf(c125, plain,
% 5.92/1.10  	~admin_indi_has_polygraph_for_compartment(admin,X9,X10) | ~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a120, a121, a122])], [c119, c124])).
% 5.92/1.10  cnf(c126, plain,
% 5.92/1.10  	~oca_compartment_is_compartment(X67,X66,X68,X69,no,X70) | ~system_indi_is_oca(system,X67),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a120, a121, a122])], [c119, c124])).
% 5.92/1.10  
% 5.92/1.10  cnf(c127, plain,
% 5.92/1.10  	oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20)).
% 5.92/1.10  cnf(a123, assumption,
% 5.92/1.10  	X67 = X17).
% 5.92/1.10  cnf(a124, assumption,
% 5.92/1.10  	X66 = X15).
% 5.92/1.10  cnf(a125, assumption,
% 5.92/1.10  	X68 = X16).
% 5.92/1.10  cnf(a126, assumption,
% 5.92/1.10  	X69 = X18).
% 5.92/1.10  cnf(a127, assumption,
% 5.92/1.10  	no = X19).
% 5.92/1.10  cnf(a128, assumption,
% 5.92/1.10  	X70 = X20).
% 5.92/1.10  cnf(c128, plain,
% 5.92/1.10  	~system_indi_is_oca(system,X67),
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a123, a124, a125, a126, a127, a128])], [c126, c127])).
% 5.92/1.10  
% 5.92/1.10  cnf(c129, plain,
% 5.92/1.10  	system_indi_is_oca(system,X17)).
% 5.92/1.10  cnf(a129, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a130, assumption,
% 5.92/1.10  	X67 = X17).
% 5.92/1.10  cnf(c130, plain,
% 5.92/1.10  	$false,
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a129, a130])], [c128, c129])).
% 5.92/1.10  
% 5.92/1.10  cnf(c131, axiom,
% 5.92/1.10  	admin_indi_has_polygraph_for_compartment(admin,X71,X72) | ~oca_compartment_is_compartment(X73,X72,X74,X75,X76,no) | ~system_indi_is_oca(system,X73)).
% 5.92/1.10  cnf(a131, assumption,
% 5.92/1.10  	admin = admin).
% 5.92/1.10  cnf(a132, assumption,
% 5.92/1.10  	X9 = X71).
% 5.92/1.10  cnf(a133, assumption,
% 5.92/1.10  	X10 = X72).
% 5.92/1.10  cnf(c132, plain,
% 5.92/1.10  	~admin_indi_has_citizenship(admin,X9,usa) | ~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a131, a132, a133])], [c125, c131])).
% 5.92/1.10  cnf(c133, plain,
% 5.92/1.10  	~oca_compartment_is_compartment(X73,X72,X74,X75,X76,no) | ~system_indi_is_oca(system,X73),
% 5.92/1.10  	inference(strict_predicate_extension, [assumptions([a131, a132, a133])], [c125, c131])).
% 5.92/1.10  
% 5.92/1.10  cnf(c134, plain,
% 5.92/1.10  	oca_compartment_is_compartment(X17,X15,X16,X18,X19,X20)).
% 5.92/1.10  cnf(a134, assumption,
% 5.92/1.10  	X73 = X17).
% 5.92/1.10  cnf(a135, assumption,
% 5.92/1.10  	X72 = X15).
% 5.92/1.10  cnf(a136, assumption,
% 5.92/1.10  	X74 = X16).
% 5.92/1.10  cnf(a137, assumption,
% 5.92/1.10  	X75 = X18).
% 5.92/1.10  cnf(a138, assumption,
% 5.92/1.10  	X76 = X19).
% 5.92/1.10  cnf(a139, assumption,
% 5.92/1.10  	no = X20).
% 5.92/1.10  cnf(c135, plain,
% 5.92/1.10  	~system_indi_is_oca(system,X73),
% 5.92/1.10  	inference(predicate_reduction, [assumptions([a134, a135, a136, a137, a138, a139])], [c133, c134])).
% 5.92/1.10  
% 5.92/1.10  cnf(c136, plain,
% 5.92/1.10  	system_indi_is_oca(system,X17)).
% 5.92/1.10  cnf(a140, assumption,
% 5.92/1.10  	system = system).
% 5.92/1.10  cnf(a141, assumption,
% 5.92/1.10  	X73 = X17).
% 5.92/1.10  cnf(c137, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a140, a141])], [c135, c136])).
% 5.92/1.11  
% 5.92/1.11  cnf(c138, plain,
% 5.92/1.11  	admin_indi_has_citizenship(admin,X21,usa)).
% 5.92/1.11  cnf(a142, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a143, assumption,
% 5.92/1.11  	X9 = X21).
% 5.92/1.11  cnf(a144, assumption,
% 5.92/1.11  	usa = usa).
% 5.92/1.11  cnf(c139, plain,
% 5.92/1.11  	~admin_indi_has_employment(admin,X9) | ~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a142, a143, a144])], [c132, c138])).
% 5.92/1.11  
% 5.92/1.11  cnf(c140, plain,
% 5.92/1.11  	admin_indi_has_employment(admin,X21)).
% 5.92/1.11  cnf(a145, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a146, assumption,
% 5.92/1.11  	X9 = X21).
% 5.92/1.11  cnf(c141, plain,
% 5.92/1.11  	~system_indi_needs_compartment(system,X9,X10),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a145, a146])], [c139, c140])).
% 5.92/1.11  
% 5.92/1.11  cnf(c142, axiom,
% 5.92/1.11  	system_indi_needs_compartment(system,alice,compartmenta)).
% 5.92/1.11  cnf(a147, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a148, assumption,
% 5.92/1.11  	X9 = alice).
% 5.92/1.11  cnf(a149, assumption,
% 5.92/1.11  	X10 = compartmenta).
% 5.92/1.11  cnf(c143, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a147, a148, a149])], [c141, c142])).
% 5.92/1.11  cnf(c144, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a147, a148, a149])], [c141, c142])).
% 5.92/1.11  
% 5.92/1.11  cnf(c145, axiom,
% 5.92/1.11  	admin_indi_has_level_for_compartment(admin,X77,X78) | ~admin_indi_has_level(admin,X77,X79) | ~oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83) | ~system_indi_is_oca(system,X80)).
% 5.92/1.11  cnf(a150, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a151, assumption,
% 5.92/1.11  	X5 = X77).
% 5.92/1.11  cnf(a152, assumption,
% 5.92/1.11  	X6 = X78).
% 5.92/1.11  cnf(c146, plain,
% 5.92/1.11  	~admin_indi_has_background_for_compartment(admin,X5,X6) | ~sso_indi_has_compartment(X8,X5,X6) | ~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a150, a151, a152])], [c12, c145])).
% 5.92/1.11  cnf(c147, plain,
% 5.92/1.11  	~admin_indi_has_level(admin,X77,X79) | ~oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83) | ~system_indi_is_oca(system,X80),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a150, a151, a152])], [c12, c145])).
% 5.92/1.11  
% 5.92/1.11  cnf(c148, axiom,
% 5.92/1.11  	admin_indi_has_level(admin,X84,X85) | ~admin_indi_has_background(admin,X84,X85) | ~loca_level_below(admin,X85,X86) | ~level_admin_indi_has_level(X87,X84,X86) | ~system_indi_is_level_admin(system,X87) | ~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88)).
% 5.92/1.11  cnf(a153, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a154, assumption,
% 5.92/1.11  	X77 = X84).
% 5.92/1.11  cnf(a155, assumption,
% 5.92/1.11  	X79 = X85).
% 5.92/1.11  cnf(c149, plain,
% 5.92/1.11  	~oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83) | ~system_indi_is_oca(system,X80),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a153, a154, a155])], [c147, c148])).
% 5.92/1.11  cnf(c150, plain,
% 5.92/1.11  	~admin_indi_has_background(admin,X84,X85) | ~loca_level_below(admin,X85,X86) | ~level_admin_indi_has_level(X87,X84,X86) | ~system_indi_is_level_admin(system,X87) | ~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a153, a154, a155])], [c147, c148])).
% 5.92/1.11  
% 5.92/1.11  cnf(c151, axiom,
% 5.92/1.11  	admin_indi_has_background(admin,X89,X90) | ~loca_level_below(admin,X90,X91) | ~background_admin_indi_has_background(X92,X89,X91) | ~system_indi_is_background_admin(system,X92)).
% 5.92/1.11  cnf(a156, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a157, assumption,
% 5.92/1.11  	X84 = X89).
% 5.92/1.11  cnf(a158, assumption,
% 5.92/1.11  	X85 = X90).
% 5.92/1.11  cnf(c152, plain,
% 5.92/1.11  	~loca_level_below(admin,X85,X86) | ~level_admin_indi_has_level(X87,X84,X86) | ~system_indi_is_level_admin(system,X87) | ~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a156, a157, a158])], [c150, c151])).
% 5.92/1.11  cnf(c153, plain,
% 5.92/1.11  	~loca_level_below(admin,X90,X91) | ~background_admin_indi_has_background(X92,X89,X91) | ~system_indi_is_background_admin(system,X92),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a156, a157, a158])], [c150, c151])).
% 5.92/1.11  
% 5.92/1.11  cnf(c154, axiom,
% 5.92/1.11  	loca_level_below(X93,X94,X95) | ~loca_level_below(X93,X94,X96) | ~loca_level_direct_below(X93,X96,X95)).
% 5.92/1.11  cnf(a159, assumption,
% 5.92/1.11  	admin = X93).
% 5.92/1.11  cnf(a160, assumption,
% 5.92/1.11  	X90 = X94).
% 5.92/1.11  cnf(a161, assumption,
% 5.92/1.11  	X91 = X95).
% 5.92/1.11  cnf(c155, plain,
% 5.92/1.11  	~background_admin_indi_has_background(X92,X89,X91) | ~system_indi_is_background_admin(system,X92),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a159, a160, a161])], [c153, c154])).
% 5.92/1.11  cnf(c156, plain,
% 5.92/1.11  	~loca_level_below(X93,X94,X96) | ~loca_level_direct_below(X93,X96,X95),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a159, a160, a161])], [c153, c154])).
% 5.92/1.11  
% 5.92/1.11  cnf(c157, axiom,
% 5.92/1.11  	loca_level_below(X97,X98,X99) | ~loca_level_below(X97,X98,X100) | ~loca_level_direct_below(X97,X100,X99)).
% 5.92/1.11  cnf(a162, assumption,
% 5.92/1.11  	X93 = X97).
% 5.92/1.11  cnf(a163, assumption,
% 5.92/1.11  	X94 = X98).
% 5.92/1.11  cnf(a164, assumption,
% 5.92/1.11  	X96 = X99).
% 5.92/1.11  cnf(c158, plain,
% 5.92/1.11  	~loca_level_direct_below(X93,X96,X95),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a162, a163, a164])], [c156, c157])).
% 5.92/1.11  cnf(c159, plain,
% 5.92/1.11  	~loca_level_below(X97,X98,X100) | ~loca_level_direct_below(X97,X100,X99),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a162, a163, a164])], [c156, c157])).
% 5.92/1.11  
% 5.92/1.11  cnf(c160, axiom,
% 5.92/1.11  	loca_level_below(X101,X102,X102)).
% 5.92/1.11  cnf(a165, assumption,
% 5.92/1.11  	X97 = X101).
% 5.92/1.11  cnf(a166, assumption,
% 5.92/1.11  	X98 = X102).
% 5.92/1.11  cnf(a167, assumption,
% 5.92/1.11  	X100 = X102).
% 5.92/1.11  cnf(c161, plain,
% 5.92/1.11  	~loca_level_direct_below(X97,X100,X99),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a165, a166, a167])], [c159, c160])).
% 5.92/1.11  cnf(c162, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a165, a166, a167])], [c159, c160])).
% 5.92/1.11  
% 5.92/1.11  cnf(c163, plain,
% 5.92/1.11  	loca_level_direct_below(X34,X37,X36)).
% 5.92/1.11  cnf(a168, assumption,
% 5.92/1.11  	X97 = X34).
% 5.92/1.11  cnf(a169, assumption,
% 5.92/1.11  	X100 = X37).
% 5.92/1.11  cnf(a170, assumption,
% 5.92/1.11  	X99 = X36).
% 5.92/1.11  cnf(c164, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a168, a169, a170])], [c161, c163])).
% 5.92/1.11  
% 5.92/1.11  cnf(c165, plain,
% 5.92/1.11  	loca_level_direct_below(X30,X33,X32)).
% 5.92/1.11  cnf(a171, assumption,
% 5.92/1.11  	X93 = X30).
% 5.92/1.11  cnf(a172, assumption,
% 5.92/1.11  	X96 = X33).
% 5.92/1.11  cnf(a173, assumption,
% 5.92/1.11  	X95 = X32).
% 5.92/1.11  cnf(c166, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a171, a172, a173])], [c158, c165])).
% 5.92/1.11  
% 5.92/1.11  cnf(c167, plain,
% 5.92/1.11  	background_admin_indi_has_background(X29,X26,X28)).
% 5.92/1.11  cnf(a174, assumption,
% 5.92/1.11  	X92 = X29).
% 5.92/1.11  cnf(a175, assumption,
% 5.92/1.11  	X89 = X26).
% 5.92/1.11  cnf(a176, assumption,
% 5.92/1.11  	X91 = X28).
% 5.92/1.11  cnf(c168, plain,
% 5.92/1.11  	~system_indi_is_background_admin(system,X92),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a174, a175, a176])], [c155, c167])).
% 5.92/1.11  
% 5.92/1.11  cnf(c169, plain,
% 5.92/1.11  	system_indi_is_background_admin(system,X29)).
% 5.92/1.11  cnf(a177, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a178, assumption,
% 5.92/1.11  	X92 = X29).
% 5.92/1.11  cnf(c170, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a177, a178])], [c168, c169])).
% 5.92/1.11  
% 5.92/1.11  cnf(c171, plain,
% 5.92/1.11  	loca_level_below(admin,X90,X91)).
% 5.92/1.11  cnf(a179, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a180, assumption,
% 5.92/1.11  	X85 = X90).
% 5.92/1.11  cnf(a181, assumption,
% 5.92/1.11  	X86 = X91).
% 5.92/1.11  cnf(c172, plain,
% 5.92/1.11  	~level_admin_indi_has_level(X87,X84,X86) | ~system_indi_is_level_admin(system,X87) | ~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a179, a180, a181])], [c152, c171])).
% 5.92/1.11  
% 5.92/1.11  cnf(c173, plain,
% 5.92/1.11  	level_admin_indi_has_level(X24,X21,X23)).
% 5.92/1.11  cnf(a182, assumption,
% 5.92/1.11  	X87 = X24).
% 5.92/1.11  cnf(a183, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(a184, assumption,
% 5.92/1.11  	X86 = X23).
% 5.92/1.11  cnf(c174, plain,
% 5.92/1.11  	~system_indi_is_level_admin(system,X87) | ~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a182, a183, a184])], [c172, c173])).
% 5.92/1.11  
% 5.92/1.11  cnf(c175, plain,
% 5.92/1.11  	system_indi_is_level_admin(system,X24)).
% 5.92/1.11  cnf(a185, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a186, assumption,
% 5.92/1.11  	X87 = X24).
% 5.92/1.11  cnf(c176, plain,
% 5.92/1.11  	~loca_level_below(admin,X85,X88) | ~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a185, a186])], [c174, c175])).
% 5.92/1.11  
% 5.92/1.11  cnf(c177, plain,
% 5.92/1.11  	loca_level_below(X93,X94,X96)).
% 5.92/1.11  cnf(a187, assumption,
% 5.92/1.11  	admin = X93).
% 5.92/1.11  cnf(a188, assumption,
% 5.92/1.11  	X85 = X94).
% 5.92/1.11  cnf(a189, assumption,
% 5.92/1.11  	X88 = X96).
% 5.92/1.11  cnf(c178, plain,
% 5.92/1.11  	~admin_indi_has_credit(admin,X84) | ~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a187, a188, a189])], [c176, c177])).
% 5.92/1.11  
% 5.92/1.11  cnf(c179, plain,
% 5.92/1.11  	admin_indi_has_credit(admin,X21)).
% 5.92/1.11  cnf(a190, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a191, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(c180, plain,
% 5.92/1.11  	~admin_indi_has_employment(admin,X84) | ~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a190, a191])], [c178, c179])).
% 5.92/1.11  
% 5.92/1.11  cnf(c181, plain,
% 5.92/1.11  	admin_indi_has_employment(admin,X21)).
% 5.92/1.11  cnf(a192, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a193, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(c182, plain,
% 5.92/1.11  	~admin_indi_has_polygraph(admin,X84) | ~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a192, a193])], [c180, c181])).
% 5.92/1.11  
% 5.92/1.11  cnf(c183, plain,
% 5.92/1.11  	admin_indi_has_polygraph(admin,X21)).
% 5.92/1.11  cnf(a194, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a195, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(c184, plain,
% 5.92/1.11  	~admin_indi_has_citizenship(admin,X84,usa) | ~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a194, a195])], [c182, c183])).
% 5.92/1.11  
% 5.92/1.11  cnf(c185, plain,
% 5.92/1.11  	admin_indi_has_citizenship(admin,X21,usa)).
% 5.92/1.11  cnf(a196, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a197, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(a198, assumption,
% 5.92/1.11  	usa = usa).
% 5.92/1.11  cnf(c186, plain,
% 5.92/1.11  	~system_indi_needs_level(system,X84,X88),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a196, a197, a198])], [c184, c185])).
% 5.92/1.11  
% 5.92/1.11  cnf(c187, plain,
% 5.92/1.11  	system_indi_needs_level(system,X21,X25)).
% 5.92/1.11  cnf(a199, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a200, assumption,
% 5.92/1.11  	X84 = X21).
% 5.92/1.11  cnf(a201, assumption,
% 5.92/1.11  	X88 = X25).
% 5.92/1.11  cnf(c188, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a199, a200, a201])], [c186, c187])).
% 5.92/1.11  
% 5.92/1.11  cnf(c189, axiom,
% 5.92/1.11  	oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)).
% 5.92/1.11  cnf(a202, assumption,
% 5.92/1.11  	X80 = oca).
% 5.92/1.11  cnf(a203, assumption,
% 5.92/1.11  	X78 = compartmentb).
% 5.92/1.11  cnf(a204, assumption,
% 5.92/1.11  	X79 = confidential).
% 5.92/1.11  cnf(a205, assumption,
% 5.92/1.11  	X81 = topsecret).
% 5.92/1.11  cnf(a206, assumption,
% 5.92/1.11  	X82 = yes).
% 5.92/1.11  cnf(a207, assumption,
% 5.92/1.11  	X83 = yes).
% 5.92/1.11  cnf(c190, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X80),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a202, a203, a204, a205, a206, a207])], [c149, c189])).
% 5.92/1.11  cnf(c191, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a202, a203, a204, a205, a206, a207])], [c149, c189])).
% 5.92/1.11  
% 5.92/1.11  cnf(c192, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a208, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a209, assumption,
% 5.92/1.11  	X80 = X17).
% 5.92/1.11  cnf(c193, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a208, a209])], [c190, c192])).
% 5.92/1.11  
% 5.92/1.11  cnf(c194, axiom,
% 5.92/1.11  	admin_indi_has_background_for_compartment(admin,X103,X104) | ~admin_indi_has_background(admin,X103,X105) | ~oca_compartment_is_compartment(X106,X104,X107,X105,X108,X109) | ~system_indi_is_oca(system,X106)).
% 5.92/1.11  cnf(a210, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a211, assumption,
% 5.92/1.11  	X5 = X103).
% 5.92/1.11  cnf(a212, assumption,
% 5.92/1.11  	X6 = X104).
% 5.92/1.11  cnf(c195, plain,
% 5.92/1.11  	~sso_indi_has_compartment(X8,X5,X6) | ~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a210, a211, a212])], [c146, c194])).
% 5.92/1.11  cnf(c196, plain,
% 5.92/1.11  	~admin_indi_has_background(admin,X103,X105) | ~oca_compartment_is_compartment(X106,X104,X107,X105,X108,X109) | ~system_indi_is_oca(system,X106),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a210, a211, a212])], [c146, c194])).
% 5.92/1.11  
% 5.92/1.11  cnf(c197, axiom,
% 5.92/1.11  	admin_indi_has_background(admin,X110,X111) | ~loca_level_below(admin,X111,X112) | ~background_admin_indi_has_background(X113,X110,X112) | ~system_indi_is_background_admin(system,X113)).
% 5.92/1.11  cnf(a213, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a214, assumption,
% 5.92/1.11  	X103 = X110).
% 5.92/1.11  cnf(a215, assumption,
% 5.92/1.11  	X105 = X111).
% 5.92/1.11  cnf(c198, plain,
% 5.92/1.11  	~oca_compartment_is_compartment(X106,X104,X107,X105,X108,X109) | ~system_indi_is_oca(system,X106),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a213, a214, a215])], [c196, c197])).
% 5.92/1.11  cnf(c199, plain,
% 5.92/1.11  	~loca_level_below(admin,X111,X112) | ~background_admin_indi_has_background(X113,X110,X112) | ~system_indi_is_background_admin(system,X113),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a213, a214, a215])], [c196, c197])).
% 5.92/1.11  
% 5.92/1.11  cnf(c200, axiom,
% 5.92/1.11  	loca_level_below(X114,X115,X115)).
% 5.92/1.11  cnf(a216, assumption,
% 5.92/1.11  	admin = X114).
% 5.92/1.11  cnf(a217, assumption,
% 5.92/1.11  	X111 = X115).
% 5.92/1.11  cnf(a218, assumption,
% 5.92/1.11  	X112 = X115).
% 5.92/1.11  cnf(c201, plain,
% 5.92/1.11  	~background_admin_indi_has_background(X113,X110,X112) | ~system_indi_is_background_admin(system,X113),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a216, a217, a218])], [c199, c200])).
% 5.92/1.11  cnf(c202, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a216, a217, a218])], [c199, c200])).
% 5.92/1.11  
% 5.92/1.11  cnf(c203, plain,
% 5.92/1.11  	background_admin_indi_has_background(X29,X26,X28)).
% 5.92/1.11  cnf(a219, assumption,
% 5.92/1.11  	X113 = X29).
% 5.92/1.11  cnf(a220, assumption,
% 5.92/1.11  	X110 = X26).
% 5.92/1.11  cnf(a221, assumption,
% 5.92/1.11  	X112 = X28).
% 5.92/1.11  cnf(c204, plain,
% 5.92/1.11  	~system_indi_is_background_admin(system,X113),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a219, a220, a221])], [c201, c203])).
% 5.92/1.11  
% 5.92/1.11  cnf(c205, plain,
% 5.92/1.11  	system_indi_is_background_admin(system,X29)).
% 5.92/1.11  cnf(a222, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a223, assumption,
% 5.92/1.11  	X113 = X29).
% 5.92/1.11  cnf(c206, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a222, a223])], [c204, c205])).
% 5.92/1.11  
% 5.92/1.11  cnf(c207, plain,
% 5.92/1.11  	oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83)).
% 5.92/1.11  cnf(a224, assumption,
% 5.92/1.11  	X106 = X80).
% 5.92/1.11  cnf(a225, assumption,
% 5.92/1.11  	X104 = X78).
% 5.92/1.11  cnf(a226, assumption,
% 5.92/1.11  	X107 = X79).
% 5.92/1.11  cnf(a227, assumption,
% 5.92/1.11  	X105 = X81).
% 5.92/1.11  cnf(a228, assumption,
% 5.92/1.11  	X108 = X82).
% 5.92/1.11  cnf(a229, assumption,
% 5.92/1.11  	X109 = X83).
% 5.92/1.11  cnf(c208, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X106),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a224, a225, a226, a227, a228, a229])], [c198, c207])).
% 5.92/1.11  
% 5.92/1.11  cnf(c209, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a230, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a231, assumption,
% 5.92/1.11  	X106 = X17).
% 5.92/1.11  cnf(c210, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a230, a231])], [c208, c209])).
% 5.92/1.11  
% 5.92/1.11  cnf(c211, axiom,
% 5.92/1.11  	sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)).
% 5.92/1.11  cnf(a232, assumption,
% 5.92/1.11  	X8 = sso_compartmentb).
% 5.92/1.11  cnf(a233, assumption,
% 5.92/1.11  	X5 = alice).
% 5.92/1.11  cnf(a234, assumption,
% 5.92/1.11  	X6 = compartmentb).
% 5.92/1.11  cnf(c212, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X6,X8) | ~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a232, a233, a234])], [c195, c211])).
% 5.92/1.11  cnf(c213, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a232, a233, a234])], [c195, c211])).
% 5.92/1.11  
% 5.92/1.11  cnf(c214, axiom,
% 5.92/1.11  	admin_compartment_has_sso(admin,X116,X117) | ~system_compartment_has_sso(system,X116,X117)).
% 5.92/1.11  cnf(a235, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a236, assumption,
% 5.92/1.11  	X6 = X116).
% 5.92/1.11  cnf(a237, assumption,
% 5.92/1.11  	X8 = X117).
% 5.92/1.11  cnf(c215, plain,
% 5.92/1.11  	~admin_indi_has_credit_for_compartment(admin,X5,X6) | ~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a235, a236, a237])], [c212, c214])).
% 5.92/1.11  cnf(c216, plain,
% 5.92/1.11  	~system_compartment_has_sso(system,X116,X117),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a235, a236, a237])], [c212, c214])).
% 5.92/1.11  
% 5.92/1.11  cnf(c217, axiom,
% 5.92/1.11  	system_compartment_has_sso(system,compartmentb,sso_compartmentb)).
% 5.92/1.11  cnf(a238, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a239, assumption,
% 5.92/1.11  	X116 = compartmentb).
% 5.92/1.11  cnf(a240, assumption,
% 5.92/1.11  	X117 = sso_compartmentb).
% 5.92/1.11  cnf(c218, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a238, a239, a240])], [c216, c217])).
% 5.92/1.11  cnf(c219, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a238, a239, a240])], [c216, c217])).
% 5.92/1.11  
% 5.92/1.11  cnf(c220, axiom,
% 5.92/1.11  	admin_indi_has_credit_for_compartment(admin,X118,X119) | ~admin_indi_has_credit(admin,X118) | ~oca_compartment_is_compartment(X120,X119,X121,X122,yes,X123) | ~system_indi_is_oca(system,X120)).
% 5.92/1.11  cnf(a241, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a242, assumption,
% 5.92/1.11  	X5 = X118).
% 5.92/1.11  cnf(a243, assumption,
% 5.92/1.11  	X6 = X119).
% 5.92/1.11  cnf(c221, plain,
% 5.92/1.11  	~admin_indi_has_polygraph_for_compartment(admin,X5,X6) | ~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a241, a242, a243])], [c215, c220])).
% 5.92/1.11  cnf(c222, plain,
% 5.92/1.11  	~admin_indi_has_credit(admin,X118) | ~oca_compartment_is_compartment(X120,X119,X121,X122,yes,X123) | ~system_indi_is_oca(system,X120),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a241, a242, a243])], [c215, c220])).
% 5.92/1.11  
% 5.92/1.11  cnf(c223, plain,
% 5.92/1.11  	admin_indi_has_credit(admin,X21)).
% 5.92/1.11  cnf(a244, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a245, assumption,
% 5.92/1.11  	X118 = X21).
% 5.92/1.11  cnf(c224, plain,
% 5.92/1.11  	~oca_compartment_is_compartment(X120,X119,X121,X122,yes,X123) | ~system_indi_is_oca(system,X120),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a244, a245])], [c222, c223])).
% 5.92/1.11  
% 5.92/1.11  cnf(c225, plain,
% 5.92/1.11  	oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83)).
% 5.92/1.11  cnf(a246, assumption,
% 5.92/1.11  	X120 = X80).
% 5.92/1.11  cnf(a247, assumption,
% 5.92/1.11  	X119 = X78).
% 5.92/1.11  cnf(a248, assumption,
% 5.92/1.11  	X121 = X79).
% 5.92/1.11  cnf(a249, assumption,
% 5.92/1.11  	X122 = X81).
% 5.92/1.11  cnf(a250, assumption,
% 5.92/1.11  	yes = X82).
% 5.92/1.11  cnf(a251, assumption,
% 5.92/1.11  	X123 = X83).
% 5.92/1.11  cnf(c226, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X120),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a246, a247, a248, a249, a250, a251])], [c224, c225])).
% 5.92/1.11  
% 5.92/1.11  cnf(c227, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a252, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a253, assumption,
% 5.92/1.11  	X120 = X17).
% 5.92/1.11  cnf(c228, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a252, a253])], [c226, c227])).
% 5.92/1.11  
% 5.92/1.11  cnf(c229, axiom,
% 5.92/1.11  	admin_indi_has_polygraph_for_compartment(admin,X124,X125) | ~admin_indi_has_polygraph(admin,X124) | ~oca_compartment_is_compartment(X126,X125,X127,X128,X129,yes) | ~system_indi_is_oca(system,X126)).
% 5.92/1.11  cnf(a254, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a255, assumption,
% 5.92/1.11  	X5 = X124).
% 5.92/1.11  cnf(a256, assumption,
% 5.92/1.11  	X6 = X125).
% 5.92/1.11  cnf(c230, plain,
% 5.92/1.11  	~admin_indi_has_citizenship(admin,X5,usa) | ~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a254, a255, a256])], [c221, c229])).
% 5.92/1.11  cnf(c231, plain,
% 5.92/1.11  	~admin_indi_has_polygraph(admin,X124) | ~oca_compartment_is_compartment(X126,X125,X127,X128,X129,yes) | ~system_indi_is_oca(system,X126),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a254, a255, a256])], [c221, c229])).
% 5.92/1.11  
% 5.92/1.11  cnf(c232, plain,
% 5.92/1.11  	admin_indi_has_polygraph(admin,X21)).
% 5.92/1.11  cnf(a257, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a258, assumption,
% 5.92/1.11  	X124 = X21).
% 5.92/1.11  cnf(c233, plain,
% 5.92/1.11  	~oca_compartment_is_compartment(X126,X125,X127,X128,X129,yes) | ~system_indi_is_oca(system,X126),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a257, a258])], [c231, c232])).
% 5.92/1.11  
% 5.92/1.11  cnf(c234, plain,
% 5.92/1.11  	oca_compartment_is_compartment(X80,X78,X79,X81,X82,X83)).
% 5.92/1.11  cnf(a259, assumption,
% 5.92/1.11  	X126 = X80).
% 5.92/1.11  cnf(a260, assumption,
% 5.92/1.11  	X125 = X78).
% 5.92/1.11  cnf(a261, assumption,
% 5.92/1.11  	X127 = X79).
% 5.92/1.11  cnf(a262, assumption,
% 5.92/1.11  	X128 = X81).
% 5.92/1.11  cnf(a263, assumption,
% 5.92/1.11  	X129 = X82).
% 5.92/1.11  cnf(a264, assumption,
% 5.92/1.11  	yes = X83).
% 5.92/1.11  cnf(c235, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X126),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a259, a260, a261, a262, a263, a264])], [c233, c234])).
% 5.92/1.11  
% 5.92/1.11  cnf(c236, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a265, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a266, assumption,
% 5.92/1.11  	X126 = X17).
% 5.92/1.11  cnf(c237, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a265, a266])], [c235, c236])).
% 5.92/1.11  
% 5.92/1.11  cnf(c238, plain,
% 5.92/1.11  	admin_indi_has_citizenship(admin,X21,usa)).
% 5.92/1.11  cnf(a267, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a268, assumption,
% 5.92/1.11  	X5 = X21).
% 5.92/1.11  cnf(a269, assumption,
% 5.92/1.11  	usa = usa).
% 5.92/1.11  cnf(c239, plain,
% 5.92/1.11  	~admin_indi_has_employment(admin,X5) | ~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a267, a268, a269])], [c230, c238])).
% 5.92/1.11  
% 5.92/1.11  cnf(c240, plain,
% 5.92/1.11  	admin_indi_has_employment(admin,X21)).
% 5.92/1.11  cnf(a270, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a271, assumption,
% 5.92/1.11  	X5 = X21).
% 5.92/1.11  cnf(c241, plain,
% 5.92/1.11  	~system_indi_needs_compartment(system,X5,X6),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a270, a271])], [c239, c240])).
% 5.92/1.11  
% 5.92/1.11  cnf(c242, axiom,
% 5.92/1.11  	system_indi_needs_compartment(system,alice,compartmentb)).
% 5.92/1.11  cnf(a272, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a273, assumption,
% 5.92/1.11  	X5 = alice).
% 5.92/1.11  cnf(a274, assumption,
% 5.92/1.11  	X6 = compartmentb).
% 5.92/1.11  cnf(c243, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a272, a273, a274])], [c241, c242])).
% 5.92/1.11  cnf(c244, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a272, a273, a274])], [c241, c242])).
% 5.92/1.11  
% 5.92/1.11  cnf(c245, axiom,
% 5.92/1.11  	admin_file_has_compartments(admin,X130,X131) | ~admin_file_has_compartments_h(admin,X130,X131,X131) | ~system_file_needs_compartments(system,X130,X131)).
% 5.92/1.11  cnf(a275, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a276, assumption,
% 5.92/1.11  	X3 = X130).
% 5.92/1.11  cnf(a277, assumption,
% 5.92/1.11  	X4 = X131).
% 5.92/1.11  cnf(c246, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a275, a276, a277])], [c9, c245])).
% 5.92/1.11  cnf(c247, plain,
% 5.92/1.11  	~admin_file_has_compartments_h(admin,X130,X131,X131) | ~system_file_needs_compartments(system,X130,X131),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a275, a276, a277])], [c9, c245])).
% 5.92/1.11  
% 5.92/1.11  cnf(c248, axiom,
% 5.92/1.11  	admin_file_has_compartments_h(admin,X132,X133,cons(X134,X135)) | ~admin_file_has_compartments_h(admin,X132,X133,X135) | ~sso_file_has_compartments(X136,X132,X133) | ~admin_compartment_has_sso(admin,X134,X136)).
% 5.92/1.11  cnf(a278, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a279, assumption,
% 5.92/1.11  	X130 = X132).
% 5.92/1.11  cnf(a280, assumption,
% 5.92/1.11  	X131 = X133).
% 5.92/1.11  cnf(a281, assumption,
% 5.92/1.11  	X131 = cons(X134,X135)).
% 5.92/1.11  cnf(c249, plain,
% 5.92/1.11  	~system_file_needs_compartments(system,X130,X131),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a278, a279, a280, a281])], [c247, c248])).
% 5.92/1.11  cnf(c250, plain,
% 5.92/1.11  	~admin_file_has_compartments_h(admin,X132,X133,X135) | ~sso_file_has_compartments(X136,X132,X133) | ~admin_compartment_has_sso(admin,X134,X136),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a278, a279, a280, a281])], [c247, c248])).
% 5.92/1.11  
% 5.92/1.11  cnf(c251, axiom,
% 5.92/1.11  	admin_file_has_compartments_h(admin,X137,X138,cons(X139,X140)) | ~admin_file_has_compartments_h(admin,X137,X138,X140) | ~sso_file_has_compartments(X141,X137,X138) | ~admin_compartment_has_sso(admin,X139,X141)).
% 5.92/1.11  cnf(a282, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a283, assumption,
% 5.92/1.11  	X132 = X137).
% 5.92/1.11  cnf(a284, assumption,
% 5.92/1.11  	X133 = X138).
% 5.92/1.11  cnf(a285, assumption,
% 5.92/1.11  	X135 = cons(X139,X140)).
% 5.92/1.11  cnf(c252, plain,
% 5.92/1.11  	~sso_file_has_compartments(X136,X132,X133) | ~admin_compartment_has_sso(admin,X134,X136),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a282, a283, a284, a285])], [c250, c251])).
% 5.92/1.11  cnf(c253, plain,
% 5.92/1.11  	~admin_file_has_compartments_h(admin,X137,X138,X140) | ~sso_file_has_compartments(X141,X137,X138) | ~admin_compartment_has_sso(admin,X139,X141),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a282, a283, a284, a285])], [c250, c251])).
% 5.92/1.11  
% 5.92/1.11  cnf(c254, axiom,
% 5.92/1.11  	admin_file_has_compartments_h(admin,X142,X143,nil)).
% 5.92/1.11  cnf(a286, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a287, assumption,
% 5.92/1.11  	X137 = X142).
% 5.92/1.11  cnf(a288, assumption,
% 5.92/1.11  	X138 = X143).
% 5.92/1.11  cnf(a289, assumption,
% 5.92/1.11  	X140 = nil).
% 5.92/1.11  cnf(c255, plain,
% 5.92/1.11  	~sso_file_has_compartments(X141,X137,X138) | ~admin_compartment_has_sso(admin,X139,X141),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a286, a287, a288, a289])], [c253, c254])).
% 5.92/1.11  cnf(c256, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a286, a287, a288, a289])], [c253, c254])).
% 5.92/1.11  
% 5.92/1.11  cnf(c257, axiom,
% 5.92/1.11  	sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))).
% 5.92/1.11  cnf(a290, assumption,
% 5.92/1.11  	X141 = sso_compartmenta).
% 5.92/1.11  cnf(a291, assumption,
% 5.92/1.11  	X137 = secretfile).
% 5.92/1.11  cnf(a292, assumption,
% 5.92/1.11  	X138 = cons(compartmentb,cons(compartmenta,nil))).
% 5.92/1.11  cnf(c258, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X139,X141),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a290, a291, a292])], [c255, c257])).
% 5.92/1.11  cnf(c259, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a290, a291, a292])], [c255, c257])).
% 5.92/1.11  
% 5.92/1.11  cnf(c260, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X10,X12)).
% 5.92/1.11  cnf(a293, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a294, assumption,
% 5.92/1.11  	X139 = X10).
% 5.92/1.11  cnf(a295, assumption,
% 5.92/1.11  	X141 = X12).
% 5.92/1.11  cnf(c261, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a293, a294, a295])], [c258, c260])).
% 5.92/1.11  
% 5.92/1.11  cnf(c262, axiom,
% 5.92/1.11  	sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))).
% 5.92/1.11  cnf(a296, assumption,
% 5.92/1.11  	X136 = sso_compartmentb).
% 5.92/1.11  cnf(a297, assumption,
% 5.92/1.11  	X132 = secretfile).
% 5.92/1.11  cnf(a298, assumption,
% 5.92/1.11  	X133 = cons(compartmentb,cons(compartmenta,nil))).
% 5.92/1.11  cnf(c263, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X134,X136),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a296, a297, a298])], [c252, c262])).
% 5.92/1.11  cnf(c264, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a296, a297, a298])], [c252, c262])).
% 5.92/1.11  
% 5.92/1.11  cnf(c265, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X6,X8)).
% 5.92/1.11  cnf(a299, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a300, assumption,
% 5.92/1.11  	X134 = X6).
% 5.92/1.11  cnf(a301, assumption,
% 5.92/1.11  	X136 = X8).
% 5.92/1.11  cnf(c266, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a299, a300, a301])], [c263, c265])).
% 5.92/1.11  
% 5.92/1.11  cnf(c267, axiom,
% 5.92/1.11  	system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))).
% 5.92/1.11  cnf(a302, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a303, assumption,
% 5.92/1.11  	X130 = secretfile).
% 5.92/1.11  cnf(a304, assumption,
% 5.92/1.11  	X131 = cons(compartmentb,cons(compartmenta,nil))).
% 5.92/1.11  cnf(c268, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a302, a303, a304])], [c249, c267])).
% 5.92/1.11  cnf(c269, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a302, a303, a304])], [c249, c267])).
% 5.92/1.11  
% 5.92/1.11  cnf(c270, axiom,
% 5.92/1.11  	admin_indi_has_level_for_file(admin,X144,X145) | ~admin_indi_has_level(admin,X144,X146) | ~admin_file_has_level(admin,X145,X146)).
% 5.92/1.11  cnf(a305, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a306, assumption,
% 5.92/1.11  	X0 = X144).
% 5.92/1.11  cnf(a307, assumption,
% 5.92/1.11  	X1 = X145).
% 5.92/1.11  cnf(c271, plain,
% 5.92/1.11  	~admin_indi_has_need_to_know_for_file(admin,X0,X1) | ~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a305, a306, a307])], [c6, c270])).
% 5.92/1.11  cnf(c272, plain,
% 5.92/1.11  	~admin_indi_has_level(admin,X144,X146) | ~admin_file_has_level(admin,X145,X146),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a305, a306, a307])], [c6, c270])).
% 5.92/1.11  
% 5.92/1.11  cnf(c273, axiom,
% 5.92/1.11  	admin_indi_has_level(admin,X147,X148) | ~admin_indi_has_background(admin,X147,X148) | ~loca_level_below(admin,X148,X149) | ~level_admin_indi_has_level(X150,X147,X149) | ~system_indi_is_level_admin(system,X150) | ~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151)).
% 5.92/1.11  cnf(a308, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a309, assumption,
% 5.92/1.11  	X144 = X147).
% 5.92/1.11  cnf(a310, assumption,
% 5.92/1.11  	X146 = X148).
% 5.92/1.11  cnf(c274, plain,
% 5.92/1.11  	~admin_file_has_level(admin,X145,X146),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a308, a309, a310])], [c272, c273])).
% 5.92/1.11  cnf(c275, plain,
% 5.92/1.11  	~admin_indi_has_background(admin,X147,X148) | ~loca_level_below(admin,X148,X149) | ~level_admin_indi_has_level(X150,X147,X149) | ~system_indi_is_level_admin(system,X150) | ~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a308, a309, a310])], [c272, c273])).
% 5.92/1.11  
% 5.92/1.11  cnf(c276, axiom,
% 5.92/1.11  	admin_indi_has_background(admin,X152,X153) | ~loca_level_below(admin,X153,X154) | ~background_admin_indi_has_background(X155,X152,X154) | ~system_indi_is_background_admin(system,X155)).
% 5.92/1.11  cnf(a311, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a312, assumption,
% 5.92/1.11  	X147 = X152).
% 5.92/1.11  cnf(a313, assumption,
% 5.92/1.11  	X148 = X153).
% 5.92/1.11  cnf(c277, plain,
% 5.92/1.11  	~loca_level_below(admin,X148,X149) | ~level_admin_indi_has_level(X150,X147,X149) | ~system_indi_is_level_admin(system,X150) | ~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a311, a312, a313])], [c275, c276])).
% 5.92/1.11  cnf(c278, plain,
% 5.92/1.11  	~loca_level_below(admin,X153,X154) | ~background_admin_indi_has_background(X155,X152,X154) | ~system_indi_is_background_admin(system,X155),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a311, a312, a313])], [c275, c276])).
% 5.92/1.11  
% 5.92/1.11  cnf(c279, axiom,
% 5.92/1.11  	loca_level_below(X156,X157,X158) | ~loca_level_below(X156,X157,X159) | ~loca_level_direct_below(X156,X159,X158)).
% 5.92/1.11  cnf(a314, assumption,
% 5.92/1.11  	admin = X156).
% 5.92/1.11  cnf(a315, assumption,
% 5.92/1.11  	X153 = X157).
% 5.92/1.11  cnf(a316, assumption,
% 5.92/1.11  	X154 = X158).
% 5.92/1.11  cnf(c280, plain,
% 5.92/1.11  	~background_admin_indi_has_background(X155,X152,X154) | ~system_indi_is_background_admin(system,X155),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a314, a315, a316])], [c278, c279])).
% 5.92/1.11  cnf(c281, plain,
% 5.92/1.11  	~loca_level_below(X156,X157,X159) | ~loca_level_direct_below(X156,X159,X158),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a314, a315, a316])], [c278, c279])).
% 5.92/1.11  
% 5.92/1.11  cnf(c282, axiom,
% 5.92/1.11  	loca_level_below(X160,X161,X161)).
% 5.92/1.11  cnf(a317, assumption,
% 5.92/1.11  	X156 = X160).
% 5.92/1.11  cnf(a318, assumption,
% 5.92/1.11  	X157 = X161).
% 5.92/1.11  cnf(a319, assumption,
% 5.92/1.11  	X159 = X161).
% 5.92/1.11  cnf(c283, plain,
% 5.92/1.11  	~loca_level_direct_below(X156,X159,X158),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a317, a318, a319])], [c281, c282])).
% 5.92/1.11  cnf(c284, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a317, a318, a319])], [c281, c282])).
% 5.92/1.11  
% 5.92/1.11  cnf(c285, plain,
% 5.92/1.11  	loca_level_direct_below(X30,X33,X32)).
% 5.92/1.11  cnf(a320, assumption,
% 5.92/1.11  	X156 = X30).
% 5.92/1.11  cnf(a321, assumption,
% 5.92/1.11  	X159 = X33).
% 5.92/1.11  cnf(a322, assumption,
% 5.92/1.11  	X158 = X32).
% 5.92/1.11  cnf(c286, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a320, a321, a322])], [c283, c285])).
% 5.92/1.11  
% 5.92/1.11  cnf(c287, plain,
% 5.92/1.11  	background_admin_indi_has_background(X29,X26,X28)).
% 5.92/1.11  cnf(a323, assumption,
% 5.92/1.11  	X155 = X29).
% 5.92/1.11  cnf(a324, assumption,
% 5.92/1.11  	X152 = X26).
% 5.92/1.11  cnf(a325, assumption,
% 5.92/1.11  	X154 = X28).
% 5.92/1.11  cnf(c288, plain,
% 5.92/1.11  	~system_indi_is_background_admin(system,X155),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a323, a324, a325])], [c280, c287])).
% 5.92/1.11  
% 5.92/1.11  cnf(c289, plain,
% 5.92/1.11  	system_indi_is_background_admin(system,X29)).
% 5.92/1.11  cnf(a326, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a327, assumption,
% 5.92/1.11  	X155 = X29).
% 5.92/1.11  cnf(c290, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a326, a327])], [c288, c289])).
% 5.92/1.11  
% 5.92/1.11  cnf(c291, plain,
% 5.92/1.11  	loca_level_below(admin,X153,X154)).
% 5.92/1.11  cnf(a328, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a329, assumption,
% 5.92/1.11  	X148 = X153).
% 5.92/1.11  cnf(a330, assumption,
% 5.92/1.11  	X149 = X154).
% 5.92/1.11  cnf(c292, plain,
% 5.92/1.11  	~level_admin_indi_has_level(X150,X147,X149) | ~system_indi_is_level_admin(system,X150) | ~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a328, a329, a330])], [c277, c291])).
% 5.92/1.11  
% 5.92/1.11  cnf(c293, plain,
% 5.92/1.11  	level_admin_indi_has_level(X24,X21,X23)).
% 5.92/1.11  cnf(a331, assumption,
% 5.92/1.11  	X150 = X24).
% 5.92/1.11  cnf(a332, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(a333, assumption,
% 5.92/1.11  	X149 = X23).
% 5.92/1.11  cnf(c294, plain,
% 5.92/1.11  	~system_indi_is_level_admin(system,X150) | ~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a331, a332, a333])], [c292, c293])).
% 5.92/1.11  
% 5.92/1.11  cnf(c295, plain,
% 5.92/1.11  	system_indi_is_level_admin(system,X24)).
% 5.92/1.11  cnf(a334, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a335, assumption,
% 5.92/1.11  	X150 = X24).
% 5.92/1.11  cnf(c296, plain,
% 5.92/1.11  	~loca_level_below(admin,X148,X151) | ~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a334, a335])], [c294, c295])).
% 5.92/1.11  
% 5.92/1.11  cnf(c297, plain,
% 5.92/1.11  	loca_level_below(X156,X157,X159)).
% 5.92/1.11  cnf(a336, assumption,
% 5.92/1.11  	admin = X156).
% 5.92/1.11  cnf(a337, assumption,
% 5.92/1.11  	X148 = X157).
% 5.92/1.11  cnf(a338, assumption,
% 5.92/1.11  	X151 = X159).
% 5.92/1.11  cnf(c298, plain,
% 5.92/1.11  	~admin_indi_has_credit(admin,X147) | ~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a336, a337, a338])], [c296, c297])).
% 5.92/1.11  
% 5.92/1.11  cnf(c299, plain,
% 5.92/1.11  	admin_indi_has_credit(admin,X21)).
% 5.92/1.11  cnf(a339, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a340, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(c300, plain,
% 5.92/1.11  	~admin_indi_has_employment(admin,X147) | ~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a339, a340])], [c298, c299])).
% 5.92/1.11  
% 5.92/1.11  cnf(c301, plain,
% 5.92/1.11  	admin_indi_has_employment(admin,X21)).
% 5.92/1.11  cnf(a341, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a342, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(c302, plain,
% 5.92/1.11  	~admin_indi_has_polygraph(admin,X147) | ~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a341, a342])], [c300, c301])).
% 5.92/1.11  
% 5.92/1.11  cnf(c303, plain,
% 5.92/1.11  	admin_indi_has_polygraph(admin,X21)).
% 5.92/1.11  cnf(a343, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a344, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(c304, plain,
% 5.92/1.11  	~admin_indi_has_citizenship(admin,X147,usa) | ~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a343, a344])], [c302, c303])).
% 5.92/1.11  
% 5.92/1.11  cnf(c305, plain,
% 5.92/1.11  	admin_indi_has_citizenship(admin,X21,usa)).
% 5.92/1.11  cnf(a345, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a346, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(a347, assumption,
% 5.92/1.11  	usa = usa).
% 5.92/1.11  cnf(c306, plain,
% 5.92/1.11  	~system_indi_needs_level(system,X147,X151),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a345, a346, a347])], [c304, c305])).
% 5.92/1.11  
% 5.92/1.11  cnf(c307, plain,
% 5.92/1.11  	system_indi_needs_level(system,X21,X25)).
% 5.92/1.11  cnf(a348, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a349, assumption,
% 5.92/1.11  	X147 = X21).
% 5.92/1.11  cnf(a350, assumption,
% 5.92/1.11  	X151 = X25).
% 5.92/1.11  cnf(c308, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a348, a349, a350])], [c306, c307])).
% 5.92/1.11  
% 5.92/1.11  cnf(c309, axiom,
% 5.92/1.11  	admin_file_has_level(admin,X162,X163) | ~admin_file_has_level_h(admin,X162,X163,X164) | ~admin_file_has_compartments(admin,X162,X164) | ~system_file_needs_level(system,X162,X163)).
% 5.92/1.11  cnf(a351, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a352, assumption,
% 5.92/1.11  	X145 = X162).
% 5.92/1.11  cnf(a353, assumption,
% 5.92/1.11  	X146 = X163).
% 5.92/1.11  cnf(c310, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a351, a352, a353])], [c274, c309])).
% 5.92/1.11  cnf(c311, plain,
% 5.92/1.11  	~admin_file_has_level_h(admin,X162,X163,X164) | ~admin_file_has_compartments(admin,X162,X164) | ~system_file_needs_level(system,X162,X163),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a351, a352, a353])], [c274, c309])).
% 5.92/1.11  
% 5.92/1.11  cnf(c312, axiom,
% 5.92/1.11  	admin_file_has_level_h(admin,X165,X166,cons(X167,X168)) | ~admin_file_has_level_h(admin,X165,X166,X168) | ~sso_file_has_level(X169,X165,X166,X170) | ~admin_compartment_has_scg(admin,X167,X170) | ~admin_compartment_has_sso(admin,X167,X169)).
% 5.92/1.11  cnf(a354, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a355, assumption,
% 5.92/1.11  	X162 = X165).
% 5.92/1.11  cnf(a356, assumption,
% 5.92/1.11  	X163 = X166).
% 5.92/1.11  cnf(a357, assumption,
% 5.92/1.11  	X164 = cons(X167,X168)).
% 5.92/1.11  cnf(c313, plain,
% 5.92/1.11  	~admin_file_has_compartments(admin,X162,X164) | ~system_file_needs_level(system,X162,X163),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a354, a355, a356, a357])], [c311, c312])).
% 5.92/1.11  cnf(c314, plain,
% 5.92/1.11  	~admin_file_has_level_h(admin,X165,X166,X168) | ~sso_file_has_level(X169,X165,X166,X170) | ~admin_compartment_has_scg(admin,X167,X170) | ~admin_compartment_has_sso(admin,X167,X169),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a354, a355, a356, a357])], [c311, c312])).
% 5.92/1.11  
% 5.92/1.11  cnf(c315, axiom,
% 5.92/1.11  	admin_file_has_level_h(admin,X171,X172,cons(X173,X174)) | ~admin_file_has_level_h(admin,X171,X172,X174) | ~sso_file_has_level(X175,X171,X172,X176) | ~admin_compartment_has_scg(admin,X173,X176) | ~admin_compartment_has_sso(admin,X173,X175)).
% 5.92/1.11  cnf(a358, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a359, assumption,
% 5.92/1.11  	X165 = X171).
% 5.92/1.11  cnf(a360, assumption,
% 5.92/1.11  	X166 = X172).
% 5.92/1.11  cnf(a361, assumption,
% 5.92/1.11  	X168 = cons(X173,X174)).
% 5.92/1.11  cnf(c316, plain,
% 5.92/1.11  	~sso_file_has_level(X169,X165,X166,X170) | ~admin_compartment_has_scg(admin,X167,X170) | ~admin_compartment_has_sso(admin,X167,X169),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a358, a359, a360, a361])], [c314, c315])).
% 5.92/1.11  cnf(c317, plain,
% 5.92/1.11  	~admin_file_has_level_h(admin,X171,X172,X174) | ~sso_file_has_level(X175,X171,X172,X176) | ~admin_compartment_has_scg(admin,X173,X176) | ~admin_compartment_has_sso(admin,X173,X175),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a358, a359, a360, a361])], [c314, c315])).
% 5.92/1.11  
% 5.92/1.11  cnf(c318, axiom,
% 5.92/1.11  	admin_file_has_level_h(admin,X177,X178,nil)).
% 5.92/1.11  cnf(a362, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a363, assumption,
% 5.92/1.11  	X171 = X177).
% 5.92/1.11  cnf(a364, assumption,
% 5.92/1.11  	X172 = X178).
% 5.92/1.11  cnf(a365, assumption,
% 5.92/1.11  	X174 = nil).
% 5.92/1.11  cnf(c319, plain,
% 5.92/1.11  	~sso_file_has_level(X175,X171,X172,X176) | ~admin_compartment_has_scg(admin,X173,X176) | ~admin_compartment_has_sso(admin,X173,X175),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a362, a363, a364, a365])], [c317, c318])).
% 5.92/1.11  cnf(c320, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a362, a363, a364, a365])], [c317, c318])).
% 5.92/1.11  
% 5.92/1.11  cnf(c321, axiom,
% 5.92/1.11  	sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta)).
% 5.92/1.11  cnf(a366, assumption,
% 5.92/1.11  	X175 = sso_compartmenta).
% 5.92/1.11  cnf(a367, assumption,
% 5.92/1.11  	X171 = secretfile).
% 5.92/1.11  cnf(a368, assumption,
% 5.92/1.11  	X172 = secret).
% 5.92/1.11  cnf(a369, assumption,
% 5.92/1.11  	X176 = scg_compartmenta).
% 5.92/1.11  cnf(c322, plain,
% 5.92/1.11  	~admin_compartment_has_scg(admin,X173,X176) | ~admin_compartment_has_sso(admin,X173,X175),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a366, a367, a368, a369])], [c319, c321])).
% 5.92/1.11  cnf(c323, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a366, a367, a368, a369])], [c319, c321])).
% 5.92/1.11  
% 5.92/1.11  cnf(c324, axiom,
% 5.92/1.11  	admin_compartment_has_scg(admin,X179,X180) | ~sso_compartment_has_scg(X181,X179,X180) | ~admin_compartment_has_sso(admin,X179,X181) | ~oca_compartment_has_scg(X182,X179,X180) | ~system_indi_is_oca(system,X182)).
% 5.92/1.11  cnf(a370, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a371, assumption,
% 5.92/1.11  	X173 = X179).
% 5.92/1.11  cnf(a372, assumption,
% 5.92/1.11  	X176 = X180).
% 5.92/1.11  cnf(c325, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X173,X175),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a370, a371, a372])], [c322, c324])).
% 5.92/1.11  cnf(c326, plain,
% 5.92/1.11  	~sso_compartment_has_scg(X181,X179,X180) | ~admin_compartment_has_sso(admin,X179,X181) | ~oca_compartment_has_scg(X182,X179,X180) | ~system_indi_is_oca(system,X182),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a370, a371, a372])], [c322, c324])).
% 5.92/1.11  
% 5.92/1.11  cnf(c327, axiom,
% 5.92/1.11  	sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta)).
% 5.92/1.11  cnf(a373, assumption,
% 5.92/1.11  	X181 = sso_compartmenta).
% 5.92/1.11  cnf(a374, assumption,
% 5.92/1.11  	X179 = compartmenta).
% 5.92/1.11  cnf(a375, assumption,
% 5.92/1.11  	X180 = scg_compartmenta).
% 5.92/1.11  cnf(c328, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X179,X181) | ~oca_compartment_has_scg(X182,X179,X180) | ~system_indi_is_oca(system,X182),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a373, a374, a375])], [c326, c327])).
% 5.92/1.11  cnf(c329, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a373, a374, a375])], [c326, c327])).
% 5.92/1.11  
% 5.92/1.11  cnf(c330, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X10,X12)).
% 5.92/1.11  cnf(a376, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a377, assumption,
% 5.92/1.11  	X179 = X10).
% 5.92/1.11  cnf(a378, assumption,
% 5.92/1.11  	X181 = X12).
% 5.92/1.11  cnf(c331, plain,
% 5.92/1.11  	~oca_compartment_has_scg(X182,X179,X180) | ~system_indi_is_oca(system,X182),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a376, a377, a378])], [c328, c330])).
% 5.92/1.11  
% 5.92/1.11  cnf(c332, axiom,
% 5.92/1.11  	oca_compartment_has_scg(oca,compartmenta,scg_compartmenta)).
% 5.92/1.11  cnf(a379, assumption,
% 5.92/1.11  	X182 = oca).
% 5.92/1.11  cnf(a380, assumption,
% 5.92/1.11  	X179 = compartmenta).
% 5.92/1.11  cnf(a381, assumption,
% 5.92/1.11  	X180 = scg_compartmenta).
% 5.92/1.11  cnf(c333, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X182),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a379, a380, a381])], [c331, c332])).
% 5.92/1.11  cnf(c334, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a379, a380, a381])], [c331, c332])).
% 5.92/1.11  
% 5.92/1.11  cnf(c335, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a382, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a383, assumption,
% 5.92/1.11  	X182 = X17).
% 5.92/1.11  cnf(c336, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a382, a383])], [c333, c335])).
% 5.92/1.11  
% 5.92/1.11  cnf(c337, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X10,X12)).
% 5.92/1.11  cnf(a384, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a385, assumption,
% 5.92/1.11  	X173 = X10).
% 5.92/1.11  cnf(a386, assumption,
% 5.92/1.11  	X175 = X12).
% 5.92/1.11  cnf(c338, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a384, a385, a386])], [c325, c337])).
% 5.92/1.11  
% 5.92/1.11  cnf(c339, axiom,
% 5.92/1.11  	sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb)).
% 5.92/1.11  cnf(a387, assumption,
% 5.92/1.11  	X169 = sso_compartmentb).
% 5.92/1.11  cnf(a388, assumption,
% 5.92/1.11  	X165 = secretfile).
% 5.92/1.11  cnf(a389, assumption,
% 5.92/1.11  	X166 = secret).
% 5.92/1.11  cnf(a390, assumption,
% 5.92/1.11  	X170 = scg_compartmentb).
% 5.92/1.11  cnf(c340, plain,
% 5.92/1.11  	~admin_compartment_has_scg(admin,X167,X170) | ~admin_compartment_has_sso(admin,X167,X169),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a387, a388, a389, a390])], [c316, c339])).
% 5.92/1.11  cnf(c341, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a387, a388, a389, a390])], [c316, c339])).
% 5.92/1.11  
% 5.92/1.11  cnf(c342, axiom,
% 5.92/1.11  	admin_compartment_has_scg(admin,X183,X184) | ~sso_compartment_has_scg(X185,X183,X184) | ~admin_compartment_has_sso(admin,X183,X185) | ~oca_compartment_has_scg(X186,X183,X184) | ~system_indi_is_oca(system,X186)).
% 5.92/1.11  cnf(a391, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a392, assumption,
% 5.92/1.11  	X167 = X183).
% 5.92/1.11  cnf(a393, assumption,
% 5.92/1.11  	X170 = X184).
% 5.92/1.11  cnf(c343, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X167,X169),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a391, a392, a393])], [c340, c342])).
% 5.92/1.11  cnf(c344, plain,
% 5.92/1.11  	~sso_compartment_has_scg(X185,X183,X184) | ~admin_compartment_has_sso(admin,X183,X185) | ~oca_compartment_has_scg(X186,X183,X184) | ~system_indi_is_oca(system,X186),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a391, a392, a393])], [c340, c342])).
% 5.92/1.11  
% 5.92/1.11  cnf(c345, axiom,
% 5.92/1.11  	sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb)).
% 5.92/1.11  cnf(a394, assumption,
% 5.92/1.11  	X185 = sso_compartmentb).
% 5.92/1.11  cnf(a395, assumption,
% 5.92/1.11  	X183 = compartmentb).
% 5.92/1.11  cnf(a396, assumption,
% 5.92/1.11  	X184 = scg_compartmentb).
% 5.92/1.11  cnf(c346, plain,
% 5.92/1.11  	~admin_compartment_has_sso(admin,X183,X185) | ~oca_compartment_has_scg(X186,X183,X184) | ~system_indi_is_oca(system,X186),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a394, a395, a396])], [c344, c345])).
% 5.92/1.11  cnf(c347, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a394, a395, a396])], [c344, c345])).
% 5.92/1.11  
% 5.92/1.11  cnf(c348, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X6,X8)).
% 5.92/1.11  cnf(a397, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a398, assumption,
% 5.92/1.11  	X183 = X6).
% 5.92/1.11  cnf(a399, assumption,
% 5.92/1.11  	X185 = X8).
% 5.92/1.11  cnf(c349, plain,
% 5.92/1.11  	~oca_compartment_has_scg(X186,X183,X184) | ~system_indi_is_oca(system,X186),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a397, a398, a399])], [c346, c348])).
% 5.92/1.11  
% 5.92/1.11  cnf(c350, axiom,
% 5.92/1.11  	oca_compartment_has_scg(oca,compartmentb,scg_compartmentb)).
% 5.92/1.11  cnf(a400, assumption,
% 5.92/1.11  	X186 = oca).
% 5.92/1.11  cnf(a401, assumption,
% 5.92/1.11  	X183 = compartmentb).
% 5.92/1.11  cnf(a402, assumption,
% 5.92/1.11  	X184 = scg_compartmentb).
% 5.92/1.11  cnf(c351, plain,
% 5.92/1.11  	~system_indi_is_oca(system,X186),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a400, a401, a402])], [c349, c350])).
% 5.92/1.11  cnf(c352, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a400, a401, a402])], [c349, c350])).
% 5.92/1.11  
% 5.92/1.11  cnf(c353, plain,
% 5.92/1.11  	system_indi_is_oca(system,X17)).
% 5.92/1.11  cnf(a403, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a404, assumption,
% 5.92/1.11  	X186 = X17).
% 5.92/1.11  cnf(c354, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a403, a404])], [c351, c353])).
% 5.92/1.11  
% 5.92/1.11  cnf(c355, plain,
% 5.92/1.11  	admin_compartment_has_sso(admin,X6,X8)).
% 5.92/1.11  cnf(a405, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a406, assumption,
% 5.92/1.11  	X167 = X6).
% 5.92/1.11  cnf(a407, assumption,
% 5.92/1.11  	X169 = X8).
% 5.92/1.11  cnf(c356, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a405, a406, a407])], [c343, c355])).
% 5.92/1.11  
% 5.92/1.11  cnf(c357, plain,
% 5.92/1.11  	admin_file_has_compartments(admin,X3,X4)).
% 5.92/1.11  cnf(a408, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a409, assumption,
% 5.92/1.11  	X162 = X3).
% 5.92/1.11  cnf(a410, assumption,
% 5.92/1.11  	X164 = X4).
% 5.92/1.11  cnf(c358, plain,
% 5.92/1.11  	~system_file_needs_level(system,X162,X163),
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a408, a409, a410])], [c313, c357])).
% 5.92/1.11  
% 5.92/1.11  cnf(c359, axiom,
% 5.92/1.11  	system_file_needs_level(system,secretfile,secret)).
% 5.92/1.11  cnf(a411, assumption,
% 5.92/1.11  	system = system).
% 5.92/1.11  cnf(a412, assumption,
% 5.92/1.11  	X162 = secretfile).
% 5.92/1.11  cnf(a413, assumption,
% 5.92/1.11  	X163 = secret).
% 5.92/1.11  cnf(c360, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a411, a412, a413])], [c358, c359])).
% 5.92/1.11  cnf(c361, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a411, a412, a413])], [c358, c359])).
% 5.92/1.11  
% 5.92/1.11  cnf(c362, axiom,
% 5.92/1.11  	admin_indi_has_need_to_know_for_file(admin,X187,X188) | ~owner_indi_has_need_to_know(X189,X187,X188) | ~state_file_has_owner(X188,X189)).
% 5.92/1.11  cnf(a414, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a415, assumption,
% 5.92/1.11  	X0 = X187).
% 5.92/1.11  cnf(a416, assumption,
% 5.92/1.11  	X1 = X188).
% 5.92/1.11  cnf(c363, plain,
% 5.92/1.11  	~admin_indi_has_citizenship_for_file(admin,X0,X1) | ~state_file_is_not_working_paper(X1),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a414, a415, a416])], [c271, c362])).
% 5.92/1.11  cnf(c364, plain,
% 5.92/1.11  	~owner_indi_has_need_to_know(X189,X187,X188) | ~state_file_has_owner(X188,X189),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a414, a415, a416])], [c271, c362])).
% 5.92/1.11  
% 5.92/1.11  cnf(c365, axiom,
% 5.92/1.11  	owner_indi_has_need_to_know(owner_secretfile,alice,secretfile)).
% 5.92/1.11  cnf(a417, assumption,
% 5.92/1.11  	X189 = owner_secretfile).
% 5.92/1.11  cnf(a418, assumption,
% 5.92/1.11  	X187 = alice).
% 5.92/1.11  cnf(a419, assumption,
% 5.92/1.11  	X188 = secretfile).
% 5.92/1.11  cnf(c366, plain,
% 5.92/1.11  	~state_file_has_owner(X188,X189),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a417, a418, a419])], [c364, c365])).
% 5.92/1.11  cnf(c367, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a417, a418, a419])], [c364, c365])).
% 5.92/1.11  
% 5.92/1.11  cnf(c368, axiom,
% 5.92/1.11  	state_file_has_owner(secretfile,owner_secretfile)).
% 5.92/1.11  cnf(a420, assumption,
% 5.92/1.11  	X188 = secretfile).
% 5.92/1.11  cnf(a421, assumption,
% 5.92/1.11  	X189 = owner_secretfile).
% 5.92/1.11  cnf(c369, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a420, a421])], [c366, c368])).
% 5.92/1.11  cnf(c370, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a420, a421])], [c366, c368])).
% 5.92/1.11  
% 5.92/1.11  cnf(c371, axiom,
% 5.92/1.11  	admin_indi_has_citizenship_for_file(admin,X190,X191) | ~admin_indi_has_citizenship(admin,X190,usa)).
% 5.92/1.11  cnf(a422, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a423, assumption,
% 5.92/1.11  	X0 = X190).
% 5.92/1.11  cnf(a424, assumption,
% 5.92/1.11  	X1 = X191).
% 5.92/1.11  cnf(c372, plain,
% 5.92/1.11  	~state_file_is_not_working_paper(X1),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a422, a423, a424])], [c363, c371])).
% 5.92/1.11  cnf(c373, plain,
% 5.92/1.11  	~admin_indi_has_citizenship(admin,X190,usa),
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a422, a423, a424])], [c363, c371])).
% 5.92/1.11  
% 5.92/1.11  cnf(c374, plain,
% 5.92/1.11  	admin_indi_has_citizenship(admin,X21,usa)).
% 5.92/1.11  cnf(a425, assumption,
% 5.92/1.11  	admin = admin).
% 5.92/1.11  cnf(a426, assumption,
% 5.92/1.11  	X190 = X21).
% 5.92/1.11  cnf(a427, assumption,
% 5.92/1.11  	usa = usa).
% 5.92/1.11  cnf(c375, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(predicate_reduction, [assumptions([a425, a426, a427])], [c373, c374])).
% 5.92/1.11  
% 5.92/1.11  cnf(c376, axiom,
% 5.92/1.11  	state_file_is_not_working_paper(secretfile)).
% 5.92/1.11  cnf(a428, assumption,
% 5.92/1.11  	X1 = secretfile).
% 5.92/1.11  cnf(c377, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a428])], [c372, c376])).
% 5.92/1.11  cnf(c378, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(strict_predicate_extension, [assumptions([a428])], [c372, c376])).
% 5.92/1.11  
% 5.92/1.11  cnf(c379, plain,
% 5.92/1.11  	$false,
% 5.92/1.11  	inference(constraint_solving, [
% 5.92/1.11  		bind(X0, alice),
% 5.92/1.11  		bind(X1, secretfile),
% 5.92/1.11  		bind(X2, alice),
% 5.92/1.11  		bind(X3, secretfile),
% 5.92/1.11  		bind(X4, cons(X6,X7)),
% 5.92/1.11  		bind(X5, alice),
% 5.92/1.11  		bind(X6, compartmentb),
% 5.92/1.11  		bind(X7, cons(X10,X11)),
% 5.92/1.11  		bind(X8, sso_compartmentb),
% 5.92/1.11  		bind(X9, alice),
% 5.92/1.11  		bind(X10, compartmenta),
% 5.92/1.11  		bind(X11, nil),
% 5.92/1.11  		bind(X12, sso_compartmenta),
% 5.92/1.11  		bind(X13, alice),
% 5.92/1.11  		bind(X14, alice),
% 5.92/1.11  		bind(X15, compartmenta),
% 5.92/1.11  		bind(X16, sbu),
% 5.92/1.11  		bind(X17, oca),
% 5.92/1.11  		bind(X18, unclassified),
% 5.92/1.11  		bind(X19, no),
% 5.92/1.11  		bind(X20, no),
% 5.92/1.11  		bind(X21, alice),
% 5.92/1.11  		bind(X22, sbu),
% 5.92/1.11  		bind(X23, topsecret),
% 5.92/1.11  		bind(X24, level_admin),
% 5.92/1.11  		bind(X25, secret),
% 5.92/1.11  		bind(X26, alice),
% 5.92/1.11  		bind(X27, sbu),
% 5.92/1.11  		bind(X28, topsecret),
% 5.92/1.11  		bind(X29, background_admin),
% 5.92/1.11  		bind(X30, admin),
% 5.92/1.11  		bind(X31, sbu),
% 5.92/1.11  		bind(X32, topsecret),
% 5.92/1.11  		bind(X33, secret),
% 5.92/1.11  		bind(X34, admin),
% 5.92/1.11  		bind(X35, sbu),
% 5.92/1.11  		bind(X36, secret),
% 5.92/1.11  		bind(X37, confidential),
% 5.92/1.11  		bind(X38, admin),
% 5.92/1.11  		bind(X39, sbu),
% 5.92/1.11  		bind(X40, confidential),
% 5.92/1.11  		bind(X41, sbu),
% 5.92/1.11  		bind(X42, admin),
% 5.92/1.11  		bind(X43, sbu),
% 5.92/1.11  		bind(X44, admin),
% 5.92/1.11  		bind(X45, admin),
% 5.92/1.11  		bind(X46, admin),
% 5.92/1.11  		bind(X47, alice),
% 5.92/1.11  		bind(X48, credit_admin),
% 5.92/1.11  		bind(X49, alice),
% 5.92/1.11  		bind(X50, hr_admin),
% 5.92/1.11  		bind(X51, alice),
% 5.92/1.11  		bind(X52, polygraph_admin),
% 5.92/1.11  		bind(X53, alice),
% 5.92/1.11  		bind(X54, usa),
% 5.92/1.11  		bind(X55, alice),
% 5.92/1.11  		bind(X56, compartmenta),
% 5.92/1.11  		bind(X57, unclassified),
% 5.92/1.11  		bind(X58, oca),
% 5.92/1.11  		bind(X59, sbu),
% 5.92/1.11  		bind(X60, no),
% 5.92/1.11  		bind(X61, no),
% 5.92/1.11  		bind(X62, alice),
% 5.92/1.11  		bind(X63, compartmenta),
% 5.92/1.11  		bind(X64, sso_compartmenta),
% 5.92/1.11  		bind(X65, alice),
% 5.92/1.11  		bind(X66, compartmenta),
% 5.92/1.11  		bind(X67, oca),
% 5.92/1.11  		bind(X68, sbu),
% 5.92/1.11  		bind(X69, unclassified),
% 5.92/1.11  		bind(X70, no),
% 5.92/1.11  		bind(X71, alice),
% 5.92/1.11  		bind(X72, compartmenta),
% 5.92/1.11  		bind(X73, oca),
% 5.92/1.11  		bind(X74, sbu),
% 5.92/1.11  		bind(X75, unclassified),
% 5.92/1.11  		bind(X76, no),
% 5.92/1.11  		bind(X77, alice),
% 5.92/1.11  		bind(X78, compartmentb),
% 5.92/1.11  		bind(X79, confidential),
% 5.92/1.11  		bind(X80, oca),
% 5.92/1.11  		bind(X81, topsecret),
% 5.92/1.11  		bind(X82, yes),
% 5.92/1.11  		bind(X83, yes),
% 5.92/1.11  		bind(X84, alice),
% 5.92/1.11  		bind(X85, confidential),
% 5.92/1.11  		bind(X86, topsecret),
% 5.92/1.11  		bind(X87, level_admin),
% 5.92/1.11  		bind(X88, secret),
% 5.92/1.11  		bind(X89, alice),
% 5.92/1.11  		bind(X90, confidential),
% 5.92/1.11  		bind(X91, topsecret),
% 5.92/1.11  		bind(X92, background_admin),
% 5.92/1.11  		bind(X93, admin),
% 5.92/1.11  		bind(X94, confidential),
% 5.92/1.11  		bind(X95, topsecret),
% 5.92/1.11  		bind(X96, secret),
% 5.92/1.11  		bind(X97, admin),
% 5.92/1.11  		bind(X98, confidential),
% 5.92/1.11  		bind(X99, secret),
% 5.92/1.11  		bind(X100, confidential),
% 5.92/1.11  		bind(X101, admin),
% 5.92/1.11  		bind(X102, confidential),
% 5.92/1.11  		bind(X103, alice),
% 5.92/1.11  		bind(X104, compartmentb),
% 5.92/1.11  		bind(X105, topsecret),
% 5.92/1.11  		bind(X106, oca),
% 5.92/1.11  		bind(X107, confidential),
% 5.92/1.11  		bind(X108, yes),
% 5.92/1.11  		bind(X109, yes),
% 5.92/1.11  		bind(X110, alice),
% 5.92/1.11  		bind(X111, topsecret),
% 5.92/1.11  		bind(X112, topsecret),
% 5.92/1.11  		bind(X113, background_admin),
% 5.92/1.11  		bind(X114, admin),
% 5.92/1.11  		bind(X115, topsecret),
% 5.92/1.11  		bind(X116, compartmentb),
% 5.92/1.11  		bind(X117, sso_compartmentb),
% 5.92/1.11  		bind(X118, alice),
% 5.92/1.11  		bind(X119, compartmentb),
% 5.92/1.11  		bind(X120, oca),
% 5.92/1.11  		bind(X121, confidential),
% 5.92/1.11  		bind(X122, topsecret),
% 5.92/1.11  		bind(X123, yes),
% 5.92/1.11  		bind(X124, alice),
% 5.92/1.11  		bind(X125, compartmentb),
% 5.92/1.11  		bind(X126, oca),
% 5.92/1.11  		bind(X127, confidential),
% 5.92/1.11  		bind(X128, topsecret),
% 5.92/1.11  		bind(X129, yes),
% 5.92/1.11  		bind(X130, secretfile),
% 5.92/1.11  		bind(X131, cons(X6,X7)),
% 5.92/1.11  		bind(X132, secretfile),
% 5.92/1.11  		bind(X133, cons(X6,X7)),
% 5.92/1.11  		bind(X134, compartmentb),
% 5.92/1.11  		bind(X135, cons(X10,X11)),
% 5.92/1.11  		bind(X136, sso_compartmentb),
% 5.92/1.11  		bind(X137, secretfile),
% 5.92/1.11  		bind(X138, cons(X6,X7)),
% 5.92/1.11  		bind(X139, compartmenta),
% 5.92/1.11  		bind(X140, nil),
% 5.92/1.11  		bind(X141, sso_compartmenta),
% 5.92/1.11  		bind(X142, secretfile),
% 5.92/1.11  		bind(X143, cons(X6,X7)),
% 5.92/1.11  		bind(X144, alice),
% 5.92/1.11  		bind(X145, secretfile),
% 5.92/1.11  		bind(X146, secret),
% 5.92/1.11  		bind(X147, alice),
% 5.92/1.11  		bind(X148, secret),
% 5.92/1.11  		bind(X149, topsecret),
% 5.92/1.11  		bind(X150, level_admin),
% 5.92/1.11  		bind(X151, secret),
% 5.92/1.11  		bind(X152, alice),
% 5.92/1.11  		bind(X153, secret),
% 5.92/1.11  		bind(X154, topsecret),
% 5.92/1.11  		bind(X155, background_admin),
% 5.92/1.11  		bind(X156, admin),
% 5.92/1.11  		bind(X157, secret),
% 5.92/1.11  		bind(X158, topsecret),
% 5.92/1.11  		bind(X159, secret),
% 5.92/1.11  		bind(X160, admin),
% 5.92/1.11  		bind(X161, secret),
% 5.92/1.11  		bind(X162, secretfile),
% 5.92/1.11  		bind(X163, secret),
% 5.92/1.11  		bind(X164, cons(X167,X168)),
% 5.92/1.11  		bind(X165, secretfile),
% 5.92/1.11  		bind(X166, secret),
% 5.92/1.11  		bind(X167, compartmentb),
% 5.92/1.11  		bind(X168, cons(X173,X174)),
% 5.92/1.11  		bind(X169, sso_compartmentb),
% 5.92/1.11  		bind(X170, scg_compartmentb),
% 5.92/1.11  		bind(X171, secretfile),
% 5.92/1.11  		bind(X172, secret),
% 5.92/1.11  		bind(X173, compartmenta),
% 5.92/1.11  		bind(X174, nil),
% 5.92/1.11  		bind(X175, sso_compartmenta),
% 5.92/1.11  		bind(X176, scg_compartmenta),
% 5.92/1.11  		bind(X177, secretfile),
% 5.92/1.11  		bind(X178, secret),
% 5.92/1.11  		bind(X179, compartmenta),
% 5.92/1.11  		bind(X180, scg_compartmenta),
% 5.92/1.11  		bind(X181, sso_compartmenta),
% 5.92/1.11  		bind(X182, oca),
% 5.92/1.11  		bind(X183, compartmentb),
% 5.92/1.11  		bind(X184, scg_compartmentb),
% 5.92/1.11  		bind(X185, sso_compartmentb),
% 5.92/1.11  		bind(X186, oca),
% 5.92/1.11  		bind(X187, alice),
% 5.92/1.11  		bind(X188, secretfile),
% 5.92/1.11  		bind(X189, owner_secretfile),
% 5.92/1.11  		bind(X190, alice),
% 5.92/1.11  		bind(X191, secretfile)
% 5.92/1.11  	],
% 5.92/1.11  	[a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59, a60, a61, a62, a63, a64, a65, a66, a67, a68, a69, a70, a71, a72, a73, a74, a75, a76, a77, a78, a79, a80, a81, a82, a83, a84, a85, a86, a87, a88, a89, a90, a91, a92, a93, a94, a95, a96, a97, a98, a99, a100, a101, a102, a103, a104, a105, a106, a107, a108, a109, a110, a111, a112, a113, a114, a115, a116, a117, a118, a119, a120, a121, a122, a123, a124, a125, a126, a127, a128, a129, a130, a131, a132, a133, a134, a135, a136, a137, a138, a139, a140, a141, a142, a143, a144, a145, a146, a147, a148, a149, a150, a151, a152, a153, a154, a155, a156, a157, a158, a159, a160, a161, a162, a163, a164, a165, a166, a167, a168, a169, a170, a171, a172, a173, a174, a175, a176, a177, a178, a179, a180, a181, a182, a183, a184, a185, a186, a187, a188, a189, a190, a191, a192, a193, a194, a195, a196, a197, a198, a199, a200, a201, a202, a203, a204, a205, a206, a207, a208, a209, a210, a211, a212, a213, a214, a215, a216, a217, a218, a219, a220, a221, a222, a223, a224, a225, a226, a227, a228, a229, a230, a231, a232, a233, a234, a235, a236, a237, a238, a239, a240, a241, a242, a243, a244, a245, a246, a247, a248, a249, a250, a251, a252, a253, a254, a255, a256, a257, a258, a259, a260, a261, a262, a263, a264, a265, a266, a267, a268, a269, a270, a271, a272, a273, a274, a275, a276, a277, a278, a279, a280, a281, a282, a283, a284, a285, a286, a287, a288, a289, a290, a291, a292, a293, a294, a295, a296, a297, a298, a299, a300, a301, a302, a303, a304, a305, a306, a307, a308, a309, a310, a311, a312, a313, a314, a315, a316, a317, a318, a319, a320, a321, a322, a323, a324, a325, a326, a327, a328, a329, a330, a331, a332, a333, a334, a335, a336, a337, a338, a339, a340, a341, a342, a343, a344, a345, a346, a347, a348, a349, a350, a351, a352, a353, a354, a355, a356, a357, a358, a359, a360, a361, a362, a363, a364, a365, a366, a367, a368, a369, a370, a371, a372, a373, a374, a375, a376, a377, a378, a379, a380, a381, a382, a383, a384, a385, a386, a387, a388, a389, a390, a391, a392, a393, a394, a395, a396, a397, a398, a399, a400, a401, a402, a403, a404, a405, a406, a407, a408, a409, a410, a411, a412, a413, a414, a415, a416, a417, a418, a419, a420, a421, a422, a423, a424, a425, a426, a427, a428])).
% 5.92/1.11  
% 5.92/1.11  % SZS output end IncompleteProof
%------------------------------------------------------------------------------