%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWV437+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 08:58:28 EST 2010
% Result : Theorem 1.05s
% Output : Solution 1.05s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP32518/SWV437+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP32518/SWV437+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP32518/SWV437+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 32614
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,system_indi_is_oca(system,oca),file('/tmp/SRASS.s.p', ax41)).
% fof(3, axiom,oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),file('/tmp/SRASS.s.p', ax42)).
% fof(4, axiom,oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),file('/tmp/SRASS.s.p', ax43)).
% fof(5, axiom,system_compartment_has_sso(system,compartmentb,sso_compartmentb),file('/tmp/SRASS.s.p', ax44)).
% fof(6, axiom,oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),file('/tmp/SRASS.s.p', ax45)).
% fof(7, axiom,sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),file('/tmp/SRASS.s.p', ax46)).
% fof(8, axiom,system_compartment_has_sso(system,compartmenta,sso_compartmenta),file('/tmp/SRASS.s.p', ax47)).
% fof(9, axiom,oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),file('/tmp/SRASS.s.p', ax48)).
% fof(10, axiom,sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),file('/tmp/SRASS.s.p', ax49)).
% fof(11, axiom,state_file_is_not_working_paper(secretfile),file('/tmp/SRASS.s.p', ax50)).
% fof(12, axiom,system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),file('/tmp/SRASS.s.p', ax51)).
% fof(13, axiom,sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),file('/tmp/SRASS.s.p', ax52)).
% fof(14, axiom,sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),file('/tmp/SRASS.s.p', ax53)).
% fof(15, axiom,system_file_needs_level(system,secretfile,secret),file('/tmp/SRASS.s.p', ax54)).
% fof(16, axiom,sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),file('/tmp/SRASS.s.p', ax55)).
% fof(17, axiom,sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),file('/tmp/SRASS.s.p', ax56)).
% fof(21, axiom,state_file_has_owner(secretfile,owner_secretfile),file('/tmp/SRASS.s.p', ax60)).
% fof(27, axiom,system_indi_is_polygraph_admin(system,polygraph_admin),file('/tmp/SRASS.s.p', ax66)).
% fof(28, axiom,system_indi_is_credit_admin(system,credit_admin),file('/tmp/SRASS.s.p', ax67)).
% fof(29, axiom,system_indi_is_background_admin(system,background_admin),file('/tmp/SRASS.s.p', ax68)).
% fof(30, axiom,system_indi_is_hr_admin(system,hr_admin),file('/tmp/SRASS.s.p', ax69)).
% fof(31, axiom,system_indi_is_level_admin(system,level_admin),file('/tmp/SRASS.s.p', ax70)).
% fof(32, axiom,system_indi_has_citizenship(system,alice,usa),file('/tmp/SRASS.s.p', ax71)).
% fof(33, axiom,polygraph_admin_indi_has_polygraph(polygraph_admin,alice),file('/tmp/SRASS.s.p', ax72)).
% fof(34, axiom,credit_admin_indi_has_credit(credit_admin,alice),file('/tmp/SRASS.s.p', ax73)).
% fof(35, axiom,background_admin_indi_has_background(background_admin,alice,topsecret),file('/tmp/SRASS.s.p', ax74)).
% fof(36, axiom,hr_admin_indi_has_employment(hr_admin,alice),file('/tmp/SRASS.s.p', ax75)).
% fof(37, axiom,system_indi_needs_level(system,alice,secret),file('/tmp/SRASS.s.p', ax76)).
% fof(38, axiom,level_admin_indi_has_level(level_admin,alice,topsecret),file('/tmp/SRASS.s.p', ax77)).
% fof(39, axiom,system_indi_needs_compartment(system,alice,compartmentb),file('/tmp/SRASS.s.p', ax78)).
% fof(40, axiom,system_indi_needs_compartment(system,alice,compartmenta),file('/tmp/SRASS.s.p', ax79)).
% fof(41, axiom,sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),file('/tmp/SRASS.s.p', ax80)).
% fof(42, axiom,sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),file('/tmp/SRASS.s.p', ax81)).
% fof(43, axiom,owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),file('/tmp/SRASS.s.p', ax82)).
% fof(48, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,X8,no)=>admin_indi_has_polygraph_for_compartment(admin,X1,X4))),file('/tmp/SRASS.s.p', ax31)).
% fof(49, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X9]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,no,X9)=>admin_indi_has_credit_for_compartment(admin,X1,X4))),file('/tmp/SRASS.s.p', ax33)).
% fof(50, axiom,![X1]:![X10]:(system_indi_is_polygraph_admin(system,X10)=>(polygraph_admin_indi_has_polygraph(X10,X1)=>admin_indi_has_polygraph(admin,X1))),file('/tmp/SRASS.s.p', ax17)).
% fof(51, axiom,![X1]:![X11]:(system_indi_is_credit_admin(system,X11)=>(credit_admin_indi_has_credit(X11,X1)=>admin_indi_has_credit(admin,X1))),file('/tmp/SRASS.s.p', ax18)).
% fof(52, axiom,![X1]:![X12]:(system_indi_is_hr_admin(system,X12)=>(hr_admin_indi_has_employment(X12,X1)=>admin_indi_has_employment(admin,X1))),file('/tmp/SRASS.s.p', ax21)).
% fof(53, axiom,![X1]:loca_level_direct_below(X1,secret,topsecret),file('/tmp/SRASS.s.p', ax3)).
% fof(54, axiom,![X1]:![X2]:![X13]:(state_file_has_owner(X2,X13)=>(owner_indi_has_need_to_know(X13,X1,X2)=>admin_indi_has_need_to_know_for_file(admin,X1,X2))),file('/tmp/SRASS.s.p', ax36)).
% fof(56, axiom,![X1]:loca_level_direct_below(X1,sbu,confidential),file('/tmp/SRASS.s.p', ax1)).
% fof(57, axiom,![X1]:loca_level_direct_below(X1,confidential,secret),file('/tmp/SRASS.s.p', ax2)).
% fof(58, axiom,![X4]:![X14]:(system_compartment_has_sso(system,X4,X14)=>admin_compartment_has_sso(admin,X4,X14)),file('/tmp/SRASS.s.p', ax6)).
% fof(59, axiom,![X5]:![X4]:![X14]:![X15]:(system_indi_is_oca(system,X5)=>(oca_compartment_has_scg(X5,X4,X15)=>(admin_compartment_has_sso(admin,X4,X14)=>(sso_compartment_has_scg(X14,X4,X15)=>admin_compartment_has_scg(admin,X4,X15))))),file('/tmp/SRASS.s.p', ax7)).
% fof(60, axiom,![X1]:![X16]:(system_indi_has_citizenship(system,X1,X16)=>admin_indi_has_citizenship(admin,X1,X16)),file('/tmp/SRASS.s.p', ax23)).
% fof(61, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,X8,yes)=>(admin_indi_has_polygraph(admin,X1)=>admin_indi_has_polygraph_for_compartment(admin,X1,X4)))),file('/tmp/SRASS.s.p', ax30)).
% fof(62, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X9]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,yes,X9)=>(admin_indi_has_credit(admin,X1)=>admin_indi_has_credit_for_compartment(admin,X1,X4)))),file('/tmp/SRASS.s.p', ax32)).
% fof(63, axiom,![X1]:![X17]:![X18]:![X6]:(system_indi_is_background_admin(system,X18)=>(background_admin_indi_has_background(X18,X1,X6)=>(loca_level_below(admin,X17,X6)=>admin_indi_has_background(admin,X1,X17)))),file('/tmp/SRASS.s.p', ax20)).
% fof(65, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,X8,X9)=>(admin_indi_has_background(admin,X1,X7)=>admin_indi_has_background_for_compartment(admin,X1,X4)))),file('/tmp/SRASS.s.p', ax28)).
% fof(66, axiom,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:(system_indi_is_oca(system,X5)=>(oca_compartment_is_compartment(X5,X4,X6,X7,X8,X9)=>(admin_indi_has_level(admin,X1,X6)=>admin_indi_has_level_for_compartment(admin,X1,X4)))),file('/tmp/SRASS.s.p', ax29)).
% fof(67, axiom,![X1]:admin_indi_has_background(admin,X1,unclassified),file('/tmp/SRASS.s.p', ax19)).
% fof(69, axiom,![X2]:![X19]:admin_file_has_compartments_h(admin,X2,X19,nil),file('/tmp/SRASS.s.p', ax9)).
% fof(70, axiom,![X2]:![X19]:![X20]:![X21]:![X14]:(admin_compartment_has_sso(admin,X20,X14)=>(sso_file_has_compartments(X14,X2,X19)=>(admin_file_has_compartments_h(admin,X2,X19,X21)=>admin_file_has_compartments_h(admin,X2,X19,cons(X20,X21))))),file('/tmp/SRASS.s.p', ax10)).
% fof(71, axiom,![X2]:![X17]:admin_file_has_level_h(admin,X2,X17,nil),file('/tmp/SRASS.s.p', ax12)).
% fof(73, axiom,![X1]:admin_indi_has_compartments(admin,X1,nil),file('/tmp/SRASS.s.p', ax26)).
% fof(74, axiom,![X1]:![X17]:loca_level_below(X1,X17,X17),file('/tmp/SRASS.s.p', ax4)).
% fof(75, axiom,![X2]:![X19]:(system_file_needs_compartments(system,X2,X19)=>(admin_file_has_compartments_h(admin,X2,X19,X19)=>admin_file_has_compartments(admin,X2,X19))),file('/tmp/SRASS.s.p', ax8)).
% fof(76, axiom,![X1]:![X2]:(state_file_is_not_working_paper(X2)=>(admin_indi_has_citizenship_for_file(admin,X1,X2)=>(admin_indi_has_need_to_know_for_file(admin,X1,X2)=>(admin_indi_has_level_for_file(admin,X1,X2)=>(admin_indi_has_compartments_for_file(admin,X1,X2)=>admin_indi_may_file(admin,X1,X2,read)))))),file('/tmp/SRASS.s.p', ax39)).
% fof(77, axiom,![X2]:![X17]:![X4]:![X19]:![X14]:![X15]:(admin_compartment_has_sso(admin,X4,X14)=>(admin_compartment_has_scg(admin,X4,X15)=>(sso_file_has_level(X14,X2,X17,X15)=>(admin_file_has_level_h(admin,X2,X17,X19)=>admin_file_has_level_h(admin,X2,X17,cons(X4,X19)))))),file('/tmp/SRASS.s.p', ax13)).
% fof(79, axiom,![X1]:![X17]:![X6]:![X22]:![X23]:(system_indi_needs_level(system,X1,X6)=>(admin_indi_has_citizenship(admin,X1,usa)=>(admin_indi_has_polygraph(admin,X1)=>(admin_indi_has_employment(admin,X1)=>(admin_indi_has_credit(admin,X1)=>(loca_level_below(admin,X17,X6)=>(system_indi_is_level_admin(system,X22)=>(level_admin_indi_has_level(X22,X1,X23)=>(loca_level_below(admin,X17,X23)=>(admin_indi_has_background(admin,X1,X17)=>admin_indi_has_level(admin,X1,X17))))))))))),file('/tmp/SRASS.s.p', ax25)).
% fof(80, axiom,![X1]:![X4]:![X19]:![X14]:(system_indi_needs_compartment(system,X1,X4)=>(admin_indi_has_employment(admin,X1)=>(admin_indi_has_citizenship(admin,X1,usa)=>(admin_indi_has_polygraph_for_compartment(admin,X1,X4)=>(admin_indi_has_credit_for_compartment(admin,X1,X4)=>(admin_compartment_has_sso(admin,X4,X14)=>(sso_indi_has_compartment(X14,X1,X4)=>(admin_indi_has_background_for_compartment(admin,X1,X4)=>(admin_indi_has_level_for_compartment(admin,X1,X4)=>(admin_indi_has_compartments(admin,X1,X19)=>admin_indi_has_compartments(admin,X1,cons(X4,X19)))))))))))),file('/tmp/SRASS.s.p', ax27)).
% fof(81, axiom,![X1]:![X2]:(admin_indi_has_citizenship(admin,X1,usa)=>admin_indi_has_citizenship_for_file(admin,X1,X2)),file('/tmp/SRASS.s.p', ax38)).
% fof(82, axiom,![X2]:![X17]:![X19]:(system_file_needs_level(system,X2,X17)=>(admin_file_has_compartments(admin,X2,X19)=>(admin_file_has_level_h(admin,X2,X17,X19)=>admin_file_has_level(admin,X2,X17)))),file('/tmp/SRASS.s.p', ax11)).
% fof(85, axiom,![X1]:![X17]:![X6]:![X23]:(loca_level_direct_below(X1,X6,X23)=>(loca_level_below(X1,X17,X6)=>loca_level_below(X1,X17,X23))),file('/tmp/SRASS.s.p', ax5)).
% fof(86, axiom,![X1]:![X2]:![X19]:(admin_file_has_compartments(admin,X2,X19)=>(admin_indi_has_compartments(admin,X1,X19)=>admin_indi_has_compartments_for_file(admin,X1,X2))),file('/tmp/SRASS.s.p', ax34)).
% fof(87, axiom,![X1]:![X2]:![X17]:(admin_file_has_level(admin,X2,X17)=>(admin_indi_has_level(admin,X1,X17)=>admin_indi_has_level_for_file(admin,X1,X2))),file('/tmp/SRASS.s.p', ax35)).
% fof(88, conjecture,admin_indi_may_file(admin,alice,secretfile,read),file('/tmp/SRASS.s.p', alicereadsecret)).
% fof(89, negated_conjecture,~(admin_indi_may_file(admin,alice,secretfile,read)),inference(assume_negation,[status(cth)],[88])).
% fof(90, negated_conjecture,~(admin_indi_may_file(admin,alice,secretfile,read)),inference(fof_simplification,[status(thm)],[89,theory(equality)])).
% cnf(94,plain,(system_indi_is_oca(system,oca)),inference(split_conjunct,[status(thm)],[2])).
% cnf(95,plain,(oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)),inference(split_conjunct,[status(thm)],[3])).
% cnf(96,plain,(oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)),inference(split_conjunct,[status(thm)],[4])).
% cnf(97,plain,(system_compartment_has_sso(system,compartmentb,sso_compartmentb)),inference(split_conjunct,[status(thm)],[5])).
% cnf(98,plain,(oca_compartment_has_scg(oca,compartmentb,scg_compartmentb)),inference(split_conjunct,[status(thm)],[6])).
% cnf(99,plain,(sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb)),inference(split_conjunct,[status(thm)],[7])).
% cnf(100,plain,(system_compartment_has_sso(system,compartmenta,sso_compartmenta)),inference(split_conjunct,[status(thm)],[8])).
% cnf(101,plain,(oca_compartment_has_scg(oca,compartmenta,scg_compartmenta)),inference(split_conjunct,[status(thm)],[9])).
% cnf(102,plain,(sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta)),inference(split_conjunct,[status(thm)],[10])).
% cnf(103,plain,(state_file_is_not_working_paper(secretfile)),inference(split_conjunct,[status(thm)],[11])).
% cnf(104,plain,(system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))),inference(split_conjunct,[status(thm)],[12])).
% cnf(105,plain,(sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))),inference(split_conjunct,[status(thm)],[13])).
% cnf(106,plain,(sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))),inference(split_conjunct,[status(thm)],[14])).
% cnf(107,plain,(system_file_needs_level(system,secretfile,secret)),inference(split_conjunct,[status(thm)],[15])).
% cnf(108,plain,(sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb)),inference(split_conjunct,[status(thm)],[16])).
% cnf(109,plain,(sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta)),inference(split_conjunct,[status(thm)],[17])).
% cnf(113,plain,(state_file_has_owner(secretfile,owner_secretfile)),inference(split_conjunct,[status(thm)],[21])).
% cnf(119,plain,(system_indi_is_polygraph_admin(system,polygraph_admin)),inference(split_conjunct,[status(thm)],[27])).
% cnf(120,plain,(system_indi_is_credit_admin(system,credit_admin)),inference(split_conjunct,[status(thm)],[28])).
% cnf(121,plain,(system_indi_is_background_admin(system,background_admin)),inference(split_conjunct,[status(thm)],[29])).
% cnf(122,plain,(system_indi_is_hr_admin(system,hr_admin)),inference(split_conjunct,[status(thm)],[30])).
% cnf(123,plain,(system_indi_is_level_admin(system,level_admin)),inference(split_conjunct,[status(thm)],[31])).
% cnf(124,plain,(system_indi_has_citizenship(system,alice,usa)),inference(split_conjunct,[status(thm)],[32])).
% cnf(125,plain,(polygraph_admin_indi_has_polygraph(polygraph_admin,alice)),inference(split_conjunct,[status(thm)],[33])).
% cnf(126,plain,(credit_admin_indi_has_credit(credit_admin,alice)),inference(split_conjunct,[status(thm)],[34])).
% cnf(127,plain,(background_admin_indi_has_background(background_admin,alice,topsecret)),inference(split_conjunct,[status(thm)],[35])).
% cnf(128,plain,(hr_admin_indi_has_employment(hr_admin,alice)),inference(split_conjunct,[status(thm)],[36])).
% cnf(129,plain,(system_indi_needs_level(system,alice,secret)),inference(split_conjunct,[status(thm)],[37])).
% cnf(130,plain,(level_admin_indi_has_level(level_admin,alice,topsecret)),inference(split_conjunct,[status(thm)],[38])).
% cnf(131,plain,(system_indi_needs_compartment(system,alice,compartmentb)),inference(split_conjunct,[status(thm)],[39])).
% cnf(132,plain,(system_indi_needs_compartment(system,alice,compartmenta)),inference(split_conjunct,[status(thm)],[40])).
% cnf(133,plain,(sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)),inference(split_conjunct,[status(thm)],[41])).
% cnf(134,plain,(sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)),inference(split_conjunct,[status(thm)],[42])).
% cnf(135,plain,(owner_indi_has_need_to_know(owner_secretfile,alice,secretfile)),inference(split_conjunct,[status(thm)],[43])).
% fof(140, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,X8,no))|admin_indi_has_polygraph_for_compartment(admin,X1,X4))),inference(fof_nnf,[status(thm)],[48])).
% fof(141, plain,![X9]:![X10]:![X11]:![X12]:![X13]:![X14]:(~(system_indi_is_oca(system,X11))|(~(oca_compartment_is_compartment(X11,X10,X12,X13,X14,no))|admin_indi_has_polygraph_for_compartment(admin,X9,X10))),inference(variable_rename,[status(thm)],[140])).
% cnf(142,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,X2)|~oca_compartment_is_compartment(X3,X2,X4,X5,X6,no)|~system_indi_is_oca(system,X3)),inference(split_conjunct,[status(thm)],[141])).
% fof(143, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X9]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,no,X9))|admin_indi_has_credit_for_compartment(admin,X1,X4))),inference(fof_nnf,[status(thm)],[49])).
% fof(144, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:(~(system_indi_is_oca(system,X12))|(~(oca_compartment_is_compartment(X12,X11,X13,X14,no,X15))|admin_indi_has_credit_for_compartment(admin,X10,X11))),inference(variable_rename,[status(thm)],[143])).
% cnf(145,plain,(admin_indi_has_credit_for_compartment(admin,X1,X2)|~oca_compartment_is_compartment(X3,X2,X4,X5,no,X6)|~system_indi_is_oca(system,X3)),inference(split_conjunct,[status(thm)],[144])).
% fof(146, plain,![X1]:![X10]:(~(system_indi_is_polygraph_admin(system,X10))|(~(polygraph_admin_indi_has_polygraph(X10,X1))|admin_indi_has_polygraph(admin,X1))),inference(fof_nnf,[status(thm)],[50])).
% fof(147, plain,![X11]:![X12]:(~(system_indi_is_polygraph_admin(system,X12))|(~(polygraph_admin_indi_has_polygraph(X12,X11))|admin_indi_has_polygraph(admin,X11))),inference(variable_rename,[status(thm)],[146])).
% cnf(148,plain,(admin_indi_has_polygraph(admin,X1)|~polygraph_admin_indi_has_polygraph(X2,X1)|~system_indi_is_polygraph_admin(system,X2)),inference(split_conjunct,[status(thm)],[147])).
% fof(149, plain,![X1]:![X11]:(~(system_indi_is_credit_admin(system,X11))|(~(credit_admin_indi_has_credit(X11,X1))|admin_indi_has_credit(admin,X1))),inference(fof_nnf,[status(thm)],[51])).
% fof(150, plain,![X12]:![X13]:(~(system_indi_is_credit_admin(system,X13))|(~(credit_admin_indi_has_credit(X13,X12))|admin_indi_has_credit(admin,X12))),inference(variable_rename,[status(thm)],[149])).
% cnf(151,plain,(admin_indi_has_credit(admin,X1)|~credit_admin_indi_has_credit(X2,X1)|~system_indi_is_credit_admin(system,X2)),inference(split_conjunct,[status(thm)],[150])).
% fof(152, plain,![X1]:![X12]:(~(system_indi_is_hr_admin(system,X12))|(~(hr_admin_indi_has_employment(X12,X1))|admin_indi_has_employment(admin,X1))),inference(fof_nnf,[status(thm)],[52])).
% fof(153, plain,![X13]:![X14]:(~(system_indi_is_hr_admin(system,X14))|(~(hr_admin_indi_has_employment(X14,X13))|admin_indi_has_employment(admin,X13))),inference(variable_rename,[status(thm)],[152])).
% cnf(154,plain,(admin_indi_has_employment(admin,X1)|~hr_admin_indi_has_employment(X2,X1)|~system_indi_is_hr_admin(system,X2)),inference(split_conjunct,[status(thm)],[153])).
% fof(155, plain,![X2]:loca_level_direct_below(X2,secret,topsecret),inference(variable_rename,[status(thm)],[53])).
% cnf(156,plain,(loca_level_direct_below(X1,secret,topsecret)),inference(split_conjunct,[status(thm)],[155])).
% fof(157, plain,![X1]:![X2]:![X13]:(~(state_file_has_owner(X2,X13))|(~(owner_indi_has_need_to_know(X13,X1,X2))|admin_indi_has_need_to_know_for_file(admin,X1,X2))),inference(fof_nnf,[status(thm)],[54])).
% fof(158, plain,![X14]:![X15]:![X16]:(~(state_file_has_owner(X15,X16))|(~(owner_indi_has_need_to_know(X16,X14,X15))|admin_indi_has_need_to_know_for_file(admin,X14,X15))),inference(variable_rename,[status(thm)],[157])).
% cnf(159,plain,(admin_indi_has_need_to_know_for_file(admin,X1,X2)|~owner_indi_has_need_to_know(X3,X1,X2)|~state_file_has_owner(X2,X3)),inference(split_conjunct,[status(thm)],[158])).
% fof(162, plain,![X2]:loca_level_direct_below(X2,sbu,confidential),inference(variable_rename,[status(thm)],[56])).
% cnf(163,plain,(loca_level_direct_below(X1,sbu,confidential)),inference(split_conjunct,[status(thm)],[162])).
% fof(164, plain,![X2]:loca_level_direct_below(X2,confidential,secret),inference(variable_rename,[status(thm)],[57])).
% cnf(165,plain,(loca_level_direct_below(X1,confidential,secret)),inference(split_conjunct,[status(thm)],[164])).
% fof(166, plain,![X4]:![X14]:(~(system_compartment_has_sso(system,X4,X14))|admin_compartment_has_sso(admin,X4,X14)),inference(fof_nnf,[status(thm)],[58])).
% fof(167, plain,![X15]:![X16]:(~(system_compartment_has_sso(system,X15,X16))|admin_compartment_has_sso(admin,X15,X16)),inference(variable_rename,[status(thm)],[166])).
% cnf(168,plain,(admin_compartment_has_sso(admin,X1,X2)|~system_compartment_has_sso(system,X1,X2)),inference(split_conjunct,[status(thm)],[167])).
% fof(169, plain,![X5]:![X4]:![X14]:![X15]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_has_scg(X5,X4,X15))|(~(admin_compartment_has_sso(admin,X4,X14))|(~(sso_compartment_has_scg(X14,X4,X15))|admin_compartment_has_scg(admin,X4,X15))))),inference(fof_nnf,[status(thm)],[59])).
% fof(170, plain,![X16]:![X17]:![X18]:![X19]:(~(system_indi_is_oca(system,X16))|(~(oca_compartment_has_scg(X16,X17,X19))|(~(admin_compartment_has_sso(admin,X17,X18))|(~(sso_compartment_has_scg(X18,X17,X19))|admin_compartment_has_scg(admin,X17,X19))))),inference(variable_rename,[status(thm)],[169])).
% cnf(171,plain,(admin_compartment_has_scg(admin,X1,X2)|~sso_compartment_has_scg(X3,X1,X2)|~admin_compartment_has_sso(admin,X1,X3)|~oca_compartment_has_scg(X4,X1,X2)|~system_indi_is_oca(system,X4)),inference(split_conjunct,[status(thm)],[170])).
% fof(172, plain,![X1]:![X16]:(~(system_indi_has_citizenship(system,X1,X16))|admin_indi_has_citizenship(admin,X1,X16)),inference(fof_nnf,[status(thm)],[60])).
% fof(173, plain,![X17]:![X18]:(~(system_indi_has_citizenship(system,X17,X18))|admin_indi_has_citizenship(admin,X17,X18)),inference(variable_rename,[status(thm)],[172])).
% cnf(174,plain,(admin_indi_has_citizenship(admin,X1,X2)|~system_indi_has_citizenship(system,X1,X2)),inference(split_conjunct,[status(thm)],[173])).
% fof(175, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,X8,yes))|(~(admin_indi_has_polygraph(admin,X1))|admin_indi_has_polygraph_for_compartment(admin,X1,X4)))),inference(fof_nnf,[status(thm)],[61])).
% fof(176, plain,![X9]:![X10]:![X11]:![X12]:![X13]:![X14]:(~(system_indi_is_oca(system,X11))|(~(oca_compartment_is_compartment(X11,X10,X12,X13,X14,yes))|(~(admin_indi_has_polygraph(admin,X9))|admin_indi_has_polygraph_for_compartment(admin,X9,X10)))),inference(variable_rename,[status(thm)],[175])).
% cnf(177,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,X2)|~admin_indi_has_polygraph(admin,X1)|~oca_compartment_is_compartment(X3,X2,X4,X5,X6,yes)|~system_indi_is_oca(system,X3)),inference(split_conjunct,[status(thm)],[176])).
% fof(178, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X9]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,yes,X9))|(~(admin_indi_has_credit(admin,X1))|admin_indi_has_credit_for_compartment(admin,X1,X4)))),inference(fof_nnf,[status(thm)],[62])).
% fof(179, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:(~(system_indi_is_oca(system,X12))|(~(oca_compartment_is_compartment(X12,X11,X13,X14,yes,X15))|(~(admin_indi_has_credit(admin,X10))|admin_indi_has_credit_for_compartment(admin,X10,X11)))),inference(variable_rename,[status(thm)],[178])).
% cnf(180,plain,(admin_indi_has_credit_for_compartment(admin,X1,X2)|~admin_indi_has_credit(admin,X1)|~oca_compartment_is_compartment(X3,X2,X4,X5,yes,X6)|~system_indi_is_oca(system,X3)),inference(split_conjunct,[status(thm)],[179])).
% fof(181, plain,![X1]:![X17]:![X18]:![X6]:(~(system_indi_is_background_admin(system,X18))|(~(background_admin_indi_has_background(X18,X1,X6))|(~(loca_level_below(admin,X17,X6))|admin_indi_has_background(admin,X1,X17)))),inference(fof_nnf,[status(thm)],[63])).
% fof(182, plain,![X19]:![X20]:![X21]:![X22]:(~(system_indi_is_background_admin(system,X21))|(~(background_admin_indi_has_background(X21,X19,X22))|(~(loca_level_below(admin,X20,X22))|admin_indi_has_background(admin,X19,X20)))),inference(variable_rename,[status(thm)],[181])).
% cnf(183,plain,(admin_indi_has_background(admin,X1,X2)|~loca_level_below(admin,X2,X3)|~background_admin_indi_has_background(X4,X1,X3)|~system_indi_is_background_admin(system,X4)),inference(split_conjunct,[status(thm)],[182])).
% fof(186, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,X8,X9))|(~(admin_indi_has_background(admin,X1,X7))|admin_indi_has_background_for_compartment(admin,X1,X4)))),inference(fof_nnf,[status(thm)],[65])).
% fof(187, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:(~(system_indi_is_oca(system,X12))|(~(oca_compartment_is_compartment(X12,X11,X13,X14,X15,X16))|(~(admin_indi_has_background(admin,X10,X14))|admin_indi_has_background_for_compartment(admin,X10,X11)))),inference(variable_rename,[status(thm)],[186])).
% cnf(188,plain,(admin_indi_has_background_for_compartment(admin,X1,X2)|~admin_indi_has_background(admin,X1,X3)|~oca_compartment_is_compartment(X4,X2,X5,X3,X6,X7)|~system_indi_is_oca(system,X4)),inference(split_conjunct,[status(thm)],[187])).
% fof(189, plain,![X1]:![X4]:![X5]:![X6]:![X7]:![X8]:![X9]:(~(system_indi_is_oca(system,X5))|(~(oca_compartment_is_compartment(X5,X4,X6,X7,X8,X9))|(~(admin_indi_has_level(admin,X1,X6))|admin_indi_has_level_for_compartment(admin,X1,X4)))),inference(fof_nnf,[status(thm)],[66])).
% fof(190, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:(~(system_indi_is_oca(system,X12))|(~(oca_compartment_is_compartment(X12,X11,X13,X14,X15,X16))|(~(admin_indi_has_level(admin,X10,X13))|admin_indi_has_level_for_compartment(admin,X10,X11)))),inference(variable_rename,[status(thm)],[189])).
% cnf(191,plain,(admin_indi_has_level_for_compartment(admin,X1,X2)|~admin_indi_has_level(admin,X1,X3)|~oca_compartment_is_compartment(X4,X2,X3,X5,X6,X7)|~system_indi_is_oca(system,X4)),inference(split_conjunct,[status(thm)],[190])).
% fof(192, plain,![X2]:admin_indi_has_background(admin,X2,unclassified),inference(variable_rename,[status(thm)],[67])).
% cnf(193,plain,(admin_indi_has_background(admin,X1,unclassified)),inference(split_conjunct,[status(thm)],[192])).
% fof(196, plain,![X20]:![X21]:admin_file_has_compartments_h(admin,X20,X21,nil),inference(variable_rename,[status(thm)],[69])).
% cnf(197,plain,(admin_file_has_compartments_h(admin,X1,X2,nil)),inference(split_conjunct,[status(thm)],[196])).
% fof(198, plain,![X2]:![X19]:![X20]:![X21]:![X14]:(~(admin_compartment_has_sso(admin,X20,X14))|(~(sso_file_has_compartments(X14,X2,X19))|(~(admin_file_has_compartments_h(admin,X2,X19,X21))|admin_file_has_compartments_h(admin,X2,X19,cons(X20,X21))))),inference(fof_nnf,[status(thm)],[70])).
% fof(199, plain,![X22]:![X23]:![X24]:![X25]:![X26]:(~(admin_compartment_has_sso(admin,X24,X26))|(~(sso_file_has_compartments(X26,X22,X23))|(~(admin_file_has_compartments_h(admin,X22,X23,X25))|admin_file_has_compartments_h(admin,X22,X23,cons(X24,X25))))),inference(variable_rename,[status(thm)],[198])).
% cnf(200,plain,(admin_file_has_compartments_h(admin,X1,X2,cons(X3,X4))|~admin_file_has_compartments_h(admin,X1,X2,X4)|~sso_file_has_compartments(X5,X1,X2)|~admin_compartment_has_sso(admin,X3,X5)),inference(split_conjunct,[status(thm)],[199])).
% fof(201, plain,![X18]:![X19]:admin_file_has_level_h(admin,X18,X19,nil),inference(variable_rename,[status(thm)],[71])).
% cnf(202,plain,(admin_file_has_level_h(admin,X1,X2,nil)),inference(split_conjunct,[status(thm)],[201])).
% fof(205, plain,![X2]:admin_indi_has_compartments(admin,X2,nil),inference(variable_rename,[status(thm)],[73])).
% cnf(206,plain,(admin_indi_has_compartments(admin,X1,nil)),inference(split_conjunct,[status(thm)],[205])).
% fof(207, plain,![X18]:![X19]:loca_level_below(X18,X19,X19),inference(variable_rename,[status(thm)],[74])).
% cnf(208,plain,(loca_level_below(X1,X2,X2)),inference(split_conjunct,[status(thm)],[207])).
% fof(209, plain,![X2]:![X19]:(~(system_file_needs_compartments(system,X2,X19))|(~(admin_file_has_compartments_h(admin,X2,X19,X19))|admin_file_has_compartments(admin,X2,X19))),inference(fof_nnf,[status(thm)],[75])).
% fof(210, plain,![X20]:![X21]:(~(system_file_needs_compartments(system,X20,X21))|(~(admin_file_has_compartments_h(admin,X20,X21,X21))|admin_file_has_compartments(admin,X20,X21))),inference(variable_rename,[status(thm)],[209])).
% cnf(211,plain,(admin_file_has_compartments(admin,X1,X2)|~admin_file_has_compartments_h(admin,X1,X2,X2)|~system_file_needs_compartments(system,X1,X2)),inference(split_conjunct,[status(thm)],[210])).
% fof(212, plain,![X1]:![X2]:(~(state_file_is_not_working_paper(X2))|(~(admin_indi_has_citizenship_for_file(admin,X1,X2))|(~(admin_indi_has_need_to_know_for_file(admin,X1,X2))|(~(admin_indi_has_level_for_file(admin,X1,X2))|(~(admin_indi_has_compartments_for_file(admin,X1,X2))|admin_indi_may_file(admin,X1,X2,read)))))),inference(fof_nnf,[status(thm)],[76])).
% fof(213, plain,![X3]:![X4]:(~(state_file_is_not_working_paper(X4))|(~(admin_indi_has_citizenship_for_file(admin,X3,X4))|(~(admin_indi_has_need_to_know_for_file(admin,X3,X4))|(~(admin_indi_has_level_for_file(admin,X3,X4))|(~(admin_indi_has_compartments_for_file(admin,X3,X4))|admin_indi_may_file(admin,X3,X4,read)))))),inference(variable_rename,[status(thm)],[212])).
% cnf(214,plain,(admin_indi_may_file(admin,X1,X2,read)|~admin_indi_has_compartments_for_file(admin,X1,X2)|~admin_indi_has_level_for_file(admin,X1,X2)|~admin_indi_has_need_to_know_for_file(admin,X1,X2)|~admin_indi_has_citizenship_for_file(admin,X1,X2)|~state_file_is_not_working_paper(X2)),inference(split_conjunct,[status(thm)],[213])).
% fof(215, plain,![X2]:![X17]:![X4]:![X19]:![X14]:![X15]:(~(admin_compartment_has_sso(admin,X4,X14))|(~(admin_compartment_has_scg(admin,X4,X15))|(~(sso_file_has_level(X14,X2,X17,X15))|(~(admin_file_has_level_h(admin,X2,X17,X19))|admin_file_has_level_h(admin,X2,X17,cons(X4,X19)))))),inference(fof_nnf,[status(thm)],[77])).
% fof(216, plain,![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:(~(admin_compartment_has_sso(admin,X22,X24))|(~(admin_compartment_has_scg(admin,X22,X25))|(~(sso_file_has_level(X24,X20,X21,X25))|(~(admin_file_has_level_h(admin,X20,X21,X23))|admin_file_has_level_h(admin,X20,X21,cons(X22,X23)))))),inference(variable_rename,[status(thm)],[215])).
% cnf(217,plain,(admin_file_has_level_h(admin,X1,X2,cons(X3,X4))|~admin_file_has_level_h(admin,X1,X2,X4)|~sso_file_has_level(X5,X1,X2,X6)|~admin_compartment_has_scg(admin,X3,X6)|~admin_compartment_has_sso(admin,X3,X5)),inference(split_conjunct,[status(thm)],[216])).
% fof(221, plain,![X1]:![X17]:![X6]:![X22]:![X23]:(~(system_indi_needs_level(system,X1,X6))|(~(admin_indi_has_citizenship(admin,X1,usa))|(~(admin_indi_has_polygraph(admin,X1))|(~(admin_indi_has_employment(admin,X1))|(~(admin_indi_has_credit(admin,X1))|(~(loca_level_below(admin,X17,X6))|(~(system_indi_is_level_admin(system,X22))|(~(level_admin_indi_has_level(X22,X1,X23))|(~(loca_level_below(admin,X17,X23))|(~(admin_indi_has_background(admin,X1,X17))|admin_indi_has_level(admin,X1,X17))))))))))),inference(fof_nnf,[status(thm)],[79])).
% fof(222, plain,![X24]:![X25]:![X26]:![X27]:![X28]:(~(system_indi_needs_level(system,X24,X26))|(~(admin_indi_has_citizenship(admin,X24,usa))|(~(admin_indi_has_polygraph(admin,X24))|(~(admin_indi_has_employment(admin,X24))|(~(admin_indi_has_credit(admin,X24))|(~(loca_level_below(admin,X25,X26))|(~(system_indi_is_level_admin(system,X27))|(~(level_admin_indi_has_level(X27,X24,X28))|(~(loca_level_below(admin,X25,X28))|(~(admin_indi_has_background(admin,X24,X25))|admin_indi_has_level(admin,X24,X25))))))))))),inference(variable_rename,[status(thm)],[221])).
% cnf(223,plain,(admin_indi_has_level(admin,X1,X2)|~admin_indi_has_background(admin,X1,X2)|~loca_level_below(admin,X2,X3)|~level_admin_indi_has_level(X4,X1,X3)|~system_indi_is_level_admin(system,X4)|~loca_level_below(admin,X2,X5)|~admin_indi_has_credit(admin,X1)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_polygraph(admin,X1)|~admin_indi_has_citizenship(admin,X1,usa)|~system_indi_needs_level(system,X1,X5)),inference(split_conjunct,[status(thm)],[222])).
% fof(224, plain,![X1]:![X4]:![X19]:![X14]:(~(system_indi_needs_compartment(system,X1,X4))|(~(admin_indi_has_employment(admin,X1))|(~(admin_indi_has_citizenship(admin,X1,usa))|(~(admin_indi_has_polygraph_for_compartment(admin,X1,X4))|(~(admin_indi_has_credit_for_compartment(admin,X1,X4))|(~(admin_compartment_has_sso(admin,X4,X14))|(~(sso_indi_has_compartment(X14,X1,X4))|(~(admin_indi_has_background_for_compartment(admin,X1,X4))|(~(admin_indi_has_level_for_compartment(admin,X1,X4))|(~(admin_indi_has_compartments(admin,X1,X19))|admin_indi_has_compartments(admin,X1,cons(X4,X19)))))))))))),inference(fof_nnf,[status(thm)],[80])).
% fof(225, plain,![X20]:![X21]:![X22]:![X23]:(~(system_indi_needs_compartment(system,X20,X21))|(~(admin_indi_has_employment(admin,X20))|(~(admin_indi_has_citizenship(admin,X20,usa))|(~(admin_indi_has_polygraph_for_compartment(admin,X20,X21))|(~(admin_indi_has_credit_for_compartment(admin,X20,X21))|(~(admin_compartment_has_sso(admin,X21,X23))|(~(sso_indi_has_compartment(X23,X20,X21))|(~(admin_indi_has_background_for_compartment(admin,X20,X21))|(~(admin_indi_has_level_for_compartment(admin,X20,X21))|(~(admin_indi_has_compartments(admin,X20,X22))|admin_indi_has_compartments(admin,X20,cons(X21,X22)))))))))))),inference(variable_rename,[status(thm)],[224])).
% cnf(226,plain,(admin_indi_has_compartments(admin,X1,cons(X2,X3))|~admin_indi_has_compartments(admin,X1,X3)|~admin_indi_has_level_for_compartment(admin,X1,X2)|~admin_indi_has_background_for_compartment(admin,X1,X2)|~sso_indi_has_compartment(X4,X1,X2)|~admin_compartment_has_sso(admin,X2,X4)|~admin_indi_has_credit_for_compartment(admin,X1,X2)|~admin_indi_has_polygraph_for_compartment(admin,X1,X2)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_indi_has_employment(admin,X1)|~system_indi_needs_compartment(system,X1,X2)),inference(split_conjunct,[status(thm)],[225])).
% fof(227, plain,![X1]:![X2]:(~(admin_indi_has_citizenship(admin,X1,usa))|admin_indi_has_citizenship_for_file(admin,X1,X2)),inference(fof_nnf,[status(thm)],[81])).
% fof(228, plain,![X3]:![X4]:(~(admin_indi_has_citizenship(admin,X3,usa))|admin_indi_has_citizenship_for_file(admin,X3,X4)),inference(variable_rename,[status(thm)],[227])).
% cnf(229,plain,(admin_indi_has_citizenship_for_file(admin,X1,X2)|~admin_indi_has_citizenship(admin,X1,usa)),inference(split_conjunct,[status(thm)],[228])).
% fof(230, plain,![X2]:![X17]:![X19]:(~(system_file_needs_level(system,X2,X17))|(~(admin_file_has_compartments(admin,X2,X19))|(~(admin_file_has_level_h(admin,X2,X17,X19))|admin_file_has_level(admin,X2,X17)))),inference(fof_nnf,[status(thm)],[82])).
% fof(231, plain,![X20]:![X21]:![X22]:(~(system_file_needs_level(system,X20,X21))|(~(admin_file_has_compartments(admin,X20,X22))|(~(admin_file_has_level_h(admin,X20,X21,X22))|admin_file_has_level(admin,X20,X21)))),inference(variable_rename,[status(thm)],[230])).
% cnf(232,plain,(admin_file_has_level(admin,X1,X2)|~admin_file_has_level_h(admin,X1,X2,X3)|~admin_file_has_compartments(admin,X1,X3)|~system_file_needs_level(system,X1,X2)),inference(split_conjunct,[status(thm)],[231])).
% fof(239, plain,![X1]:![X17]:![X6]:![X23]:(~(loca_level_direct_below(X1,X6,X23))|(~(loca_level_below(X1,X17,X6))|loca_level_below(X1,X17,X23))),inference(fof_nnf,[status(thm)],[85])).
% fof(240, plain,![X24]:![X25]:![X26]:![X27]:(~(loca_level_direct_below(X24,X26,X27))|(~(loca_level_below(X24,X25,X26))|loca_level_below(X24,X25,X27))),inference(variable_rename,[status(thm)],[239])).
% cnf(241,plain,(loca_level_below(X1,X2,X3)|~loca_level_below(X1,X2,X4)|~loca_level_direct_below(X1,X4,X3)),inference(split_conjunct,[status(thm)],[240])).
% fof(242, plain,![X1]:![X2]:![X19]:(~(admin_file_has_compartments(admin,X2,X19))|(~(admin_indi_has_compartments(admin,X1,X19))|admin_indi_has_compartments_for_file(admin,X1,X2))),inference(fof_nnf,[status(thm)],[86])).
% fof(243, plain,![X20]:![X21]:![X22]:(~(admin_file_has_compartments(admin,X21,X22))|(~(admin_indi_has_compartments(admin,X20,X22))|admin_indi_has_compartments_for_file(admin,X20,X21))),inference(variable_rename,[status(thm)],[242])).
% cnf(244,plain,(admin_indi_has_compartments_for_file(admin,X1,X2)|~admin_indi_has_compartments(admin,X1,X3)|~admin_file_has_compartments(admin,X2,X3)),inference(split_conjunct,[status(thm)],[243])).
% fof(245, plain,![X1]:![X2]:![X17]:(~(admin_file_has_level(admin,X2,X17))|(~(admin_indi_has_level(admin,X1,X17))|admin_indi_has_level_for_file(admin,X1,X2))),inference(fof_nnf,[status(thm)],[87])).
% fof(246, plain,![X18]:![X19]:![X20]:(~(admin_file_has_level(admin,X19,X20))|(~(admin_indi_has_level(admin,X18,X20))|admin_indi_has_level_for_file(admin,X18,X19))),inference(variable_rename,[status(thm)],[245])).
% cnf(247,plain,(admin_indi_has_level_for_file(admin,X1,X2)|~admin_indi_has_level(admin,X1,X3)|~admin_file_has_level(admin,X2,X3)),inference(split_conjunct,[status(thm)],[246])).
% cnf(248,negated_conjecture,(~admin_indi_may_file(admin,alice,secretfile,read)),inference(split_conjunct,[status(thm)],[90])).
% cnf(249,plain,(admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)),inference(spm,[status(thm)],[168,100,theory(equality)])).
% cnf(250,plain,(admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)),inference(spm,[status(thm)],[168,97,theory(equality)])).
% cnf(252,plain,(admin_indi_has_citizenship(admin,alice,usa)),inference(spm,[status(thm)],[174,124,theory(equality)])).
% cnf(253,plain,(admin_indi_has_polygraph(admin,alice)|~system_indi_is_polygraph_admin(system,polygraph_admin)),inference(spm,[status(thm)],[148,125,theory(equality)])).
% cnf(254,plain,(admin_indi_has_polygraph(admin,alice)|$false),inference(rw,[status(thm)],[253,119,theory(equality)])).
% cnf(255,plain,(admin_indi_has_polygraph(admin,alice)),inference(cn,[status(thm)],[254,theory(equality)])).
% cnf(256,plain,(admin_indi_has_credit(admin,alice)|~system_indi_is_credit_admin(system,credit_admin)),inference(spm,[status(thm)],[151,126,theory(equality)])).
% cnf(257,plain,(admin_indi_has_credit(admin,alice)|$false),inference(rw,[status(thm)],[256,120,theory(equality)])).
% cnf(258,plain,(admin_indi_has_credit(admin,alice)),inference(cn,[status(thm)],[257,theory(equality)])).
% cnf(259,plain,(admin_indi_has_employment(admin,alice)|~system_indi_is_hr_admin(system,hr_admin)),inference(spm,[status(thm)],[154,128,theory(equality)])).
% cnf(260,plain,(admin_indi_has_employment(admin,alice)|$false),inference(rw,[status(thm)],[259,122,theory(equality)])).
% cnf(261,plain,(admin_indi_has_employment(admin,alice)),inference(cn,[status(thm)],[260,theory(equality)])).
% cnf(263,plain,(admin_indi_has_need_to_know_for_file(admin,alice,secretfile)|~state_file_has_owner(secretfile,owner_secretfile)),inference(spm,[status(thm)],[159,135,theory(equality)])).
% cnf(267,plain,(admin_indi_has_need_to_know_for_file(admin,alice,secretfile)|$false),inference(rw,[status(thm)],[263,113,theory(equality)])).
% cnf(268,plain,(admin_indi_has_need_to_know_for_file(admin,alice,secretfile)),inference(cn,[status(thm)],[267,theory(equality)])).
% cnf(271,plain,(loca_level_below(X1,X2,topsecret)|~loca_level_below(X1,X2,secret)),inference(spm,[status(thm)],[241,156,theory(equality)])).
% cnf(273,plain,(loca_level_below(X1,X2,confidential)|~loca_level_below(X1,X2,sbu)),inference(spm,[status(thm)],[241,163,theory(equality)])).
% cnf(274,plain,(loca_level_below(X1,X2,secret)|~loca_level_below(X1,X2,confidential)),inference(spm,[status(thm)],[241,165,theory(equality)])).
% cnf(275,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[142,96,theory(equality)])).
% cnf(276,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)|$false),inference(rw,[status(thm)],[275,94,theory(equality)])).
% cnf(277,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)),inference(cn,[status(thm)],[276,theory(equality)])).
% cnf(278,plain,(admin_indi_has_background(admin,X1,X2)|~background_admin_indi_has_background(X3,X1,X2)|~system_indi_is_background_admin(system,X3)),inference(spm,[status(thm)],[183,208,theory(equality)])).
% cnf(279,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmenta)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[145,96,theory(equality)])).
% cnf(280,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmenta)|$false),inference(rw,[status(thm)],[279,94,theory(equality)])).
% cnf(281,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmenta)),inference(cn,[status(thm)],[280,theory(equality)])).
% cnf(284,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~admin_indi_has_polygraph(admin,X1)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[177,95,theory(equality)])).
% cnf(285,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~admin_indi_has_polygraph(admin,X1)|$false),inference(rw,[status(thm)],[284,94,theory(equality)])).
% cnf(286,plain,(admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~admin_indi_has_polygraph(admin,X1)),inference(cn,[status(thm)],[285,theory(equality)])).
% cnf(287,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmentb)|~admin_indi_has_credit(admin,X1)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[180,95,theory(equality)])).
% cnf(288,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmentb)|~admin_indi_has_credit(admin,X1)|$false),inference(rw,[status(thm)],[287,94,theory(equality)])).
% cnf(289,plain,(admin_indi_has_credit_for_compartment(admin,X1,compartmentb)|~admin_indi_has_credit(admin,X1)),inference(cn,[status(thm)],[288,theory(equality)])).
% cnf(290,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmenta)|~admin_indi_has_background(admin,X1,unclassified)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[188,96,theory(equality)])).
% cnf(291,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmentb)|~admin_indi_has_background(admin,X1,topsecret)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[188,95,theory(equality)])).
% cnf(292,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmenta)|$false|~system_indi_is_oca(system,oca)),inference(rw,[status(thm)],[290,193,theory(equality)])).
% cnf(293,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmenta)|$false|$false),inference(rw,[status(thm)],[292,94,theory(equality)])).
% cnf(294,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmenta)),inference(cn,[status(thm)],[293,theory(equality)])).
% cnf(295,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmentb)|~admin_indi_has_background(admin,X1,topsecret)|$false),inference(rw,[status(thm)],[291,94,theory(equality)])).
% cnf(296,plain,(admin_indi_has_background_for_compartment(admin,X1,compartmentb)|~admin_indi_has_background(admin,X1,topsecret)),inference(cn,[status(thm)],[295,theory(equality)])).
% cnf(297,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[191,96,theory(equality)])).
% cnf(298,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmentb)|~admin_indi_has_level(admin,X1,confidential)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[191,95,theory(equality)])).
% cnf(299,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)|$false),inference(rw,[status(thm)],[297,94,theory(equality)])).
% cnf(300,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(cn,[status(thm)],[299,theory(equality)])).
% cnf(301,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmentb)|~admin_indi_has_level(admin,X1,confidential)|$false),inference(rw,[status(thm)],[298,94,theory(equality)])).
% cnf(302,plain,(admin_indi_has_level_for_compartment(admin,X1,compartmentb)|~admin_indi_has_level(admin,X1,confidential)),inference(cn,[status(thm)],[301,theory(equality)])).
% cnf(303,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)|~admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)|~oca_compartment_has_scg(X1,compartmenta,scg_compartmenta)|~system_indi_is_oca(system,X1)),inference(spm,[status(thm)],[171,102,theory(equality)])).
% cnf(304,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)|~admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)|~oca_compartment_has_scg(X1,compartmentb,scg_compartmentb)|~system_indi_is_oca(system,X1)),inference(spm,[status(thm)],[171,99,theory(equality)])).
% cnf(305,plain,(admin_indi_has_level(admin,X1,X2)|~admin_indi_has_background(admin,X1,X2)|~loca_level_below(admin,X2,X3)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit(admin,X1)|~admin_indi_has_polygraph(admin,X1)|~level_admin_indi_has_level(X4,X1,X3)|~system_indi_needs_level(system,X1,X2)|~system_indi_is_level_admin(system,X4)),inference(spm,[status(thm)],[223,208,theory(equality)])).
% cnf(306,plain,(admin_file_has_compartments_h(admin,X1,X2,cons(compartmenta,X3))|~admin_file_has_compartments_h(admin,X1,X2,X3)|~sso_file_has_compartments(sso_compartmenta,X1,X2)),inference(spm,[status(thm)],[200,249,theory(equality)])).
% cnf(307,plain,(admin_file_has_compartments_h(admin,X1,X2,cons(compartmentb,X3))|~admin_file_has_compartments_h(admin,X1,X2,X3)|~sso_file_has_compartments(sso_compartmentb,X1,X2)),inference(spm,[status(thm)],[200,250,theory(equality)])).
% cnf(308,plain,(admin_indi_has_background(admin,X1,X2)|~background_admin_indi_has_background(X3,X1,topsecret)|~system_indi_is_background_admin(system,X3)|~loca_level_below(admin,X2,secret)),inference(spm,[status(thm)],[183,271,theory(equality)])).
% cnf(310,plain,(admin_indi_has_compartments(admin,X1,cons(compartmenta,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_background_for_compartment(admin,X1,compartmenta)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmenta,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit_for_compartment(admin,X1,compartmenta)|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)|~sso_indi_has_compartment(X3,X1,compartmenta)|~system_indi_needs_compartment(system,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(spm,[status(thm)],[226,300,theory(equality)])).
% cnf(311,plain,(admin_indi_has_compartments(admin,X1,cons(compartmenta,X2))|~admin_indi_has_compartments(admin,X1,X2)|$false|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmenta,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit_for_compartment(admin,X1,compartmenta)|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)|~sso_indi_has_compartment(X3,X1,compartmenta)|~system_indi_needs_compartment(system,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(rw,[status(thm)],[310,294,theory(equality)])).
% cnf(312,plain,(admin_indi_has_compartments(admin,X1,cons(compartmenta,X2))|~admin_indi_has_compartments(admin,X1,X2)|$false|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmenta,X3)|~admin_indi_has_employment(admin,X1)|$false|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmenta)|~sso_indi_has_compartment(X3,X1,compartmenta)|~system_indi_needs_compartment(system,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(rw,[status(thm)],[311,281,theory(equality)])).
% cnf(313,plain,(admin_indi_has_compartments(admin,X1,cons(compartmenta,X2))|~admin_indi_has_compartments(admin,X1,X2)|$false|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmenta,X3)|~admin_indi_has_employment(admin,X1)|$false|$false|~sso_indi_has_compartment(X3,X1,compartmenta)|~system_indi_needs_compartment(system,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(rw,[status(thm)],[312,277,theory(equality)])).
% cnf(314,plain,(admin_indi_has_compartments(admin,X1,cons(compartmenta,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmenta,X3)|~admin_indi_has_employment(admin,X1)|~sso_indi_has_compartment(X3,X1,compartmenta)|~system_indi_needs_compartment(system,X1,compartmenta)|~admin_indi_has_level(admin,X1,sbu)),inference(cn,[status(thm)],[313,theory(equality)])).
% cnf(315,plain,(admin_indi_has_compartments(admin,X1,cons(compartmentb,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_background_for_compartment(admin,X1,compartmentb)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmentb,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit_for_compartment(admin,X1,compartmentb)|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~sso_indi_has_compartment(X3,X1,compartmentb)|~system_indi_needs_compartment(system,X1,compartmentb)|~admin_indi_has_level(admin,X1,confidential)),inference(spm,[status(thm)],[226,302,theory(equality)])).
% cnf(325,plain,(loca_level_below(X1,confidential,secret)),inference(spm,[status(thm)],[274,208,theory(equality)])).
% cnf(327,plain,(admin_indi_has_level(admin,X1,confidential)|~admin_indi_has_background(admin,X1,confidential)|~loca_level_below(admin,confidential,X2)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit(admin,X1)|~admin_indi_has_polygraph(admin,X1)|~level_admin_indi_has_level(X3,X1,X2)|~system_indi_needs_level(system,X1,secret)|~system_indi_is_level_admin(system,X3)),inference(spm,[status(thm)],[223,325,theory(equality)])).
% cnf(328,plain,(loca_level_below(X1,sbu,confidential)),inference(spm,[status(thm)],[273,208,theory(equality)])).
% cnf(332,plain,(loca_level_below(X1,sbu,secret)),inference(spm,[status(thm)],[274,328,theory(equality)])).
% cnf(334,plain,(admin_indi_has_level(admin,X1,sbu)|~admin_indi_has_background(admin,X1,sbu)|~loca_level_below(admin,sbu,X2)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit(admin,X1)|~admin_indi_has_polygraph(admin,X1)|~level_admin_indi_has_level(X3,X1,X2)|~system_indi_needs_level(system,X1,secret)|~system_indi_is_level_admin(system,X3)),inference(spm,[status(thm)],[223,332,theory(equality)])).
% cnf(338,plain,(admin_indi_has_background(admin,alice,topsecret)|~system_indi_is_background_admin(system,background_admin)),inference(spm,[status(thm)],[278,127,theory(equality)])).
% cnf(339,plain,(admin_indi_has_background(admin,alice,topsecret)|$false),inference(rw,[status(thm)],[338,121,theory(equality)])).
% cnf(340,plain,(admin_indi_has_background(admin,alice,topsecret)),inference(cn,[status(thm)],[339,theory(equality)])).
% cnf(350,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)|$false|~oca_compartment_has_scg(X1,compartmenta,scg_compartmenta)|~system_indi_is_oca(system,X1)),inference(rw,[status(thm)],[303,249,theory(equality)])).
% cnf(351,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)|~oca_compartment_has_scg(X1,compartmenta,scg_compartmenta)|~system_indi_is_oca(system,X1)),inference(cn,[status(thm)],[350,theory(equality)])).
% cnf(352,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[351,101,theory(equality)])).
% cnf(353,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)|$false),inference(rw,[status(thm)],[352,94,theory(equality)])).
% cnf(354,plain,(admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)),inference(cn,[status(thm)],[353,theory(equality)])).
% cnf(355,plain,(admin_file_has_level_h(admin,X1,X2,cons(compartmenta,X3))|~admin_file_has_level_h(admin,X1,X2,X3)|~admin_compartment_has_sso(admin,compartmenta,X4)|~sso_file_has_level(X4,X1,X2,scg_compartmenta)),inference(spm,[status(thm)],[217,354,theory(equality)])).
% cnf(358,plain,(admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|~system_indi_is_background_admin(system,background_admin)),inference(spm,[status(thm)],[308,127,theory(equality)])).
% cnf(359,plain,(admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false),inference(rw,[status(thm)],[358,121,theory(equality)])).
% cnf(360,plain,(admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)),inference(cn,[status(thm)],[359,theory(equality)])).
% cnf(361,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)|$false|~oca_compartment_has_scg(X1,compartmentb,scg_compartmentb)|~system_indi_is_oca(system,X1)),inference(rw,[status(thm)],[304,250,theory(equality)])).
% cnf(362,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)|~oca_compartment_has_scg(X1,compartmentb,scg_compartmentb)|~system_indi_is_oca(system,X1)),inference(cn,[status(thm)],[361,theory(equality)])).
% cnf(363,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)|~system_indi_is_oca(system,oca)),inference(spm,[status(thm)],[362,98,theory(equality)])).
% cnf(364,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)|$false),inference(rw,[status(thm)],[363,94,theory(equality)])).
% cnf(365,plain,(admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)),inference(cn,[status(thm)],[364,theory(equality)])).
% cnf(366,plain,(admin_file_has_level_h(admin,X1,X2,cons(compartmentb,X3))|~admin_file_has_level_h(admin,X1,X2,X3)|~admin_compartment_has_sso(admin,compartmentb,X4)|~sso_file_has_level(X4,X1,X2,scg_compartmentb)),inference(spm,[status(thm)],[217,365,theory(equality)])).
% cnf(374,plain,(admin_indi_has_level(admin,X1,X2)|~admin_indi_has_background(admin,X1,X2)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit(admin,X1)|~admin_indi_has_polygraph(admin,X1)|~level_admin_indi_has_level(X3,X1,topsecret)|~system_indi_needs_level(system,X1,X2)|~system_indi_is_level_admin(system,X3)|~loca_level_below(admin,X2,secret)),inference(spm,[status(thm)],[305,271,theory(equality)])).
% cnf(380,plain,(admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,X1))|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),X1)),inference(spm,[status(thm)],[306,106,theory(equality)])).
% cnf(381,plain,(admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,X1))|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),X1)),inference(spm,[status(thm)],[307,105,theory(equality)])).
% cnf(410,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)|~admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)),inference(spm,[status(thm)],[355,109,theory(equality)])).
% cnf(411,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)|$false),inference(rw,[status(thm)],[410,249,theory(equality)])).
% cnf(412,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)),inference(cn,[status(thm)],[411,theory(equality)])).
% cnf(422,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_citizenship(admin,alice,usa)|~admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)|~admin_indi_has_employment(admin,alice)|~system_indi_needs_compartment(system,alice,compartmenta)),inference(spm,[status(thm)],[314,134,theory(equality)])).
% cnf(423,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)|$false|~admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)|~admin_indi_has_employment(admin,alice)|~system_indi_needs_compartment(system,alice,compartmenta)),inference(rw,[status(thm)],[422,252,theory(equality)])).
% cnf(424,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)|$false|$false|~admin_indi_has_employment(admin,alice)|~system_indi_needs_compartment(system,alice,compartmenta)),inference(rw,[status(thm)],[423,249,theory(equality)])).
% cnf(425,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)|$false|$false|$false|~system_indi_needs_compartment(system,alice,compartmenta)),inference(rw,[status(thm)],[424,261,theory(equality)])).
% cnf(426,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)|$false|$false|$false|$false),inference(rw,[status(thm)],[425,132,theory(equality)])).
% cnf(427,plain,(admin_indi_has_compartments(admin,alice,cons(compartmenta,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,sbu)),inference(cn,[status(thm)],[426,theory(equality)])).
% cnf(428,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)|~admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)),inference(spm,[status(thm)],[366,108,theory(equality)])).
% cnf(429,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)|$false),inference(rw,[status(thm)],[428,250,theory(equality)])).
% cnf(430,plain,(admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)),inference(cn,[status(thm)],[429,theory(equality)])).
% cnf(431,plain,(admin_file_has_level(admin,secretfile,secret)|~admin_file_has_compartments(admin,secretfile,cons(compartmentb,X1))|~system_file_needs_level(system,secretfile,secret)|~admin_file_has_level_h(admin,secretfile,secret,X1)),inference(spm,[status(thm)],[232,430,theory(equality)])).
% cnf(432,plain,(admin_file_has_level(admin,secretfile,secret)|~admin_file_has_compartments(admin,secretfile,cons(compartmentb,X1))|$false|~admin_file_has_level_h(admin,secretfile,secret,X1)),inference(rw,[status(thm)],[431,107,theory(equality)])).
% cnf(433,plain,(admin_file_has_level(admin,secretfile,secret)|~admin_file_has_compartments(admin,secretfile,cons(compartmentb,X1))|~admin_file_has_level_h(admin,secretfile,secret,X1)),inference(cn,[status(thm)],[432,theory(equality)])).
% cnf(440,plain,(admin_indi_has_compartments(admin,X1,cons(compartmentb,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_level(admin,X1,confidential)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmentb,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit_for_compartment(admin,X1,compartmentb)|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~sso_indi_has_compartment(X3,X1,compartmentb)|~system_indi_needs_compartment(system,X1,compartmentb)|~admin_indi_has_background(admin,X1,topsecret)),inference(spm,[status(thm)],[315,296,theory(equality)])).
% cnf(441,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))|~system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))),inference(spm,[status(thm)],[211,381,theory(equality)])).
% cnf(442,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))|$false|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))),inference(rw,[status(thm)],[441,104,theory(equality)])).
% cnf(443,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))),inference(cn,[status(thm)],[442,theory(equality)])).
% cnf(444,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),nil)),inference(spm,[status(thm)],[443,380,theory(equality)])).
% cnf(445,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))|$false),inference(rw,[status(thm)],[444,197,theory(equality)])).
% cnf(446,plain,(admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))),inference(cn,[status(thm)],[445,theory(equality)])).
% cnf(447,plain,(admin_indi_has_compartments_for_file(admin,X1,secretfile)|~admin_indi_has_compartments(admin,X1,cons(compartmentb,cons(compartmenta,nil)))),inference(spm,[status(thm)],[244,446,theory(equality)])).
% cnf(448,plain,(admin_file_has_level(admin,secretfile,secret)|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))),inference(spm,[status(thm)],[433,446,theory(equality)])).
% cnf(451,plain,(admin_indi_has_level_for_file(admin,X1,secretfile)|~admin_indi_has_level(admin,X1,secret)|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))),inference(spm,[status(thm)],[247,448,theory(equality)])).
% cnf(453,plain,(admin_indi_may_file(admin,X1,secretfile,read)|~admin_indi_has_level_for_file(admin,X1,secretfile)|~admin_indi_has_citizenship_for_file(admin,X1,secretfile)|~admin_indi_has_need_to_know_for_file(admin,X1,secretfile)|~state_file_is_not_working_paper(secretfile)|~admin_indi_has_compartments(admin,X1,cons(compartmentb,cons(compartmenta,nil)))),inference(spm,[status(thm)],[214,447,theory(equality)])).
% cnf(454,plain,(admin_indi_may_file(admin,X1,secretfile,read)|~admin_indi_has_level_for_file(admin,X1,secretfile)|~admin_indi_has_citizenship_for_file(admin,X1,secretfile)|~admin_indi_has_need_to_know_for_file(admin,X1,secretfile)|$false|~admin_indi_has_compartments(admin,X1,cons(compartmentb,cons(compartmenta,nil)))),inference(rw,[status(thm)],[453,103,theory(equality)])).
% cnf(455,plain,(admin_indi_may_file(admin,X1,secretfile,read)|~admin_indi_has_level_for_file(admin,X1,secretfile)|~admin_indi_has_citizenship_for_file(admin,X1,secretfile)|~admin_indi_has_need_to_know_for_file(admin,X1,secretfile)|~admin_indi_has_compartments(admin,X1,cons(compartmentb,cons(compartmenta,nil)))),inference(cn,[status(thm)],[454,theory(equality)])).
% cnf(470,plain,(admin_indi_may_file(admin,X1,secretfile,read)|~admin_indi_has_citizenship_for_file(admin,X1,secretfile)|~admin_indi_has_compartments(admin,X1,cons(compartmentb,cons(compartmenta,nil)))|~admin_indi_has_need_to_know_for_file(admin,X1,secretfile)|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,X1,secret)),inference(spm,[status(thm)],[455,451,theory(equality)])).
% cnf(480,plain,(admin_indi_may_file(admin,alice,secretfile,read)|~admin_indi_has_citizenship_for_file(admin,alice,secretfile)|~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,secret)),inference(spm,[status(thm)],[470,268,theory(equality)])).
% cnf(481,plain,(~admin_indi_has_citizenship_for_file(admin,alice,secretfile)|~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,secret)),inference(sr,[status(thm)],[480,248,theory(equality)])).
% cnf(482,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|~admin_indi_has_citizenship(admin,alice,usa)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(spm,[status(thm)],[327,130,theory(equality)])).
% cnf(483,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[482,252,theory(equality)])).
% cnf(484,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|$false|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[483,261,theory(equality)])).
% cnf(485,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|$false|$false|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[484,258,theory(equality)])).
% cnf(486,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|$false|$false|$false|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[485,255,theory(equality)])).
% cnf(487,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|$false|$false|$false|$false|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[486,129,theory(equality)])).
% cnf(488,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[487,123,theory(equality)])).
% cnf(489,plain,(admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)),inference(cn,[status(thm)],[488,theory(equality)])).
% cnf(490,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,secret)|~admin_indi_has_citizenship(admin,alice,usa)),inference(spm,[status(thm)],[481,229,theory(equality)])).
% cnf(493,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,secret)|$false),inference(rw,[status(thm)],[490,252,theory(equality)])).
% cnf(494,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,secret)),inference(cn,[status(thm)],[493,theory(equality)])).
% cnf(497,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_indi_has_level(admin,alice,secret)|~admin_file_has_level_h(admin,secretfile,secret,nil)),inference(spm,[status(thm)],[494,412,theory(equality)])).
% cnf(498,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_indi_has_level(admin,alice,secret)|$false),inference(rw,[status(thm)],[497,202,theory(equality)])).
% cnf(499,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|~admin_indi_has_level(admin,alice,secret)),inference(cn,[status(thm)],[498,theory(equality)])).
% cnf(536,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|~admin_indi_has_citizenship(admin,alice,usa)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(spm,[status(thm)],[334,130,theory(equality)])).
% cnf(537,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[536,252,theory(equality)])).
% cnf(538,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|$false|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[537,261,theory(equality)])).
% cnf(539,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|$false|$false|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[538,258,theory(equality)])).
% cnf(540,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|$false|$false|$false|~system_indi_needs_level(system,alice,secret)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[539,255,theory(equality)])).
% cnf(541,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|$false|$false|$false|$false|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[540,129,theory(equality)])).
% cnf(542,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[541,123,theory(equality)])).
% cnf(543,plain,(admin_indi_has_level(admin,alice,sbu)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)),inference(cn,[status(thm)],[542,theory(equality)])).
% cnf(558,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|~admin_indi_has_citizenship(admin,alice,usa)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,X1)|~system_indi_is_level_admin(system,level_admin)),inference(spm,[status(thm)],[374,130,theory(equality)])).
% cnf(559,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,X1)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[558,252,theory(equality)])).
% cnf(560,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false|$false|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,X1)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[559,261,theory(equality)])).
% cnf(561,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false|$false|$false|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_level(system,alice,X1)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[560,258,theory(equality)])).
% cnf(562,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false|$false|$false|$false|~system_indi_needs_level(system,alice,X1)|~system_indi_is_level_admin(system,level_admin)),inference(rw,[status(thm)],[561,255,theory(equality)])).
% cnf(563,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|$false|$false|$false|$false|~system_indi_needs_level(system,alice,X1)|$false),inference(rw,[status(thm)],[562,123,theory(equality)])).
% cnf(564,plain,(admin_indi_has_level(admin,alice,X1)|~admin_indi_has_background(admin,alice,X1)|~loca_level_below(admin,X1,secret)|~system_indi_needs_level(system,alice,X1)),inference(cn,[status(thm)],[563,theory(equality)])).
% cnf(577,plain,(admin_indi_has_level(admin,alice,X1)|~loca_level_below(admin,X1,secret)|~system_indi_needs_level(system,alice,X1)),inference(csr,[status(thm)],[564,360])).
% cnf(578,plain,(admin_indi_has_level(admin,alice,secret)|~loca_level_below(admin,secret,secret)),inference(spm,[status(thm)],[577,129,theory(equality)])).
% cnf(579,plain,(admin_indi_has_level(admin,alice,secret)|$false),inference(rw,[status(thm)],[578,208,theory(equality)])).
% cnf(580,plain,(admin_indi_has_level(admin,alice,secret)),inference(cn,[status(thm)],[579,theory(equality)])).
% cnf(582,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))|$false),inference(rw,[status(thm)],[499,580,theory(equality)])).
% cnf(583,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))),inference(cn,[status(thm)],[582,theory(equality)])).
% cnf(632,plain,(admin_indi_has_compartments(admin,X1,cons(compartmentb,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_level(admin,X1,confidential)|~admin_indi_has_background(admin,X1,topsecret)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmentb,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_polygraph_for_compartment(admin,X1,compartmentb)|~sso_indi_has_compartment(X3,X1,compartmentb)|~system_indi_needs_compartment(system,X1,compartmentb)|~admin_indi_has_credit(admin,X1)),inference(spm,[status(thm)],[440,289,theory(equality)])).
% cnf(633,plain,(admin_indi_has_compartments(admin,X1,cons(compartmentb,X2))|~admin_indi_has_compartments(admin,X1,X2)|~admin_indi_has_level(admin,X1,confidential)|~admin_indi_has_background(admin,X1,topsecret)|~admin_indi_has_citizenship(admin,X1,usa)|~admin_compartment_has_sso(admin,compartmentb,X3)|~admin_indi_has_employment(admin,X1)|~admin_indi_has_credit(admin,X1)|~sso_indi_has_compartment(X3,X1,compartmentb)|~system_indi_needs_compartment(system,X1,compartmentb)|~admin_indi_has_polygraph(admin,X1)),inference(spm,[status(thm)],[632,286,theory(equality)])).
% cnf(634,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,topsecret)|~admin_indi_has_citizenship(admin,alice,usa)|~admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(spm,[status(thm)],[633,133,theory(equality)])).
% cnf(635,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|~admin_indi_has_citizenship(admin,alice,usa)|~admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[634,340,theory(equality)])).
% cnf(636,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|~admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[635,252,theory(equality)])).
% cnf(637,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|$false|~admin_indi_has_employment(admin,alice)|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[636,250,theory(equality)])).
% cnf(638,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|$false|$false|~admin_indi_has_credit(admin,alice)|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[637,261,theory(equality)])).
% cnf(639,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|$false|$false|$false|~admin_indi_has_polygraph(admin,alice)|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[638,258,theory(equality)])).
% cnf(640,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|$false|$false|$false|$false|~system_indi_needs_compartment(system,alice,compartmentb)),inference(rw,[status(thm)],[639,255,theory(equality)])).
% cnf(641,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)|$false|$false|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[640,131,theory(equality)])).
% cnf(642,plain,(admin_indi_has_compartments(admin,alice,cons(compartmentb,X1))|~admin_indi_has_compartments(admin,alice,X1)|~admin_indi_has_level(admin,alice,confidential)),inference(cn,[status(thm)],[641,theory(equality)])).
% cnf(643,plain,(~admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))|~admin_indi_has_level(admin,alice,confidential)),inference(spm,[status(thm)],[583,642,theory(equality)])).
% cnf(644,plain,(~admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_compartments(admin,alice,nil)|~admin_indi_has_level(admin,alice,sbu)),inference(spm,[status(thm)],[643,427,theory(equality)])).
% cnf(645,plain,(~admin_indi_has_level(admin,alice,confidential)|$false|~admin_indi_has_level(admin,alice,sbu)),inference(rw,[status(thm)],[644,206,theory(equality)])).
% cnf(646,plain,(~admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_level(admin,alice,sbu)),inference(cn,[status(thm)],[645,theory(equality)])).
% cnf(647,plain,(~admin_indi_has_level(admin,alice,confidential)|~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)),inference(spm,[status(thm)],[646,543,theory(equality)])).
% cnf(648,plain,(~admin_indi_has_background(admin,alice,sbu)|~loca_level_below(admin,sbu,topsecret)|~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,confidential,topsecret)),inference(spm,[status(thm)],[647,489,theory(equality)])).
% cnf(649,plain,(~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)|~loca_level_below(admin,sbu,secret)),inference(spm,[status(thm)],[648,360,theory(equality)])).
% cnf(650,plain,(~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)|$false),inference(rw,[status(thm)],[649,332,theory(equality)])).
% cnf(651,plain,(~admin_indi_has_background(admin,alice,confidential)|~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)),inference(cn,[status(thm)],[650,theory(equality)])).
% cnf(652,plain,(~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)|~loca_level_below(admin,confidential,secret)),inference(spm,[status(thm)],[651,360,theory(equality)])).
% cnf(653,plain,(~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)|$false),inference(rw,[status(thm)],[652,325,theory(equality)])).
% cnf(654,plain,(~loca_level_below(admin,sbu,topsecret)|~loca_level_below(admin,confidential,topsecret)),inference(cn,[status(thm)],[653,theory(equality)])).
% cnf(655,plain,(~loca_level_below(admin,confidential,topsecret)|~loca_level_below(admin,sbu,secret)),inference(spm,[status(thm)],[654,271,theory(equality)])).
% cnf(656,plain,(~loca_level_below(admin,confidential,topsecret)|$false),inference(rw,[status(thm)],[655,332,theory(equality)])).
% cnf(657,plain,(~loca_level_below(admin,confidential,topsecret)),inference(cn,[status(thm)],[656,theory(equality)])).
% cnf(658,plain,(~loca_level_below(admin,confidential,secret)),inference(spm,[status(thm)],[657,271,theory(equality)])).
% cnf(659,plain,($false),inference(rw,[status(thm)],[658,325,theory(equality)])).
% cnf(660,plain,($false),inference(cn,[status(thm)],[659,theory(equality)])).
% cnf(661,plain,($false),660,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 334
% # ...of these trivial : 0
% # ...subsumed : 6
% # ...remaining for further processing: 328
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 10
% # Backward-rewritten : 4
% # Generated clauses : 172
% # ...of the previous two non-trivial : 166
% # Contextual simplify-reflections : 11
% # Paramodulations : 172
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 226
% # Positive orientable unit clauses: 81
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 142
% # Current number of unprocessed clauses: 0
% # ...number of literals in the above : 0
% # Clause-clause subsumption calls (NU) : 18362
% # Rec. Clause-clause subsumption calls : 1268
% # Unit Clause-clause subsumption calls : 187
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 19
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 180 leaves, 1.95+/-1.661 terms/leaf
% # Paramod-from index: 95 leaves, 1.21+/-0.500 terms/leaf
% # Paramod-into index: 157 leaves, 1.39+/-0.949 terms/leaf
% # -------------------------------------------------
% # User time : 0.052 s
% # System time : 0.005 s
% # Total time : 0.057 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.27 WC
% FINAL PrfWatch: 0.16 CPU 0.27 WC
% SZS output end Solution for /tmp/SystemOnTPTP32518/SWV437+1.tptp
%
%------------------------------------------------------------------------------