%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n012.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 : 300s
% DateTime : Wed Jul 27 13:20:48 EDT 2022
% Result : Theorem 1.52s 1.74s
% Output : Refutation 1.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 21
% Syntax : Number of clauses : 30 ( 22 unt; 0 nHn; 21 RR)
% Number of literals : 51 ( 0 equ; 22 neg)
% Maximal clause size : 6 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 34 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
( ~ system_file_needs_compartments(system,A,B)
| ~ admin_file_has_compartments_h(admin,A,B,B)
| admin_file_has_compartments(admin,A,B) ),
file('SWV438+1.p',unknown),
[] ).
cnf(6,axiom,
( ~ system_file_needs_level(system,A,B)
| ~ admin_file_has_compartments(admin,A,C)
| ~ admin_file_has_level_h(admin,A,B,C)
| admin_file_has_level(admin,A,B) ),
file('SWV438+1.p',unknown),
[] ).
cnf(8,axiom,
( ~ system_file_needs_citizenship(system,A,B)
| ~ admin_file_has_compartments(admin,A,C)
| ~ admin_file_has_citizenship_h(admin,A,B,C)
| admin_file_has_citizenship(admin,A,B) ),
file('SWV438+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ admin_file_has_compartments(admin,A,B)
| ~ admin_indi_has_compartments(admin,C,B)
| admin_indi_has_compartments_for_file(admin,C,A) ),
file('SWV438+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ admin_file_has_level(admin,A,B)
| ~ admin_indi_has_level(admin,C,B)
| admin_indi_has_level_for_file(admin,C,A) ),
file('SWV438+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ state_file_has_owner(A,B)
| ~ owner_indi_has_need_to_know(B,C,A)
| admin_indi_has_need_to_know_for_file(admin,C,A) ),
file('SWV438+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ admin_file_has_citizenship(admin,A,B)
| ~ admin_indi_has_citizenship(admin,C,B)
| admin_indi_has_citizenship_for_file(admin,C,A) ),
file('SWV438+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ state_file_is_not_working_paper(A)
| ~ admin_indi_has_citizenship_for_file(admin,B,A)
| ~ admin_indi_has_need_to_know_for_file(admin,B,A)
| ~ admin_indi_has_level_for_file(admin,B,A)
| ~ admin_indi_has_compartments_for_file(admin,B,A)
| admin_indi_may_file(admin,B,A,read) ),
file('SWV438+1.p',unknown),
[] ).
cnf(30,axiom,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
file('SWV438+1.p',unknown),
[] ).
cnf(36,axiom,
admin_file_has_compartments_h(admin,A,B,nil),
file('SWV438+1.p',unknown),
[] ).
cnf(37,axiom,
admin_file_has_level_h(admin,A,B,nil),
file('SWV438+1.p',unknown),
[] ).
cnf(38,axiom,
admin_file_has_citizenship_h(admin,A,B,nil),
file('SWV438+1.p',unknown),
[] ).
cnf(40,axiom,
admin_indi_has_citizenship(admin,A,anycountry),
file('SWV438+1.p',unknown),
[] ).
cnf(41,axiom,
admin_indi_has_level(admin,A,unclassified),
file('SWV438+1.p',unknown),
[] ).
cnf(42,axiom,
admin_indi_has_compartments(admin,A,nil),
file('SWV438+1.p',unknown),
[] ).
cnf(63,axiom,
state_file_is_not_working_paper(not_secretfile),
file('SWV438+1.p',unknown),
[] ).
cnf(64,axiom,
system_file_needs_compartments(system,not_secretfile,nil),
file('SWV438+1.p',unknown),
[] ).
cnf(65,axiom,
system_file_needs_level(system,not_secretfile,unclassified),
file('SWV438+1.p',unknown),
[] ).
cnf(66,axiom,
system_file_needs_citizenship(system,not_secretfile,anycountry),
file('SWV438+1.p',unknown),
[] ).
cnf(67,axiom,
state_file_has_owner(not_secretfile,owner_not_secretfile),
file('SWV438+1.p',unknown),
[] ).
cnf(87,axiom,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),
file('SWV438+1.p',unknown),
[] ).
cnf(98,plain,
admin_file_has_compartments(admin,not_secretfile,nil),
inference(hyper,[status(thm)],[64,4,36]),
[iquote('hyper,64,4,36')] ).
cnf(108,plain,
admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile),
inference(hyper,[status(thm)],[87,25,67]),
[iquote('hyper,87,25,67')] ).
cnf(118,plain,
admin_indi_has_compartments_for_file(admin,A,not_secretfile),
inference(hyper,[status(thm)],[98,23,42]),
[iquote('hyper,98,23,42')] ).
cnf(119,plain,
admin_file_has_citizenship(admin,not_secretfile,anycountry),
inference(hyper,[status(thm)],[98,8,66,38]),
[iquote('hyper,98,8,66,38')] ).
cnf(120,plain,
admin_file_has_level(admin,not_secretfile,unclassified),
inference(hyper,[status(thm)],[98,6,65,37]),
[iquote('hyper,98,6,65,37')] ).
cnf(131,plain,
admin_indi_has_citizenship_for_file(admin,A,not_secretfile),
inference(hyper,[status(thm)],[119,26,40]),
[iquote('hyper,119,26,40')] ).
cnf(132,plain,
admin_indi_has_level_for_file(admin,A,not_secretfile),
inference(hyper,[status(thm)],[120,24,41]),
[iquote('hyper,120,24,41')] ).
cnf(140,plain,
admin_indi_may_file(admin,babu,not_secretfile,read),
inference(hyper,[status(thm)],[132,28,63,131,108,118]),
[iquote('hyper,132,28,63,131,108,118')] ).
cnf(141,plain,
$false,
inference(binary,[status(thm)],[140,30]),
[iquote('binary,140.1,30.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.12 % Command : otter-tptp-script %s
% 0.13/0.33 % Computer : n012.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Jul 27 06:05:50 EDT 2022
% 0.13/0.33 % CPUTime :
% 1.52/1.73 ----- Otter 3.3f, August 2004 -----
% 1.52/1.73 The process was started by sandbox2 on n012.cluster.edu,
% 1.52/1.73 Wed Jul 27 06:05:50 2022
% 1.52/1.73 The command was "./otter". The process ID is 24606.
% 1.52/1.73
% 1.52/1.73 set(prolog_style_variables).
% 1.52/1.73 set(auto).
% 1.52/1.73 dependent: set(auto1).
% 1.52/1.73 dependent: set(process_input).
% 1.52/1.73 dependent: clear(print_kept).
% 1.52/1.73 dependent: clear(print_new_demod).
% 1.52/1.73 dependent: clear(print_back_demod).
% 1.52/1.73 dependent: clear(print_back_sub).
% 1.52/1.73 dependent: set(control_memory).
% 1.52/1.73 dependent: assign(max_mem, 12000).
% 1.52/1.73 dependent: assign(pick_given_ratio, 4).
% 1.52/1.73 dependent: assign(stats_level, 1).
% 1.52/1.73 dependent: assign(max_seconds, 10800).
% 1.52/1.73 clear(print_given).
% 1.52/1.73
% 1.52/1.73 formula_list(usable).
% 1.52/1.73 all K loca_level_direct_below(K,unclassified,sbu).
% 1.52/1.73 all K loca_level_direct_below(K,sbu,confidential).
% 1.52/1.73 all K loca_level_direct_below(K,confidential,secret).
% 1.52/1.73 all K loca_level_direct_below(K,secret,topsecret).
% 1.52/1.73 all K L loca_level_below(K,L,L).
% 1.52/1.73 all K L L1 L11 (loca_level_direct_below(K,L1,L11)-> (loca_level_below(K,L,L1)->loca_level_below(K,L,L11))).
% 1.52/1.73 all C SSO (system_compartment_has_sso(system,C,SSO)->admin_compartment_has_sso(admin,C,SSO)).
% 1.52/1.73 all OCA C SSO SCG (system_indi_is_oca(system,OCA)-> (oca_compartment_has_scg(OCA,C,SCG)-> (admin_compartment_has_sso(admin,C,SSO)-> (sso_compartment_has_scg(SSO,C,SCG)->admin_compartment_has_scg(admin,C,SCG))))).
% 1.52/1.73 all F CL (system_file_needs_compartments(system,F,CL)-> (admin_file_has_compartments_h(admin,F,CL,CL)->admin_file_has_compartments(admin,F,CL))).
% 1.52/1.73 all F CL admin_file_has_compartments_h(admin,F,CL,nil).
% 1.52/1.73 all F CL C1 CL1 SSO (admin_compartment_has_sso(admin,C1,SSO)-> (sso_file_has_compartments(SSO,F,CL)-> (admin_file_has_compartments_h(admin,F,CL,CL1)->admin_file_has_compartments_h(admin,F,CL,cons(C1,CL1))))).
% 1.52/1.73 all F L CL (system_file_needs_level(system,F,L)-> (admin_file_has_compartments(admin,F,CL)-> (admin_file_has_level_h(admin,F,L,CL)->admin_file_has_level(admin,F,L)))).
% 1.52/1.73 all F L admin_file_has_level_h(admin,F,L,nil).
% 1.52/1.73 all F L C CL SSO SCG (admin_compartment_has_sso(admin,C,SSO)-> (admin_compartment_has_scg(admin,C,SCG)-> (sso_file_has_level(SSO,F,L,SCG)-> (admin_file_has_level_h(admin,F,L,CL)->admin_file_has_level_h(admin,F,L,cons(C,CL)))))).
% 1.52/1.73 all F U CL (system_file_needs_citizenship(system,F,U)-> (admin_file_has_compartments(admin,F,CL)-> (admin_file_has_citizenship_h(admin,F,U,CL)->admin_file_has_citizenship(admin,F,U)))).
% 1.52/1.73 all F U admin_file_has_citizenship_h(admin,F,U,nil).
% 1.52/1.73 all F U C CL SSO SCG (admin_compartment_has_sso(admin,C,SSO)-> (admin_compartment_has_scg(admin,C,SCG)-> (sso_file_has_citizenship(SSO,F,U,SCG)-> (admin_file_has_citizenship_h(admin,F,U,CL)->admin_file_has_citizenship_h(admin,F,U,cons(C,CL)))))).
% 1.52/1.73 all K PA (system_indi_is_polygraph_admin(system,PA)-> (polygraph_admin_indi_has_polygraph(PA,K)->admin_indi_has_polygraph(admin,K))).
% 1.52/1.73 all K CA (system_indi_is_credit_admin(system,CA)-> (credit_admin_indi_has_credit(CA,K)->admin_indi_has_credit(admin,K))).
% 1.52/1.73 all K admin_indi_has_background(admin,K,unclassified).
% 1.52/1.73 all K L BA L1 (system_indi_is_background_admin(system,BA)-> (background_admin_indi_has_background(BA,K,L1)-> (loca_level_below(admin,L,L1)->admin_indi_has_background(admin,K,L)))).
% 1.52/1.73 all K HR (system_indi_is_hr_admin(system,HR)-> (hr_admin_indi_has_employment(HR,K)->admin_indi_has_employment(admin,K))).
% 1.52/1.73 all K admin_indi_has_citizenship(admin,K,anycountry).
% 1.52/1.73 all K U (system_indi_has_citizenship(system,K,U)->admin_indi_has_citizenship(admin,K,U)).
% 1.52/1.73 all K admin_indi_has_level(admin,K,unclassified).
% 1.52/1.73 all K L L1 LA L11 (system_indi_needs_level(system,K,L1)-> (admin_indi_has_citizenship(admin,K,usa)-> (admin_indi_has_polygraph(admin,K)-> (admin_indi_has_employment(admin,K)-> (admin_indi_has_credit(admin,K)-> (loca_level_below(admin,L,L1)-> (system_indi_is_level_admin(system,LA)-> (level_admin_indi_has_level(LA,K,L11)-> (loca_level_below(admin,L,L11)-> (admin_indi_has_background(admin,K,L)->admin_indi_has_level(admin,K,L))))))))))).
% 1.52/1.73 all K admin_indi_has_compartments(admin,K,nil).
% 1.52/1.73 all K C CL SSO (system_indi_needs_compartment(system,K,C)-> (admin_indi_has_employment(admin,K)-> (admin_indi_has_citizenship(admin,K,usa)-> (admin_indi_has_polygraph_for_compartment(admin,K,C)-> (admin_indi_has_credit_for_compartment(admin,K,C)-> (admin_compartment_has_sso(admin,C,SSO)-> (sso_indi_has_compartment(SSO,K,C)-> (admin_indi_has_background_for_compartment(admin,K,C)-> (admin_indi_has_level_for_compartment(admin,K,C)-> (admin_indi_has_compartments(admin,K,CL)->admin_indi_has_compartments(admin,K,cons(C,CL)))))))))))).
% 1.52/1.73 all K C OCA L1 L2 B1 B2 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)-> (admin_indi_has_background(admin,K,L2)->admin_indi_has_background_for_compartment(admin,K,C)))).
% 1.52/1.73 all K C OCA L1 L2 B1 B2 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)-> (admin_indi_has_level(admin,K,L1)->admin_indi_has_level_for_compartment(admin,K,C)))).
% 1.52/1.73 all K C OCA L1 L2 B1 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,B1,yes)-> (admin_indi_has_polygraph(admin,K)->admin_indi_has_polygraph_for_compartment(admin,K,C)))).
% 1.52/1.73 all K C OCA L1 L2 B1 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,B1,no)->admin_indi_has_polygraph_for_compartment(admin,K,C))).
% 1.52/1.73 all K C OCA L1 L2 B2 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,yes,B2)-> (admin_indi_has_credit(admin,K)->admin_indi_has_credit_for_compartment(admin,K,C)))).
% 1.52/1.73 all K C OCA L1 L2 B2 (system_indi_is_oca(system,OCA)-> (oca_compartment_is_compartment(OCA,C,L1,L2,no,B2)->admin_indi_has_credit_for_compartment(admin,K,C))).
% 1.52/1.73 all K F CL (admin_file_has_compartments(admin,F,CL)-> (admin_indi_has_compartments(admin,K,CL)->admin_indi_has_compartments_for_file(admin,K,F))).
% 1.52/1.73 all K F L (admin_file_has_level(admin,F,L)-> (admin_indi_has_level(admin,K,L)->admin_indi_has_level_for_file(admin,K,F))).
% 1.52/1.73 all K F OWR (state_file_has_owner(F,OWR)-> (owner_indi_has_need_to_know(OWR,K,F)->admin_indi_has_need_to_know_for_file(admin,K,F))).
% 1.52/1.73 all K F L (admin_file_has_citizenship(admin,F,L)-> (admin_indi_has_citizenship(admin,K,L)->admin_indi_has_citizenship_for_file(admin,K,F))).
% 1.52/1.73 all K F (admin_indi_has_citizenship(admin,K,usa)->admin_indi_has_citizenship_for_file(admin,K,F)).
% 1.52/1.73 all K F (state_file_is_not_working_paper(F)-> (admin_indi_has_citizenship_for_file(admin,K,F)-> (admin_indi_has_need_to_know_for_file(admin,K,F)-> (admin_indi_has_level_for_file(admin,K,F)-> (admin_indi_has_compartments_for_file(admin,K,F)->admin_indi_may_file(admin,K,F,read)))))).
% 1.52/1.73 all K F K1 (state_file_has_owner(F,K1)-> (system_indi_is_counterintelligence(system,K,K1)->admin_indi_may_file(admin,K,F,read))).
% 1.52/1.73 system_indi_is_oca(system,oca).
% 1.52/1.73 oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes).
% 1.52/1.73 oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no).
% 1.52/1.73 system_compartment_has_sso(system,compartmentb,sso_compartmentb).
% 1.52/1.73 oca_compartment_has_scg(oca,compartmentb,scg_compartmentb).
% 1.52/1.73 sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb).
% 1.52/1.73 system_compartment_has_sso(system,compartmenta,sso_compartmenta).
% 1.52/1.73 oca_compartment_has_scg(oca,compartmenta,scg_compartmenta).
% 1.52/1.73 sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta).
% 1.52/1.73 state_file_is_not_working_paper(secretfile).
% 1.52/1.73 system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 system_file_needs_level(system,secretfile,secret).
% 1.52/1.73 sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb).
% 1.52/1.73 sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta).
% 1.52/1.73 system_file_needs_citizenship(system,secretfile,usa).
% 1.52/1.73 sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb).
% 1.52/1.73 sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta).
% 1.52/1.73 state_file_has_owner(secretfile,owner_secretfile).
% 1.52/1.73 state_file_is_not_working_paper(not_secretfile).
% 1.52/1.73 system_file_needs_compartments(system,not_secretfile,nil).
% 1.52/1.73 system_file_needs_level(system,not_secretfile,unclassified).
% 1.52/1.73 system_file_needs_citizenship(system,not_secretfile,anycountry).
% 1.52/1.73 state_file_has_owner(not_secretfile,owner_not_secretfile).
% 1.52/1.73 system_indi_is_polygraph_admin(system,polygraph_admin).
% 1.52/1.73 system_indi_is_credit_admin(system,credit_admin).
% 1.52/1.73 system_indi_is_background_admin(system,background_admin).
% 1.52/1.73 system_indi_is_hr_admin(system,hr_admin).
% 1.52/1.73 system_indi_is_level_admin(system,level_admin).
% 1.52/1.73 system_indi_has_citizenship(system,alice,usa).
% 1.52/1.73 polygraph_admin_indi_has_polygraph(polygraph_admin,alice).
% 1.52/1.73 credit_admin_indi_has_credit(credit_admin,alice).
% 1.52/1.73 background_admin_indi_has_background(background_admin,alice,topsecret).
% 1.52/1.73 hr_admin_indi_has_employment(hr_admin,alice).
% 1.52/1.73 system_indi_needs_level(system,alice,secret).
% 1.52/1.73 level_admin_indi_has_level(level_admin,alice,topsecret).
% 1.52/1.73 system_indi_needs_compartment(system,alice,compartmentb).
% 1.52/1.73 system_indi_needs_compartment(system,alice,compartmenta).
% 1.52/1.73 sso_indi_has_compartment(sso_compartmentb,alice,compartmentb).
% 1.52/1.73 sso_indi_has_compartment(sso_compartmenta,alice,compartmenta).
% 1.52/1.73 owner_indi_has_need_to_know(owner_secretfile,alice,secretfile).
% 1.52/1.73 owner_indi_has_need_to_know(owner_secretfile,alice,not_secretfile).
% 1.52/1.73 system_indi_has_citizenship(system,babu,india).
% 1.52/1.73 owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile).
% 1.52/1.73 system_indi_is_counterintelligence(system,ci,owner_secretfile).
% 1.52/1.73 -admin_indi_may_file(admin,babu,not_secretfile,read).
% 1.52/1.73 end_of_list.
% 1.52/1.73
% 1.52/1.73 -------> usable clausifies to:
% 1.52/1.73
% 1.52/1.73 list(usable).
% 1.52/1.73 0 [] loca_level_direct_below(K,unclassified,sbu).
% 1.52/1.73 0 [] loca_level_direct_below(K,sbu,confidential).
% 1.52/1.73 0 [] loca_level_direct_below(K,confidential,secret).
% 1.52/1.73 0 [] loca_level_direct_below(K,secret,topsecret).
% 1.52/1.73 0 [] loca_level_below(K,L,L).
% 1.52/1.73 0 [] -loca_level_direct_below(K,L1,L11)| -loca_level_below(K,L,L1)|loca_level_below(K,L,L11).
% 1.52/1.73 0 [] -system_compartment_has_sso(system,C,SSO)|admin_compartment_has_sso(admin,C,SSO).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_has_scg(OCA,C,SCG)| -admin_compartment_has_sso(admin,C,SSO)| -sso_compartment_has_scg(SSO,C,SCG)|admin_compartment_has_scg(admin,C,SCG).
% 1.52/1.73 0 [] -system_file_needs_compartments(system,F,CL)| -admin_file_has_compartments_h(admin,F,CL,CL)|admin_file_has_compartments(admin,F,CL).
% 1.52/1.73 0 [] admin_file_has_compartments_h(admin,F,CL,nil).
% 1.52/1.73 0 [] -admin_compartment_has_sso(admin,C1,SSO)| -sso_file_has_compartments(SSO,F,CL)| -admin_file_has_compartments_h(admin,F,CL,CL1)|admin_file_has_compartments_h(admin,F,CL,cons(C1,CL1)).
% 1.52/1.73 0 [] -system_file_needs_level(system,F,L)| -admin_file_has_compartments(admin,F,CL)| -admin_file_has_level_h(admin,F,L,CL)|admin_file_has_level(admin,F,L).
% 1.52/1.73 0 [] admin_file_has_level_h(admin,F,L,nil).
% 1.52/1.73 0 [] -admin_compartment_has_sso(admin,C,SSO)| -admin_compartment_has_scg(admin,C,SCG)| -sso_file_has_level(SSO,F,L,SCG)| -admin_file_has_level_h(admin,F,L,CL)|admin_file_has_level_h(admin,F,L,cons(C,CL)).
% 1.52/1.73 0 [] -system_file_needs_citizenship(system,F,U)| -admin_file_has_compartments(admin,F,CL)| -admin_file_has_citizenship_h(admin,F,U,CL)|admin_file_has_citizenship(admin,F,U).
% 1.52/1.73 0 [] admin_file_has_citizenship_h(admin,F,U,nil).
% 1.52/1.73 0 [] -admin_compartment_has_sso(admin,C,SSO)| -admin_compartment_has_scg(admin,C,SCG)| -sso_file_has_citizenship(SSO,F,U,SCG)| -admin_file_has_citizenship_h(admin,F,U,CL)|admin_file_has_citizenship_h(admin,F,U,cons(C,CL)).
% 1.52/1.73 0 [] -system_indi_is_polygraph_admin(system,PA)| -polygraph_admin_indi_has_polygraph(PA,K)|admin_indi_has_polygraph(admin,K).
% 1.52/1.73 0 [] -system_indi_is_credit_admin(system,CA)| -credit_admin_indi_has_credit(CA,K)|admin_indi_has_credit(admin,K).
% 1.52/1.73 0 [] admin_indi_has_background(admin,K,unclassified).
% 1.52/1.73 0 [] -system_indi_is_background_admin(system,BA)| -background_admin_indi_has_background(BA,K,L1)| -loca_level_below(admin,L,L1)|admin_indi_has_background(admin,K,L).
% 1.52/1.73 0 [] -system_indi_is_hr_admin(system,HR)| -hr_admin_indi_has_employment(HR,K)|admin_indi_has_employment(admin,K).
% 1.52/1.73 0 [] admin_indi_has_citizenship(admin,K,anycountry).
% 1.52/1.73 0 [] -system_indi_has_citizenship(system,K,U)|admin_indi_has_citizenship(admin,K,U).
% 1.52/1.73 0 [] admin_indi_has_level(admin,K,unclassified).
% 1.52/1.73 0 [] -system_indi_needs_level(system,K,L1)| -admin_indi_has_citizenship(admin,K,usa)| -admin_indi_has_polygraph(admin,K)| -admin_indi_has_employment(admin,K)| -admin_indi_has_credit(admin,K)| -loca_level_below(admin,L,L1)| -system_indi_is_level_admin(system,LA)| -level_admin_indi_has_level(LA,K,L11)| -loca_level_below(admin,L,L11)| -admin_indi_has_background(admin,K,L)|admin_indi_has_level(admin,K,L).
% 1.52/1.73 0 [] admin_indi_has_compartments(admin,K,nil).
% 1.52/1.73 0 [] -system_indi_needs_compartment(system,K,C)| -admin_indi_has_employment(admin,K)| -admin_indi_has_citizenship(admin,K,usa)| -admin_indi_has_polygraph_for_compartment(admin,K,C)| -admin_indi_has_credit_for_compartment(admin,K,C)| -admin_compartment_has_sso(admin,C,SSO)| -sso_indi_has_compartment(SSO,K,C)| -admin_indi_has_background_for_compartment(admin,K,C)| -admin_indi_has_level_for_compartment(admin,K,C)| -admin_indi_has_compartments(admin,K,CL)|admin_indi_has_compartments(admin,K,cons(C,CL)).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)| -admin_indi_has_background(admin,K,L2)|admin_indi_has_background_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,B1,B2)| -admin_indi_has_level(admin,K,L1)|admin_indi_has_level_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,B1,yes)| -admin_indi_has_polygraph(admin,K)|admin_indi_has_polygraph_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,B1,no)|admin_indi_has_polygraph_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,yes,B2)| -admin_indi_has_credit(admin,K)|admin_indi_has_credit_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -system_indi_is_oca(system,OCA)| -oca_compartment_is_compartment(OCA,C,L1,L2,no,B2)|admin_indi_has_credit_for_compartment(admin,K,C).
% 1.52/1.73 0 [] -admin_file_has_compartments(admin,F,CL)| -admin_indi_has_compartments(admin,K,CL)|admin_indi_has_compartments_for_file(admin,K,F).
% 1.52/1.73 0 [] -admin_file_has_level(admin,F,L)| -admin_indi_has_level(admin,K,L)|admin_indi_has_level_for_file(admin,K,F).
% 1.52/1.73 0 [] -state_file_has_owner(F,OWR)| -owner_indi_has_need_to_know(OWR,K,F)|admin_indi_has_need_to_know_for_file(admin,K,F).
% 1.52/1.73 0 [] -admin_file_has_citizenship(admin,F,L)| -admin_indi_has_citizenship(admin,K,L)|admin_indi_has_citizenship_for_file(admin,K,F).
% 1.52/1.73 0 [] -admin_indi_has_citizenship(admin,K,usa)|admin_indi_has_citizenship_for_file(admin,K,F).
% 1.52/1.73 0 [] -state_file_is_not_working_paper(F)| -admin_indi_has_citizenship_for_file(admin,K,F)| -admin_indi_has_need_to_know_for_file(admin,K,F)| -admin_indi_has_level_for_file(admin,K,F)| -admin_indi_has_compartments_for_file(admin,K,F)|admin_indi_may_file(admin,K,F,read).
% 1.52/1.73 0 [] -state_file_has_owner(F,K1)| -system_indi_is_counterintelligence(system,K,K1)|admin_indi_may_file(admin,K,F,read).
% 1.52/1.73 0 [] system_indi_is_oca(system,oca).
% 1.52/1.73 0 [] oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes).
% 1.52/1.73 0 [] oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no).
% 1.52/1.73 0 [] system_compartment_has_sso(system,compartmentb,sso_compartmentb).
% 1.52/1.73 0 [] oca_compartment_has_scg(oca,compartmentb,scg_compartmentb).
% 1.52/1.73 0 [] sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb).
% 1.52/1.73 0 [] system_compartment_has_sso(system,compartmenta,sso_compartmenta).
% 1.52/1.73 0 [] oca_compartment_has_scg(oca,compartmenta,scg_compartmenta).
% 1.52/1.73 0 [] sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta).
% 1.52/1.73 0 [] state_file_is_not_working_paper(secretfile).
% 1.52/1.73 0 [] system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 0 [] sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 0 [] sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 0 [] system_file_needs_level(system,secretfile,secret).
% 1.52/1.73 0 [] sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb).
% 1.52/1.73 0 [] sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta).
% 1.52/1.73 0 [] system_file_needs_citizenship(system,secretfile,usa).
% 1.52/1.73 0 [] sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb).
% 1.52/1.73 0 [] sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta).
% 1.52/1.73 0 [] state_file_has_owner(secretfile,owner_secretfile).
% 1.52/1.73 0 [] state_file_is_not_working_paper(not_secretfile).
% 1.52/1.73 0 [] system_file_needs_compartments(system,not_secretfile,nil).
% 1.52/1.73 0 [] system_file_needs_level(system,not_secretfile,unclassified).
% 1.52/1.73 0 [] system_file_needs_citizenship(system,not_secretfile,anycountry).
% 1.52/1.73 0 [] state_file_has_owner(not_secretfile,owner_not_secretfile).
% 1.52/1.73 0 [] system_indi_is_polygraph_admin(system,polygraph_admin).
% 1.52/1.73 0 [] system_indi_is_credit_admin(system,credit_admin).
% 1.52/1.73 0 [] system_indi_is_background_admin(system,background_admin).
% 1.52/1.73 0 [] system_indi_is_hr_admin(system,hr_admin).
% 1.52/1.73 0 [] system_indi_is_level_admin(system,level_admin).
% 1.52/1.73 0 [] system_indi_has_citizenship(system,alice,usa).
% 1.52/1.73 0 [] polygraph_admin_indi_has_polygraph(polygraph_admin,alice).
% 1.52/1.73 0 [] credit_admin_indi_has_credit(credit_admin,alice).
% 1.52/1.73 0 [] background_admin_indi_has_background(background_admin,alice,topsecret).
% 1.52/1.73 0 [] hr_admin_indi_has_employment(hr_admin,alice).
% 1.52/1.73 0 [] system_indi_needs_level(system,alice,secret).
% 1.52/1.73 0 [] level_admin_indi_has_level(level_admin,alice,topsecret).
% 1.52/1.73 0 [] system_indi_needs_compartment(system,alice,compartmentb).
% 1.52/1.73 0 [] system_indi_needs_compartment(system,alice,compartmenta).
% 1.52/1.73 0 [] sso_indi_has_compartment(sso_compartmentb,alice,compartmentb).
% 1.52/1.73 0 [] sso_indi_has_compartment(sso_compartmenta,alice,compartmenta).
% 1.52/1.73 0 [] owner_indi_has_need_to_know(owner_secretfile,alice,secretfile).
% 1.52/1.73 0 [] owner_indi_has_need_to_know(owner_secretfile,alice,not_secretfile).
% 1.52/1.73 0 [] system_indi_has_citizenship(system,babu,india).
% 1.52/1.73 0 [] owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile).
% 1.52/1.73 0 [] system_indi_is_counterintelligence(system,ci,owner_secretfile).
% 1.52/1.73 0 [] -admin_indi_may_file(admin,babu,not_secretfile,read).
% 1.52/1.73 end_of_list.
% 1.52/1.73
% 1.52/1.73 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=11.
% 1.52/1.73
% 1.52/1.73 This is a Horn set without equality. The strategy will
% 1.52/1.73 be hyperresolution, with satellites in sos and nuclei
% 1.52/1.73 in usable.
% 1.52/1.73
% 1.52/1.73 dependent: set(hyper_res).
% 1.52/1.73 dependent: clear(order_hyper).
% 1.52/1.73
% 1.52/1.73 ------------> process usable:
% 1.52/1.73 ** KEPT (pick-wt=12): 1 [] -loca_level_direct_below(A,B,C)| -loca_level_below(A,D,B)|loca_level_below(A,D,C).
% 1.52/1.73 ** KEPT (pick-wt=8): 2 [] -system_compartment_has_sso(system,A,B)|admin_compartment_has_sso(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=19): 3 [] -system_indi_is_oca(system,A)| -oca_compartment_has_scg(A,B,C)| -admin_compartment_has_sso(admin,B,D)| -sso_compartment_has_scg(D,B,C)|admin_compartment_has_scg(admin,B,C).
% 1.52/1.73 ** KEPT (pick-wt=13): 4 [] -system_file_needs_compartments(system,A,B)| -admin_file_has_compartments_h(admin,A,B,B)|admin_file_has_compartments(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=20): 5 [] -admin_compartment_has_sso(admin,A,B)| -sso_file_has_compartments(B,C,D)| -admin_file_has_compartments_h(admin,C,D,E)|admin_file_has_compartments_h(admin,C,D,cons(A,E)).
% 1.52/1.73 ** KEPT (pick-wt=17): 6 [] -system_file_needs_level(system,A,B)| -admin_file_has_compartments(admin,A,C)| -admin_file_has_level_h(admin,A,B,C)|admin_file_has_level(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=25): 7 [] -admin_compartment_has_sso(admin,A,B)| -admin_compartment_has_scg(admin,A,C)| -sso_file_has_level(B,D,E,C)| -admin_file_has_level_h(admin,D,E,F)|admin_file_has_level_h(admin,D,E,cons(A,F)).
% 1.52/1.73 ** KEPT (pick-wt=17): 8 [] -system_file_needs_citizenship(system,A,B)| -admin_file_has_compartments(admin,A,C)| -admin_file_has_citizenship_h(admin,A,B,C)|admin_file_has_citizenship(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=25): 9 [] -admin_compartment_has_sso(admin,A,B)| -admin_compartment_has_scg(admin,A,C)| -sso_file_has_citizenship(B,D,E,C)| -admin_file_has_citizenship_h(admin,D,E,F)|admin_file_has_citizenship_h(admin,D,E,cons(A,F)).
% 1.52/1.73 ** KEPT (pick-wt=9): 10 [] -system_indi_is_polygraph_admin(system,A)| -polygraph_admin_indi_has_polygraph(A,B)|admin_indi_has_polygraph(admin,B).
% 1.52/1.73 ** KEPT (pick-wt=9): 11 [] -system_indi_is_credit_admin(system,A)| -credit_admin_indi_has_credit(A,B)|admin_indi_has_credit(admin,B).
% 1.52/1.73 ** KEPT (pick-wt=15): 12 [] -system_indi_is_background_admin(system,A)| -background_admin_indi_has_background(A,B,C)| -loca_level_below(admin,D,C)|admin_indi_has_background(admin,B,D).
% 1.52/1.73 ** KEPT (pick-wt=9): 13 [] -system_indi_is_hr_admin(system,A)| -hr_admin_indi_has_employment(A,B)|admin_indi_has_employment(admin,B).
% 1.52/1.73 ** KEPT (pick-wt=8): 14 [] -system_indi_has_citizenship(system,A,B)|admin_indi_has_citizenship(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=40): 15 [] -system_indi_needs_level(system,A,B)| -admin_indi_has_citizenship(admin,A,usa)| -admin_indi_has_polygraph(admin,A)| -admin_indi_has_employment(admin,A)| -admin_indi_has_credit(admin,A)| -loca_level_below(admin,C,B)| -system_indi_is_level_admin(system,D)| -level_admin_indi_has_level(D,A,E)| -loca_level_below(admin,C,E)| -admin_indi_has_background(admin,A,C)|admin_indi_has_level(admin,A,C).
% 1.52/1.73 ** KEPT (pick-wt=45): 16 [] -system_indi_needs_compartment(system,A,B)| -admin_indi_has_employment(admin,A)| -admin_indi_has_citizenship(admin,A,usa)| -admin_indi_has_polygraph_for_compartment(admin,A,B)| -admin_indi_has_credit_for_compartment(admin,A,B)| -admin_compartment_has_sso(admin,B,C)| -sso_indi_has_compartment(C,A,B)| -admin_indi_has_background_for_compartment(admin,A,B)| -admin_indi_has_level_for_compartment(admin,A,B)| -admin_indi_has_compartments(admin,A,D)|admin_indi_has_compartments(admin,A,cons(B,D)).
% 1.52/1.73 ** KEPT (pick-wt=18): 17 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,E,F)| -admin_indi_has_background(admin,G,D)|admin_indi_has_background_for_compartment(admin,G,B).
% 1.52/1.73 ** KEPT (pick-wt=18): 18 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,E,F)| -admin_indi_has_level(admin,G,C)|admin_indi_has_level_for_compartment(admin,G,B).
% 1.52/1.73 ** KEPT (pick-wt=17): 19 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,E,yes)| -admin_indi_has_polygraph(admin,F)|admin_indi_has_polygraph_for_compartment(admin,F,B).
% 1.52/1.73 ** KEPT (pick-wt=14): 20 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,E,no)|admin_indi_has_polygraph_for_compartment(admin,F,B).
% 1.52/1.73 ** KEPT (pick-wt=17): 21 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,yes,E)| -admin_indi_has_credit(admin,F)|admin_indi_has_credit_for_compartment(admin,F,B).
% 1.52/1.73 ** KEPT (pick-wt=14): 22 [] -system_indi_is_oca(system,A)| -oca_compartment_is_compartment(A,B,C,D,no,E)|admin_indi_has_credit_for_compartment(admin,F,B).
% 1.52/1.73 ** KEPT (pick-wt=12): 23 [] -admin_file_has_compartments(admin,A,B)| -admin_indi_has_compartments(admin,C,B)|admin_indi_has_compartments_for_file(admin,C,A).
% 1.52/1.73 ** KEPT (pick-wt=12): 24 [] -admin_file_has_level(admin,A,B)| -admin_indi_has_level(admin,C,B)|admin_indi_has_level_for_file(admin,C,A).
% 1.52/1.73 ** KEPT (pick-wt=11): 25 [] -state_file_has_owner(A,B)| -owner_indi_has_need_to_know(B,C,A)|admin_indi_has_need_to_know_for_file(admin,C,A).
% 1.52/1.73 ** KEPT (pick-wt=12): 26 [] -admin_file_has_citizenship(admin,A,B)| -admin_indi_has_citizenship(admin,C,B)|admin_indi_has_citizenship_for_file(admin,C,A).
% 1.52/1.73 ** KEPT (pick-wt=8): 27 [] -admin_indi_has_citizenship(admin,A,usa)|admin_indi_has_citizenship_for_file(admin,A,B).
% 1.52/1.73 ** KEPT (pick-wt=23): 28 [] -state_file_is_not_working_paper(A)| -admin_indi_has_citizenship_for_file(admin,B,A)| -admin_indi_has_need_to_know_for_file(admin,B,A)| -admin_indi_has_level_for_file(admin,B,A)| -admin_indi_has_compartments_for_file(admin,B,A)|admin_indi_may_file(admin,B,A,read).
% 1.52/1.73 ** KEPT (pick-wt=12): 29 [] -state_file_has_owner(A,B)| -system_indi_is_counterintelligence(system,C,B)|admin_indi_may_file(admin,C,A,read).
% 1.52/1.73 ** KEPT (pick-wt=5): 30 [] -admin_indi_may_file(admin,babu,not_secretfile,read).
% 1.52/1.73
% 1.52/1.73 ------------> process sos:
% 1.52/1.73 ** KEPT (pick-wt=4): 31 [] loca_level_direct_below(A,unclassified,sbu).
% 1.52/1.73 ** KEPT (pick-wt=4): 32 [] loca_level_direct_below(A,sbu,confidential).
% 1.52/1.73 ** KEPT (pick-wt=4): 33 [] loca_level_direct_below(A,confidential,secret).
% 1.52/1.73 ** KEPT (pick-wt=4): 34 [] loca_level_direct_below(A,secret,topsecret).
% 1.52/1.73 ** KEPT (pick-wt=4): 35 [] loca_level_below(A,B,B).
% 1.52/1.73 ** KEPT (pick-wt=5): 36 [] admin_file_has_compartments_h(admin,A,B,nil).
% 1.52/1.73 ** KEPT (pick-wt=5): 37 [] admin_file_has_level_h(admin,A,B,nil).
% 1.52/1.73 ** KEPT (pick-wt=5): 38 [] admin_file_has_citizenship_h(admin,A,B,nil).
% 1.52/1.73 ** KEPT (pick-wt=4): 39 [] admin_indi_has_background(admin,A,unclassified).
% 1.52/1.73 ** KEPT (pick-wt=4): 40 [] admin_indi_has_citizenship(admin,A,anycountry).
% 1.52/1.73 ** KEPT (pick-wt=4): 41 [] admin_indi_has_level(admin,A,unclassified).
% 1.52/1.73 ** KEPT (pick-wt=4): 42 [] admin_indi_has_compartments(admin,A,nil).
% 1.52/1.73 ** KEPT (pick-wt=3): 43 [] system_indi_is_oca(system,oca).
% 1.52/1.73 ** KEPT (pick-wt=7): 44 [] oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes).
% 1.52/1.73 ** KEPT (pick-wt=7): 45 [] oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no).
% 1.52/1.73 ** KEPT (pick-wt=4): 46 [] system_compartment_has_sso(system,compartmentb,sso_compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=4): 47 [] oca_compartment_has_scg(oca,compartmentb,scg_compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=4): 48 [] sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=4): 49 [] system_compartment_has_sso(system,compartmenta,sso_compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=4): 50 [] oca_compartment_has_scg(oca,compartmenta,scg_compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=4): 51 [] sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=2): 52 [] state_file_is_not_working_paper(secretfile).
% 1.52/1.73 ** KEPT (pick-wt=8): 53 [] system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 ** KEPT (pick-wt=8): 54 [] sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 ** KEPT (pick-wt=8): 55 [] sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.52/1.73 ** KEPT (pick-wt=4): 56 [] system_file_needs_level(system,secretfile,secret).
% 1.52/1.73 ** KEPT (pick-wt=5): 57 [] sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=5): 58 [] sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=4): 59 [] system_file_needs_citizenship(system,secretfile,usa).
% 1.52/1.73 ** KEPT (pick-wt=5): 60 [] sso_file_has_citizenship(sso_compartmentb,secretfile,usa,scg_compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=5): 61 [] sso_file_has_citizenship(sso_compartmenta,secretfile,usa,scg_compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=3): 62 [] state_file_has_owner(secretfile,owner_secretfile).
% 1.52/1.73 ** KEPT (pick-wt=2): 63 [] state_file_is_not_working_paper(not_secretfile).
% 1.52/1.73 ** KEPT (pick-wt=4): 64 [] system_file_needs_compartments(system,not_secretfile,nil).
% 1.52/1.73 ** KEPT (pick-wt=4): 65 [] system_file_needs_level(system,not_secretfile,unclassified).
% 1.52/1.73 ** KEPT (pick-wt=4): 66 [] system_file_needs_citizenship(system,not_secretfile,anycountry).
% 1.52/1.73 ** KEPT (pick-wt=3): 67 [] state_file_has_owner(not_secretfile,owner_not_secretfile).
% 1.52/1.73 ** KEPT (pick-wt=3): 68 [] system_indi_is_polygraph_admin(system,polygraph_admin).
% 1.52/1.73 ** KEPT (pick-wt=3): 69 [] system_indi_is_credit_admin(system,credit_admin).
% 1.52/1.73 ** KEPT (pick-wt=3): 70 [] system_indi_is_background_admin(system,background_admin).
% 1.52/1.73 ** KEPT (pick-wt=3): 71 [] system_indi_is_hr_admin(system,hr_admin).
% 1.52/1.73 ** KEPT (pick-wt=3): 72 [] system_indi_is_level_admin(system,level_admin).
% 1.52/1.73 ** KEPT (pick-wt=4): 73 [] system_indi_has_citizenship(system,alice,usa).
% 1.52/1.73 ** KEPT (pick-wt=3): 74 [] polygraph_admin_indi_has_polygraph(polygraph_admin,alice).
% 1.52/1.73 ** KEPT (pick-wt=3): 75 [] credit_admin_indi_has_credit(credit_admin,alice).
% 1.52/1.73 ** KEPT (pick-wt=4): 76 [] background_admin_indi_has_background(background_admin,alice,topsecret).
% 1.52/1.73 ** KEPT (pick-wt=3): 77 [] hr_admin_indi_has_employment(hr_admin,alice).
% 1.52/1.73 ** KEPT (pick-wt=4): 78 [] system_indi_needs_level(system,alice,secret).
% 1.52/1.73 ** KEPT (pick-wt=4): 79 [] level_admin_indi_has_level(level_admin,alice,topsecret).
% 1.52/1.73 ** KEPT (pick-wt=4): 80 [] system_indi_needs_compartment(system,alice,compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=4): 81 [] system_indi_needs_compartment(system,alice,compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=4): 82 [] sso_indi_has_compartment(sso_compartmentb,alice,compartmentb).
% 1.52/1.73 ** KEPT (pick-wt=4): 83 [] sso_indi_has_compartment(sso_compartmenta,alice,compartmenta).
% 1.52/1.73 ** KEPT (pick-wt=4): 84 [] owner_indi_has_need_to_know(owner_secretfile,alice,secretfile).
% 1.52/1.74 ** KEPT (pick-wt=4): 85 [] owner_indi_has_need_to_know(owner_secretfile,alice,not_secretfile).
% 1.52/1.74 ** KEPT (pick-wt=4): 86 [] system_indi_has_citizenship(system,babu,india).
% 1.52/1.74 ** KEPT (pick-wt=4): 87 [] owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile).
% 1.52/1.74 ** KEPT (pick-wt=4): 88 [] system_indi_is_counterintelligence(system,ci,owner_secretfile).
% 1.52/1.74
% 1.52/1.74 ======= end of input processing =======
% 1.52/1.74
% 1.52/1.74 =========== start of search ===========
% 1.52/1.74
% 1.52/1.74 -------- PROOF --------
% 1.52/1.74
% 1.52/1.74 ----> UNIT CONFLICT at 0.01 sec ----> 141 [binary,140.1,30.1] $F.
% 1.52/1.74
% 1.52/1.74 Length of proof is 8. Level of proof is 4.
% 1.52/1.74
% 1.52/1.74 ---------------- PROOF ----------------
% 1.52/1.74 % SZS status Theorem
% 1.52/1.74 % SZS output start Refutation
% See solution above
% 1.52/1.74 ------------ end of proof -------------
% 1.52/1.74
% 1.52/1.74
% 1.52/1.74 Search stopped by max_proofs option.
% 1.52/1.74
% 1.52/1.74
% 1.52/1.74 Search stopped by max_proofs option.
% 1.52/1.74
% 1.52/1.74 ============ end of search ============
% 1.52/1.74
% 1.52/1.74 -------------- statistics -------------
% 1.52/1.74 clauses given 98
% 1.52/1.74 clauses generated 52
% 1.52/1.74 clauses kept 140
% 1.52/1.74 clauses forward subsumed 0
% 1.52/1.74 clauses back subsumed 0
% 1.52/1.74 Kbytes malloced 2929
% 1.52/1.74
% 1.52/1.74 ----------- times (seconds) -----------
% 1.52/1.74 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.52/1.74 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.52/1.74 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.52/1.74
% 1.52/1.74 That finishes the proof of the theorem.
% 1.52/1.74
% 1.52/1.74 Process 24606 finished Wed Jul 27 06:05:52 2022
% 1.52/1.74 Otter interrupted
% 1.52/1.74 PROOF FOUND
%------------------------------------------------------------------------------