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