%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:43:06 EDT 2022
% Result : Theorem 0.19s 0.49s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 68
% Syntax : Number of clauses : 175 ( 55 unt; 0 nHn; 175 RR)
% Number of literals : 608 ( 0 equ; 468 neg)
% Maximal clause size : 12 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 51 ( 50 usr; 1 prp; 0-6 aty)
% Number of functors : 35 ( 35 usr; 34 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
state_file_is_not_working_paper(secretfile),
file('SWV437+1.p',unknown),
[] ).
cnf(3,axiom,
system_indi_is_oca(system,oca),
file('SWV437+1.p',unknown),
[] ).
cnf(4,axiom,
state_file_has_owner(secretfile,owner_secretfile),
file('SWV437+1.p',unknown),
[] ).
cnf(6,axiom,
system_indi_is_polygraph_admin(system,polygraph_admin),
file('SWV437+1.p',unknown),
[] ).
cnf(7,axiom,
system_indi_is_credit_admin(system,credit_admin),
file('SWV437+1.p',unknown),
[] ).
cnf(8,axiom,
system_indi_is_background_admin(system,background_admin),
file('SWV437+1.p',unknown),
[] ).
cnf(9,axiom,
system_indi_is_hr_admin(system,hr_admin),
file('SWV437+1.p',unknown),
[] ).
cnf(10,axiom,
system_indi_is_level_admin(system,level_admin),
file('SWV437+1.p',unknown),
[] ).
cnf(11,axiom,
polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
file('SWV437+1.p',unknown),
[] ).
cnf(12,axiom,
credit_admin_indi_has_credit(credit_admin,alice),
file('SWV437+1.p',unknown),
[] ).
cnf(13,axiom,
hr_admin_indi_has_employment(hr_admin,alice),
file('SWV437+1.p',unknown),
[] ).
cnf(14,axiom,
system_compartment_has_sso(system,compartmentb,sso_compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(15,axiom,
oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(16,axiom,
sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(17,axiom,
system_compartment_has_sso(system,compartmenta,sso_compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(18,axiom,
oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(19,axiom,
sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(20,axiom,
system_file_needs_level(system,secretfile,secret),
file('SWV437+1.p',unknown),
[] ).
cnf(25,axiom,
system_indi_has_citizenship(system,alice,usa),
file('SWV437+1.p',unknown),
[] ).
cnf(26,axiom,
background_admin_indi_has_background(background_admin,alice,topsecret),
file('SWV437+1.p',unknown),
[] ).
cnf(27,axiom,
system_indi_needs_level(system,alice,secret),
file('SWV437+1.p',unknown),
[] ).
cnf(28,axiom,
level_admin_indi_has_level(level_admin,alice,topsecret),
file('SWV437+1.p',unknown),
[] ).
cnf(29,axiom,
system_indi_needs_compartment(system,alice,compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(30,axiom,
system_indi_needs_compartment(system,alice,compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(31,axiom,
sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(32,axiom,
sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(33,axiom,
owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
file('SWV437+1.p',unknown),
[] ).
cnf(39,axiom,
loca_level_direct_below(u,sbu,confidential),
file('SWV437+1.p',unknown),
[] ).
cnf(40,axiom,
loca_level_direct_below(u,confidential,secret),
file('SWV437+1.p',unknown),
[] ).
cnf(41,axiom,
loca_level_direct_below(u,secret,topsecret),
file('SWV437+1.p',unknown),
[] ).
cnf(42,axiom,
loca_level_below(u,v,v),
file('SWV437+1.p',unknown),
[] ).
cnf(43,axiom,
admin_indi_has_background(admin,u,unclassified),
file('SWV437+1.p',unknown),
[] ).
cnf(46,axiom,
admin_indi_has_compartments(admin,u,nil),
file('SWV437+1.p',unknown),
[] ).
cnf(47,axiom,
sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
file('SWV437+1.p',unknown),
[] ).
cnf(48,axiom,
sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
file('SWV437+1.p',unknown),
[] ).
cnf(51,axiom,
admin_file_has_compartments_h(admin,u,v,nil),
file('SWV437+1.p',unknown),
[] ).
cnf(52,axiom,
admin_file_has_level_h(admin,u,v,nil),
file('SWV437+1.p',unknown),
[] ).
cnf(54,axiom,
~ admin_indi_may_file(admin,alice,secretfile,read),
file('SWV437+1.p',unknown),
[] ).
cnf(55,axiom,
oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
file('SWV437+1.p',unknown),
[] ).
cnf(56,axiom,
oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
file('SWV437+1.p',unknown),
[] ).
cnf(57,axiom,
system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('SWV437+1.p',unknown),
[] ).
cnf(58,axiom,
sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('SWV437+1.p',unknown),
[] ).
cnf(59,axiom,
sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
file('SWV437+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ system_compartment_has_sso(system,u,v)
| admin_compartment_has_sso(admin,u,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(61,axiom,
( ~ system_indi_has_citizenship(system,u,v)
| admin_indi_has_citizenship(admin,u,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ admin_indi_has_citizenship(admin,u,usa)
| admin_indi_has_citizenship_for_file(admin,u,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(63,axiom,
( ~ polygraph_admin_indi_has_polygraph(u,v)
| ~ system_indi_is_polygraph_admin(system,u)
| admin_indi_has_polygraph(admin,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ credit_admin_indi_has_credit(u,v)
| ~ system_indi_is_credit_admin(system,u)
| admin_indi_has_credit(admin,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(65,axiom,
( ~ hr_admin_indi_has_employment(u,v)
| ~ system_indi_is_hr_admin(system,u)
| admin_indi_has_employment(admin,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(66,axiom,
( ~ state_file_has_owner(u,v)
| ~ owner_indi_has_need_to_know(v,w,u)
| admin_indi_has_need_to_know_for_file(admin,w,u) ),
file('SWV437+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ loca_level_direct_below(u,v,w)
| ~ loca_level_below(u,x,v)
| loca_level_below(u,x,w) ),
file('SWV437+1.p',unknown),
[] ).
cnf(68,axiom,
( ~ admin_file_has_compartments(admin,u,v)
| ~ admin_indi_has_compartments(admin,w,v)
| admin_indi_has_compartments_for_file(admin,w,u) ),
file('SWV437+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ admin_file_has_level(admin,u,v)
| ~ admin_indi_has_level(admin,w,v)
| admin_indi_has_level_for_file(admin,w,u) ),
file('SWV437+1.p',unknown),
[] ).
cnf(72,axiom,
( ~ system_file_needs_compartments(system,u,v)
| ~ admin_file_has_compartments_h(admin,u,v,v)
| admin_file_has_compartments(admin,u,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ system_indi_is_oca(system,u)
| ~ oca_compartment_is_compartment(u,v,w,x,y,no)
| admin_indi_has_polygraph_for_compartment(admin,z,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(74,axiom,
( ~ system_indi_is_oca(system,u)
| ~ oca_compartment_is_compartment(u,v,w,x,no,y)
| admin_indi_has_credit_for_compartment(admin,z,v) ),
file('SWV437+1.p',unknown),
[] ).
cnf(75,axiom,
( ~ system_indi_is_background_admin(system,u)
| ~ background_admin_indi_has_background(u,v,w)
| ~ loca_level_below(admin,x,w)
| admin_indi_has_background(admin,v,x) ),
file('SWV437+1.p',unknown),
[] ).
cnf(76,axiom,
( ~ system_indi_is_oca(system,u)
| ~ admin_indi_has_credit(admin,v)
| ~ oca_compartment_is_compartment(u,w,x,y,yes,z)
| admin_indi_has_credit_for_compartment(admin,v,w) ),
file('SWV437+1.p',unknown),
[] ).
cnf(77,axiom,
( ~ system_indi_is_oca(system,u)
| ~ admin_indi_has_polygraph(admin,v)
| ~ oca_compartment_is_compartment(u,w,x,y,z,yes)
| admin_indi_has_polygraph_for_compartment(admin,v,w) ),
file('SWV437+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ admin_file_has_compartments(admin,u,v)
| ~ system_file_needs_level(system,u,w)
| ~ admin_file_has_level_h(admin,u,w,v)
| admin_file_has_level(admin,u,w) ),
file('SWV437+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ system_indi_is_oca(system,u)
| ~ admin_indi_has_level(admin,v,w)
| ~ oca_compartment_is_compartment(u,x,w,y,z,x1)
| admin_indi_has_level_for_compartment(admin,v,x) ),
file('SWV437+1.p',unknown),
[] ).
cnf(81,axiom,
( ~ system_indi_is_oca(system,u)
| ~ admin_indi_has_background(admin,v,w)
| ~ oca_compartment_is_compartment(u,x,y,w,z,x1)
| admin_indi_has_background_for_compartment(admin,v,x) ),
file('SWV437+1.p',unknown),
[] ).
cnf(82,axiom,
( ~ sso_file_has_compartments(u,v,w)
| ~ admin_compartment_has_sso(admin,x,u)
| ~ admin_file_has_compartments_h(admin,v,w,y)
| admin_file_has_compartments_h(admin,v,w,cons(x,y)) ),
file('SWV437+1.p',unknown),
[] ).
cnf(83,axiom,
( ~ system_indi_is_oca(system,u)
| ~ oca_compartment_has_scg(u,v,w)
| ~ sso_compartment_has_scg(x,v,w)
| ~ admin_compartment_has_sso(admin,v,x)
| admin_compartment_has_scg(admin,v,w) ),
file('SWV437+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ state_file_is_not_working_paper(u)
| ~ admin_indi_has_citizenship_for_file(admin,v,u)
| ~ admin_indi_has_compartments_for_file(admin,v,u)
| ~ admin_indi_has_level_for_file(admin,v,u)
| ~ admin_indi_has_need_to_know_for_file(admin,v,u)
| admin_indi_may_file(admin,v,u,read) ),
file('SWV437+1.p',unknown),
[] ).
cnf(86,axiom,
( ~ admin_compartment_has_scg(admin,u,v)
| ~ admin_compartment_has_sso(admin,u,w)
| ~ sso_file_has_level(w,x,y,v)
| ~ admin_file_has_level_h(admin,x,y,z)
| admin_file_has_level_h(admin,x,y,cons(u,z)) ),
file('SWV437+1.p',unknown),
[] ).
cnf(87,axiom,
( ~ system_indi_is_level_admin(system,u)
| ~ admin_indi_has_credit(admin,v)
| ~ admin_indi_has_employment(admin,v)
| ~ admin_indi_has_polygraph(admin,v)
| ~ level_admin_indi_has_level(u,v,w)
| ~ loca_level_below(admin,x,y)
| ~ loca_level_below(admin,x,w)
| ~ admin_indi_has_background(admin,v,x)
| ~ system_indi_needs_level(system,v,y)
| ~ admin_indi_has_citizenship(admin,v,usa)
| admin_indi_has_level(admin,v,x) ),
file('SWV437+1.p',unknown),
[] ).
cnf(88,axiom,
( ~ admin_indi_has_employment(admin,u)
| ~ sso_indi_has_compartment(v,u,w)
| ~ admin_compartment_has_sso(admin,w,v)
| ~ system_indi_needs_compartment(system,u,w)
| ~ admin_indi_has_polygraph_for_compartment(admin,u,w)
| ~ admin_indi_has_credit_for_compartment(admin,u,w)
| ~ admin_indi_has_background_for_compartment(admin,u,w)
| ~ admin_indi_has_level_for_compartment(admin,u,w)
| ~ admin_indi_has_compartments(admin,u,x)
| ~ admin_indi_has_citizenship(admin,u,usa)
| admin_indi_has_compartments(admin,u,cons(w,x)) ),
file('SWV437+1.p',unknown),
[] ).
cnf(90,plain,
( ~ state_file_is_not_working_paper(secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[84,54]),
[iquote('0:Res:84.5,54.0')] ).
cnf(91,plain,
( ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,alice,secretfile) ),
inference(mrr,[status(thm)],[90,1]),
[iquote('0:MRR:90.0,1.0')] ).
cnf(94,plain,
( ~ system_indi_is_hr_admin(system,hr_admin)
| admin_indi_has_employment(admin,alice) ),
inference(res,[status(thm),theory(equality)],[13,65]),
[iquote('0:Res:13.0,65.0')] ).
cnf(95,plain,
admin_indi_has_employment(admin,alice),
inference(mrr,[status(thm)],[94,9]),
[iquote('0:MRR:94.0,9.0')] ).
cnf(96,plain,
( ~ system_indi_is_credit_admin(system,credit_admin)
| admin_indi_has_credit(admin,alice) ),
inference(res,[status(thm),theory(equality)],[12,64]),
[iquote('0:Res:12.0,64.0')] ).
cnf(97,plain,
admin_indi_has_credit(admin,alice),
inference(mrr,[status(thm)],[96,7]),
[iquote('0:MRR:96.0,7.0')] ).
cnf(98,plain,
( ~ system_indi_is_polygraph_admin(system,polygraph_admin)
| admin_indi_has_polygraph(admin,alice) ),
inference(res,[status(thm),theory(equality)],[11,63]),
[iquote('0:Res:11.0,63.0')] ).
cnf(99,plain,
admin_indi_has_polygraph(admin,alice),
inference(mrr,[status(thm)],[98,6]),
[iquote('0:MRR:98.0,6.0')] ).
cnf(102,plain,
( ~ state_file_has_owner(secretfile,owner_secretfile)
| admin_indi_has_need_to_know_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[33,66]),
[iquote('0:Res:33.0,66.1')] ).
cnf(104,plain,
admin_indi_has_need_to_know_for_file(admin,alice,secretfile),
inference(mrr,[status(thm)],[102,4]),
[iquote('0:MRR:102.0,4.0')] ).
cnf(105,plain,
( ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile)
| ~ admin_indi_has_level_for_file(admin,alice,secretfile) ),
inference(mrr,[status(thm)],[91,104]),
[iquote('0:MRR:91.3,104.0')] ).
cnf(107,plain,
( ~ loca_level_below(u,v,secret)
| loca_level_below(u,v,topsecret) ),
inference(res,[status(thm),theory(equality)],[41,67]),
[iquote('0:Res:41.0,67.0')] ).
cnf(108,plain,
( ~ loca_level_below(u,v,confidential)
| loca_level_below(u,v,secret) ),
inference(res,[status(thm),theory(equality)],[40,67]),
[iquote('0:Res:40.0,67.0')] ).
cnf(109,plain,
( ~ loca_level_below(u,v,sbu)
| loca_level_below(u,v,confidential) ),
inference(res,[status(thm),theory(equality)],[39,67]),
[iquote('0:Res:39.0,67.0')] ).
cnf(114,plain,
loca_level_below(u,confidential,secret),
inference(res,[status(thm),theory(equality)],[42,108]),
[iquote('0:Res:42.0,108.0')] ).
cnf(115,plain,
( ~ system_indi_is_oca(system,oca)
| admin_indi_has_credit_for_compartment(admin,u,compartmenta) ),
inference(res,[status(thm),theory(equality)],[56,74]),
[iquote('0:Res:56.0,74.1')] ).
cnf(116,plain,
admin_indi_has_credit_for_compartment(admin,u,compartmenta),
inference(mrr,[status(thm)],[115,3]),
[iquote('0:MRR:115.0,3.0')] ).
cnf(117,plain,
( ~ loca_level_below(u,v,sbu)
| loca_level_below(u,v,secret) ),
inference(res,[status(thm),theory(equality)],[109,108]),
[iquote('0:Res:109.1,108.0')] ).
cnf(118,plain,
( ~ system_indi_is_oca(system,oca)
| admin_indi_has_polygraph_for_compartment(admin,u,compartmenta) ),
inference(res,[status(thm),theory(equality)],[56,73]),
[iquote('0:Res:56.0,73.1')] ).
cnf(119,plain,
admin_indi_has_polygraph_for_compartment(admin,u,compartmenta),
inference(mrr,[status(thm)],[118,3]),
[iquote('0:MRR:118.0,3.0')] ).
cnf(120,plain,
loca_level_below(u,sbu,secret),
inference(res,[status(thm),theory(equality)],[42,117]),
[iquote('0:Res:42.0,117.0')] ).
cnf(123,plain,
( ~ system_indi_is_background_admin(system,background_admin)
| ~ loca_level_below(admin,u,topsecret)
| admin_indi_has_background(admin,alice,u) ),
inference(res,[status(thm),theory(equality)],[26,75]),
[iquote('0:Res:26.0,75.1')] ).
cnf(124,plain,
( ~ loca_level_below(admin,u,topsecret)
| admin_indi_has_background(admin,alice,u) ),
inference(mrr,[status(thm)],[123,8]),
[iquote('0:MRR:123.0,8.0')] ).
cnf(131,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_credit(admin,u)
| admin_indi_has_credit_for_compartment(admin,u,compartmentb) ),
inference(res,[status(thm),theory(equality)],[55,76]),
[iquote('0:Res:55.0,76.2')] ).
cnf(132,plain,
( ~ admin_indi_has_credit(admin,u)
| admin_indi_has_credit_for_compartment(admin,u,compartmentb) ),
inference(mrr,[status(thm)],[131,3]),
[iquote('0:MRR:131.0,3.0')] ).
cnf(136,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_polygraph(admin,u)
| admin_indi_has_polygraph_for_compartment(admin,u,compartmentb) ),
inference(res,[status(thm),theory(equality)],[55,77]),
[iquote('0:Res:55.0,77.2')] ).
cnf(137,plain,
( ~ admin_indi_has_polygraph(admin,u)
| admin_indi_has_polygraph_for_compartment(admin,u,compartmentb) ),
inference(mrr,[status(thm)],[136,3]),
[iquote('0:MRR:136.0,3.0')] ).
cnf(141,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_background(admin,u,unclassified)
| admin_indi_has_background_for_compartment(admin,u,compartmenta) ),
inference(res,[status(thm),theory(equality)],[56,81]),
[iquote('0:Res:56.0,81.2')] ).
cnf(142,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_background(admin,u,topsecret)
| admin_indi_has_background_for_compartment(admin,u,compartmentb) ),
inference(res,[status(thm),theory(equality)],[55,81]),
[iquote('0:Res:55.0,81.2')] ).
cnf(143,plain,
admin_indi_has_background_for_compartment(admin,u,compartmenta),
inference(mrr,[status(thm)],[141,3,43]),
[iquote('0:MRR:141.0,141.1,3.0,43.0')] ).
cnf(144,plain,
( ~ admin_indi_has_background(admin,u,topsecret)
| admin_indi_has_background_for_compartment(admin,u,compartmentb) ),
inference(mrr,[status(thm)],[142,3]),
[iquote('0:MRR:142.0,3.0')] ).
cnf(145,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_level(admin,u,sbu)
| admin_indi_has_level_for_compartment(admin,u,compartmenta) ),
inference(res,[status(thm),theory(equality)],[56,80]),
[iquote('0:Res:56.0,80.2')] ).
cnf(146,plain,
( ~ system_indi_is_oca(system,oca)
| ~ admin_indi_has_level(admin,u,confidential)
| admin_indi_has_level_for_compartment(admin,u,compartmentb) ),
inference(res,[status(thm),theory(equality)],[55,80]),
[iquote('0:Res:55.0,80.2')] ).
cnf(147,plain,
( ~ admin_indi_has_level(admin,u,sbu)
| admin_indi_has_level_for_compartment(admin,u,compartmenta) ),
inference(mrr,[status(thm)],[145,3]),
[iquote('0:MRR:145.0,3.0')] ).
cnf(148,plain,
( ~ admin_indi_has_level(admin,u,confidential)
| admin_indi_has_level_for_compartment(admin,u,compartmentb) ),
inference(mrr,[status(thm)],[146,3]),
[iquote('0:MRR:146.0,3.0')] ).
cnf(149,plain,
( ~ system_indi_is_oca(system,oca)
| ~ sso_compartment_has_scg(u,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,u)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(res,[status(thm),theory(equality)],[18,83]),
[iquote('0:Res:18.0,83.1')] ).
cnf(150,plain,
( ~ system_indi_is_oca(system,oca)
| ~ sso_compartment_has_scg(u,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,u)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(res,[status(thm),theory(equality)],[15,83]),
[iquote('0:Res:15.0,83.1')] ).
cnf(151,plain,
( ~ sso_compartment_has_scg(u,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,u)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(mrr,[status(thm)],[149,3]),
[iquote('0:MRR:149.0,3.0')] ).
cnf(152,plain,
( ~ sso_compartment_has_scg(u,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,u)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(mrr,[status(thm)],[150,3]),
[iquote('0:MRR:150.0,3.0')] ).
cnf(153,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) ),
inference(res,[status(thm),theory(equality)],[19,151]),
[iquote('0:Res:19.0,151.0')] ).
cnf(154,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) ),
inference(res,[status(thm),theory(equality)],[16,152]),
[iquote('0:Res:16.0,152.0')] ).
cnf(155,plain,
( ~ sso_file_has_compartments(u,v,w)
| ~ admin_compartment_has_sso(admin,x,u)
| admin_file_has_compartments_h(admin,v,w,cons(x,nil)) ),
inference(res,[status(thm),theory(equality)],[51,82]),
[iquote('0:Res:51.0,82.2')] ).
cnf(156,plain,
( ~ admin_compartment_has_sso(admin,u,sso_compartmenta)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(u,nil)) ),
inference(res,[status(thm),theory(equality)],[59,155]),
[iquote('0:Res:59.0,155.0')] ).
cnf(158,plain,
( ~ admin_compartment_has_sso(admin,u,sso_compartmenta)
| ~ sso_file_has_compartments(v,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| ~ admin_compartment_has_sso(admin,w,v)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(w,cons(u,nil))) ),
inference(res,[status(thm),theory(equality)],[156,82]),
[iquote('0:Res:156.1,82.2')] ).
cnf(161,plain,
( ~ admin_compartment_has_scg(admin,u,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,u,sso_compartmenta)
| ~ admin_file_has_level_h(admin,secretfile,secret,v)
| admin_file_has_level_h(admin,secretfile,secret,cons(u,v)) ),
inference(res,[status(thm),theory(equality)],[48,86]),
[iquote('0:Res:48.0,86.2')] ).
cnf(162,plain,
( ~ admin_compartment_has_scg(admin,u,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,u,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,v)
| admin_file_has_level_h(admin,secretfile,secret,cons(u,v)) ),
inference(res,[status(thm),theory(equality)],[47,86]),
[iquote('0:Res:47.0,86.2')] ).
cnf(163,plain,
( ~ admin_compartment_has_scg(admin,u,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,u,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,v)
| ~ admin_file_has_compartments(admin,secretfile,cons(u,v))
| ~ system_file_needs_level(system,secretfile,secret)
| admin_file_has_level(admin,secretfile,secret) ),
inference(res,[status(thm),theory(equality)],[162,79]),
[iquote('0:Res:162.3,79.2')] ).
cnf(164,plain,
( ~ admin_compartment_has_scg(admin,u,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,u,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,v)
| ~ admin_file_has_compartments(admin,secretfile,cons(u,v))
| admin_file_has_level(admin,secretfile,secret) ),
inference(mrr,[status(thm)],[163,20]),
[iquote('0:MRR:163.4,20.0')] ).
cnf(173,plain,
( ~ system_indi_is_level_admin(system,level_admin)
| ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_employment(admin,alice)
| ~ admin_indi_has_polygraph(admin,alice)
| ~ loca_level_below(admin,u,v)
| ~ loca_level_below(admin,u,topsecret)
| ~ admin_indi_has_background(admin,alice,u)
| ~ system_indi_needs_level(system,alice,v)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,u) ),
inference(res,[status(thm),theory(equality)],[28,87]),
[iquote('0:Res:28.0,87.4')] ).
cnf(174,plain,
( ~ loca_level_below(admin,u,v)
| ~ loca_level_below(admin,u,topsecret)
| ~ system_indi_needs_level(system,alice,v)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,u) ),
inference(mrr,[status(thm)],[173,10,97,95,99,124]),
[iquote('0:MRR:173.0,173.1,173.2,173.3,173.6,10.0,97.0,95.0,99.0,124.1')] ).
cnf(175,plain,
( ~ loca_level_below(admin,u,topsecret)
| ~ system_indi_needs_level(system,alice,u)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,u) ),
inference(res,[status(thm),theory(equality)],[42,174]),
[iquote('0:Res:42.0,174.0')] ).
cnf(179,plain,
( ~ loca_level_below(admin,confidential,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,confidential) ),
inference(res,[status(thm),theory(equality)],[114,174]),
[iquote('0:Res:114.0,174.0')] ).
cnf(180,plain,
( ~ loca_level_below(admin,sbu,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,sbu) ),
inference(res,[status(thm),theory(equality)],[120,174]),
[iquote('0:Res:120.0,174.0')] ).
cnf(182,plain,
( ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,confidential) ),
inference(mrr,[status(thm)],[179,27]),
[iquote('0:MRR:179.1,27.0')] ).
cnf(183,plain,
( ~ loca_level_below(admin,sbu,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_level(admin,alice,sbu) ),
inference(mrr,[status(thm)],[180,27]),
[iquote('0:MRR:180.1,27.0')] ).
cnf(185,plain,
( ~ admin_indi_has_employment(admin,alice)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ system_indi_needs_compartment(system,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_compartments(admin,alice,u)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_compartments(admin,alice,cons(compartmenta,u)) ),
inference(res,[status(thm),theory(equality)],[32,88]),
[iquote('0:Res:32.0,88.1')] ).
cnf(186,plain,
( ~ admin_indi_has_employment(admin,alice)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ system_indi_needs_compartment(system,alice,compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_compartments(admin,alice,u)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,u)) ),
inference(res,[status(thm),theory(equality)],[31,88]),
[iquote('0:Res:31.0,88.1')] ).
cnf(187,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_compartments(admin,alice,u)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_compartments(admin,alice,cons(compartmentb,u)) ),
inference(mrr,[status(thm)],[186,95,29]),
[iquote('0:MRR:186.0,186.2,95.0,29.0')] ).
cnf(188,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_compartments(admin,alice,u)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| admin_indi_has_compartments(admin,alice,cons(compartmenta,u)) ),
inference(mrr,[status(thm)],[185,95,30,119,116,143]),
[iquote('0:MRR:185.0,185.2,185.3,185.4,185.5,95.0,30.0,119.0,116.0,143.0')] ).
cnf(190,plain,
( ~ admin_compartment_has_sso(admin,u,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,v,sso_compartmentb)
| admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(v,cons(u,nil))) ),
inference(res,[status(thm),theory(equality)],[58,158]),
[iquote('0:Res:58.0,158.1')] ).
cnf(191,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(res,[status(thm),theory(equality)],[190,72]),
[iquote('0:Res:190.2,72.1')] ).
cnf(193,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) ),
inference(mrr,[status(thm)],[191,57]),
[iquote('0:MRR:191.2,57.0')] ).
cnf(194,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_compartments(admin,u,cons(compartmentb,cons(compartmenta,nil)))
| admin_indi_has_compartments_for_file(admin,u,secretfile) ),
inference(res,[status(thm),theory(equality)],[193,68]),
[iquote('0:Res:193.2,68.0')] ).
cnf(198,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))
| admin_file_has_level(admin,secretfile,secret) ),
inference(res,[status(thm),theory(equality)],[193,164]),
[iquote('0:Res:193.2,164.3')] ).
cnf(199,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))
| admin_file_has_level(admin,secretfile,secret) ),
inference(obv,[status(thm),theory(equality)],[198]),
[iquote('0:Obv:198.1')] ).
cnf(200,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))
| admin_file_has_level(admin,secretfile,secret) ),
inference(mrr,[status(thm)],[199,154]),
[iquote('0:MRR:199.1,154.1')] ).
cnf(205,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_file_has_level_h(admin,secretfile,secret,nil)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_level(admin,secretfile,secret) ),
inference(res,[status(thm),theory(equality)],[161,200]),
[iquote('0:Res:161.3,200.2')] ).
cnf(208,plain,
( ~ admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)
| ~ admin_file_has_level_h(admin,secretfile,secret,nil)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_level(admin,secretfile,secret) ),
inference(obv,[status(thm),theory(equality)],[205]),
[iquote('0:Obv:205.1')] ).
cnf(209,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_file_has_level(admin,secretfile,secret) ),
inference(mrr,[status(thm)],[208,153,52]),
[iquote('0:MRR:208.0,208.1,153.1,52.0')] ).
cnf(210,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,u,secret)
| admin_indi_has_level_for_file(admin,u,secretfile) ),
inference(res,[status(thm),theory(equality)],[209,69]),
[iquote('0:Res:209.2,69.0')] ).
cnf(211,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret)
| ~ admin_indi_has_citizenship_for_file(admin,alice,secretfile)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[210,105]),
[iquote('0:Res:210.3,105.2')] ).
cnf(228,plain,
( ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[187,194]),
[iquote('0:Res:187.7,194.2')] ).
cnf(229,plain,
( ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(obv,[status(thm),theory(equality)],[228]),
[iquote('0:Obv:228.0')] ).
cnf(269,plain,
( ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret)
| ~ admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[62,211]),
[iquote('0:Res:62.1,211.3')] ).
cnf(316,plain,
( ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(res,[status(thm),theory(equality)],[188,229]),
[iquote('0:Res:188.4,229.4')] ).
cnf(317,plain,
( ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_compartments(admin,alice,nil)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(obv,[status(thm),theory(equality)],[316]),
[iquote('0:Obv:316.3')] ).
cnf(318,plain,
( ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| admin_indi_has_compartments_for_file(admin,alice,secretfile) ),
inference(mrr,[status(thm)],[317,46]),
[iquote('0:MRR:317.1,46.0')] ).
cnf(321,plain,
( ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[318,269]),
[iquote('0:Res:318.8,269.4')] ).
cnf(322,plain,
( ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_background_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(obv,[status(thm),theory(equality)],[321]),
[iquote('0:Obv:321.7')] ).
cnf(323,plain,
( ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[144,322]),
[iquote('0:Res:144.1,322.3')] ).
cnf(324,plain,
( ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_level_for_compartment(admin,alice,compartmenta)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[148,323]),
[iquote('0:Res:148.1,323.4')] ).
cnf(325,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[147,324]),
[iquote('0:Res:147.1,324.2')] ).
cnf(330,plain,
( ~ admin_indi_has_polygraph(admin,alice)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[137,325]),
[iquote('0:Res:137.1,325.3')] ).
cnf(331,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_credit_for_compartment(admin,alice,compartmentb)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(mrr,[status(thm)],[330,99]),
[iquote('0:MRR:330.0,99.0')] ).
cnf(332,plain,
( ~ admin_indi_has_credit(admin,alice)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[132,331]),
[iquote('0:Res:132.1,331.3')] ).
cnf(333,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(mrr,[status(thm)],[332,97]),
[iquote('0:MRR:332.0,97.0')] ).
cnf(336,plain,
( ~ system_compartment_has_sso(system,compartmentb,sso_compartmentb)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[60,333]),
[iquote('0:Res:60.1,333.5')] ).
cnf(337,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(mrr,[status(thm)],[336,14]),
[iquote('0:MRR:336.0,14.0')] ).
cnf(338,plain,
( ~ system_compartment_has_sso(system,compartmenta,sso_compartmenta)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[60,337]),
[iquote('0:Res:60.1,337.4')] ).
cnf(339,plain,
( ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_level(admin,alice,confidential)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(mrr,[status(thm)],[338,17]),
[iquote('0:MRR:338.0,17.0')] ).
cnf(344,plain,
( ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[182,339]),
[iquote('0:Res:182.2,339.1')] ).
cnf(345,plain,
( ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_level(admin,alice,sbu)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(obv,[status(thm),theory(equality)],[344]),
[iquote('0:Obv:344.1')] ).
cnf(355,plain,
( ~ loca_level_below(admin,sbu,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(res,[status(thm),theory(equality)],[183,345]),
[iquote('0:Res:183.2,345.1')] ).
cnf(356,plain,
( ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ admin_indi_has_level(admin,alice,secret) ),
inference(obv,[status(thm),theory(equality)],[355]),
[iquote('0:Obv:355.1')] ).
cnf(392,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| ~ admin_indi_has_citizenship(admin,alice,usa)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa) ),
inference(res,[status(thm),theory(equality)],[175,356]),
[iquote('0:Res:175.3,356.4')] ).
cnf(393,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ system_indi_needs_level(system,alice,secret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa) ),
inference(obv,[status(thm),theory(equality)],[392]),
[iquote('0:Obv:392.2')] ).
cnf(394,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_background(admin,alice,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa) ),
inference(mrr,[status(thm)],[393,27]),
[iquote('0:MRR:393.1,27.0')] ).
cnf(397,plain,
( ~ loca_level_below(admin,topsecret,topsecret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa) ),
inference(res,[status(thm),theory(equality)],[124,394]),
[iquote('0:Res:124.1,394.3')] ).
cnf(398,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret)
| ~ admin_indi_has_citizenship(admin,alice,usa) ),
inference(mrr,[status(thm)],[397,42]),
[iquote('0:MRR:397.0,42.0')] ).
cnf(399,plain,
( ~ system_indi_has_citizenship(system,alice,usa)
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret) ),
inference(res,[status(thm),theory(equality)],[61,398]),
[iquote('0:Res:61.1,398.3')] ).
cnf(400,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret)
| ~ loca_level_below(admin,confidential,topsecret) ),
inference(mrr,[status(thm)],[399,25]),
[iquote('0:MRR:399.0,25.0')] ).
cnf(403,plain,
( ~ loca_level_below(admin,confidential,secret)
| ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(res,[status(thm),theory(equality)],[107,400]),
[iquote('0:Res:107.1,400.2')] ).
cnf(404,plain,
( ~ loca_level_below(admin,secret,topsecret)
| ~ loca_level_below(admin,sbu,topsecret) ),
inference(mrr,[status(thm)],[403,114]),
[iquote('0:MRR:403.0,114.0')] ).
cnf(405,plain,
( ~ loca_level_below(admin,sbu,secret)
| ~ loca_level_below(admin,secret,topsecret) ),
inference(res,[status(thm),theory(equality)],[107,404]),
[iquote('0:Res:107.1,404.1')] ).
cnf(406,plain,
~ loca_level_below(admin,secret,topsecret),
inference(mrr,[status(thm)],[405,120]),
[iquote('0:MRR:405.0,120.0')] ).
cnf(407,plain,
~ loca_level_below(admin,secret,secret),
inference(res,[status(thm),theory(equality)],[107,406]),
[iquote('0:Res:107.1,406.0')] ).
cnf(408,plain,
$false,
inference(mrr,[status(thm)],[407,42]),
[iquote('0:MRR:407.0,42.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.13 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 16 02:22:48 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.49
% 0.19/0.49 SPASS V 3.9
% 0.19/0.49 SPASS beiseite: Proof found.
% 0.19/0.49 % SZS status Theorem
% 0.19/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.49 SPASS derived 206 clauses, backtracked 0 clauses, performed 0 splits and kept 259 clauses.
% 0.19/0.49 SPASS allocated 98019 KBytes.
% 0.19/0.49 SPASS spent 0:00:00.14 on the problem.
% 0.19/0.49 0:00:00.03 for the input.
% 0.19/0.49 0:00:00.04 for the FLOTTER CNF translation.
% 0.19/0.49 0:00:00.01 for inferences.
% 0.19/0.49 0:00:00.00 for the backtracking.
% 0.19/0.49 0:00:00.03 for the reduction.
% 0.19/0.49
% 0.19/0.49
% 0.19/0.49 Here is a proof with depth 26, length 175 :
% 0.19/0.49 % SZS output start Refutation
% See solution above
% 0.19/0.49 Formulae used in the proof : ax50 ax41 ax60 ax66 ax67 ax68 ax69 ax70 ax72 ax73 ax75 ax44 ax45 ax46 ax47 ax48 ax49 ax54 ax71 ax74 ax76 ax77 ax78 ax79 ax80 ax81 ax82 ax1 ax2 ax3 ax4 ax19 ax26 ax55 ax56 ax9 ax12 alicereadsecret ax42 ax43 ax51 ax52 ax53 ax6 ax23 ax38 ax17 ax18 ax21 ax36 ax5 ax34 ax35 ax8 ax31 ax33 ax20 ax32 ax30 ax11 ax29 ax28 ax10 ax7 ax39 ax13 ax25 ax27
% 0.19/0.49
%------------------------------------------------------------------------------