%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n009.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 20:31:50 EDT 2022
% Result : Theorem 0.18s 0.45s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 21
% Syntax : Number of formulae : 124 ( 65 unt; 0 def)
% Number of atoms : 258 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 250 ( 116 ~; 113 |; 0 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 160 ( 26 sgn 93 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax8,axiom,
! [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) ) ) ).
fof(ax9,axiom,
! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil) ).
fof(ax11,axiom,
! [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) ) ) ) ).
fof(ax12,axiom,
! [F,L] : admin_file_has_level_h(admin,F,L,nil) ).
fof(ax14,axiom,
! [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) ) ) ) ).
fof(ax15,axiom,
! [F,U] : admin_file_has_citizenship_h(admin,F,U,nil) ).
fof(ax22,axiom,
! [K] : admin_indi_has_citizenship(admin,K,anycountry) ).
fof(ax24,axiom,
! [K] : admin_indi_has_level(admin,K,unclassified) ).
fof(ax26,axiom,
! [K] : admin_indi_has_compartments(admin,K,nil) ).
fof(ax34,axiom,
! [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) ) ) ).
fof(ax35,axiom,
! [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) ) ) ).
fof(ax36,axiom,
! [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) ) ) ).
fof(ax37,axiom,
! [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) ) ) ).
fof(ax39,axiom,
! [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) ) ) ) ) ) ).
fof(ax61,hypothesis,
state_file_is_not_working_paper(not_secretfile) ).
fof(ax62,hypothesis,
system_file_needs_compartments(system,not_secretfile,nil) ).
fof(ax63,hypothesis,
system_file_needs_level(system,not_secretfile,unclassified) ).
fof(ax64,hypothesis,
system_file_needs_citizenship(system,not_secretfile,anycountry) ).
fof(ax65,hypothesis,
state_file_has_owner(not_secretfile,owner_not_secretfile) ).
fof(ax85,hypothesis,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) ).
fof(babureadnotsecret,conjecture,
admin_indi_may_file(admin,babu,not_secretfile,read) ).
fof(subgoal_0,plain,
admin_indi_may_file(admin,babu,not_secretfile,read),
inference(strip,[],[babureadnotsecret]) ).
fof(negate_0_0,plain,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),
inference(canonicalize,[],[ax85]) ).
fof(normalize_0_1,plain,
! [F,K,OWR] :
( ~ owner_indi_has_need_to_know(OWR,K,F)
| ~ state_file_has_owner(F,OWR)
| admin_indi_has_need_to_know_for_file(admin,K,F) ),
inference(canonicalize,[],[ax36]) ).
fof(normalize_0_2,plain,
! [F,K,OWR] :
( ~ owner_indi_has_need_to_know(OWR,K,F)
| ~ state_file_has_owner(F,OWR)
| admin_indi_has_need_to_know_for_file(admin,K,F) ),
inference(specialize,[],[normalize_0_1]) ).
fof(normalize_0_3,plain,
state_file_has_owner(not_secretfile,owner_not_secretfile),
inference(canonicalize,[],[ax65]) ).
fof(normalize_0_4,plain,
! [F,K] :
( ~ admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_need_to_know_for_file(admin,K,F)
| ~ state_file_is_not_working_paper(F)
| admin_indi_may_file(admin,K,F,read) ),
inference(canonicalize,[],[ax39]) ).
fof(normalize_0_5,plain,
! [F,K] :
( ~ admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_need_to_know_for_file(admin,K,F)
| ~ state_file_is_not_working_paper(F)
| admin_indi_may_file(admin,K,F,read) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [K] : admin_indi_has_citizenship(admin,K,anycountry),
inference(canonicalize,[],[ax22]) ).
fof(normalize_0_7,plain,
! [K] : admin_indi_has_citizenship(admin,K,anycountry),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [F,K,L] :
( ~ admin_file_has_citizenship(admin,F,L)
| ~ admin_indi_has_citizenship(admin,K,L)
| admin_indi_has_citizenship_for_file(admin,K,F) ),
inference(canonicalize,[],[ax37]) ).
fof(normalize_0_9,plain,
! [F,K,L] :
( ~ admin_file_has_citizenship(admin,F,L)
| ~ admin_indi_has_citizenship(admin,K,L)
| admin_indi_has_citizenship_for_file(admin,K,F) ),
inference(specialize,[],[normalize_0_8]) ).
fof(normalize_0_10,plain,
system_file_needs_citizenship(system,not_secretfile,anycountry),
inference(canonicalize,[],[ax64]) ).
fof(normalize_0_11,plain,
! [F,U] : admin_file_has_citizenship_h(admin,F,U,nil),
inference(canonicalize,[],[ax15]) ).
fof(normalize_0_12,plain,
! [F,U] : admin_file_has_citizenship_h(admin,F,U,nil),
inference(specialize,[],[normalize_0_11]) ).
fof(normalize_0_13,plain,
! [CL,F,U] :
( ~ admin_file_has_citizenship_h(admin,F,U,CL)
| ~ admin_file_has_compartments(admin,F,CL)
| ~ system_file_needs_citizenship(system,F,U)
| admin_file_has_citizenship(admin,F,U) ),
inference(canonicalize,[],[ax14]) ).
fof(normalize_0_14,plain,
! [CL,F,U] :
( ~ admin_file_has_citizenship_h(admin,F,U,CL)
| ~ admin_file_has_compartments(admin,F,CL)
| ~ system_file_needs_citizenship(system,F,U)
| admin_file_has_citizenship(admin,F,U) ),
inference(specialize,[],[normalize_0_13]) ).
fof(normalize_0_15,plain,
system_file_needs_compartments(system,not_secretfile,nil),
inference(canonicalize,[],[ax62]) ).
fof(normalize_0_16,plain,
! [CL,F] : admin_file_has_compartments_h(admin,F,CL,nil),
inference(canonicalize,[],[ax9]) ).
fof(normalize_0_17,plain,
! [CL,F] : admin_file_has_compartments_h(admin,F,CL,nil),
inference(specialize,[],[normalize_0_16]) ).
fof(normalize_0_18,plain,
! [CL,F] :
( ~ admin_file_has_compartments_h(admin,F,CL,CL)
| ~ system_file_needs_compartments(system,F,CL)
| admin_file_has_compartments(admin,F,CL) ),
inference(canonicalize,[],[ax8]) ).
fof(normalize_0_19,plain,
! [CL,F] :
( ~ admin_file_has_compartments_h(admin,F,CL,CL)
| ~ system_file_needs_compartments(system,F,CL)
| admin_file_has_compartments(admin,F,CL) ),
inference(specialize,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
! [K] : admin_indi_has_compartments(admin,K,nil),
inference(canonicalize,[],[ax26]) ).
fof(normalize_0_21,plain,
! [K] : admin_indi_has_compartments(admin,K,nil),
inference(specialize,[],[normalize_0_20]) ).
fof(normalize_0_22,plain,
! [CL,F,K] :
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_indi_has_compartments(admin,K,CL)
| admin_indi_has_compartments_for_file(admin,K,F) ),
inference(canonicalize,[],[ax34]) ).
fof(normalize_0_23,plain,
! [CL,F,K] :
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_indi_has_compartments(admin,K,CL)
| admin_indi_has_compartments_for_file(admin,K,F) ),
inference(specialize,[],[normalize_0_22]) ).
fof(normalize_0_24,plain,
! [K] : admin_indi_has_level(admin,K,unclassified),
inference(canonicalize,[],[ax24]) ).
fof(normalize_0_25,plain,
! [K] : admin_indi_has_level(admin,K,unclassified),
inference(specialize,[],[normalize_0_24]) ).
fof(normalize_0_26,plain,
! [F,K,L] :
( ~ admin_file_has_level(admin,F,L)
| ~ admin_indi_has_level(admin,K,L)
| admin_indi_has_level_for_file(admin,K,F) ),
inference(canonicalize,[],[ax35]) ).
fof(normalize_0_27,plain,
! [F,K,L] :
( ~ admin_file_has_level(admin,F,L)
| ~ admin_indi_has_level(admin,K,L)
| admin_indi_has_level_for_file(admin,K,F) ),
inference(specialize,[],[normalize_0_26]) ).
fof(normalize_0_28,plain,
system_file_needs_level(system,not_secretfile,unclassified),
inference(canonicalize,[],[ax63]) ).
fof(normalize_0_29,plain,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
inference(canonicalize,[],[ax12]) ).
fof(normalize_0_30,plain,
! [F,L] : admin_file_has_level_h(admin,F,L,nil),
inference(specialize,[],[normalize_0_29]) ).
fof(normalize_0_31,plain,
! [CL,F,L] :
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_file_has_level_h(admin,F,L,CL)
| ~ system_file_needs_level(system,F,L)
| admin_file_has_level(admin,F,L) ),
inference(canonicalize,[],[ax11]) ).
fof(normalize_0_32,plain,
! [CL,F,L] :
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_file_has_level_h(admin,F,L,CL)
| ~ system_file_needs_level(system,F,L)
| admin_file_has_level(admin,F,L) ),
inference(specialize,[],[normalize_0_31]) ).
fof(normalize_0_33,plain,
state_file_is_not_working_paper(not_secretfile),
inference(canonicalize,[],[ax61]) ).
fof(normalize_0_34,plain,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
inference(canonicalize,[],[negate_0_0]) ).
cnf(refute_0_0,plain,
owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
( ~ owner_indi_has_need_to_know(OWR,K,F)
| ~ state_file_has_owner(F,OWR)
| admin_indi_has_need_to_know_for_file(admin,K,F) ),
inference(canonicalize,[],[normalize_0_2]) ).
cnf(refute_0_2,plain,
( ~ owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile)
| ~ state_file_has_owner(not_secretfile,owner_not_secretfile)
| admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile) ),
inference(subst,[],[refute_0_1:[bind(F,$fot(not_secretfile)),bind(K,$fot(babu)),bind(OWR,$fot(owner_not_secretfile))]]) ).
cnf(refute_0_3,plain,
( ~ state_file_has_owner(not_secretfile,owner_not_secretfile)
| admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile) ),
inference(resolve,[$cnf( owner_indi_has_need_to_know(owner_not_secretfile,babu,not_secretfile) )],[refute_0_0,refute_0_2]) ).
cnf(refute_0_4,plain,
state_file_has_owner(not_secretfile,owner_not_secretfile),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_5,plain,
admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile),
inference(resolve,[$cnf( state_file_has_owner(not_secretfile,owner_not_secretfile) )],[refute_0_4,refute_0_3]) ).
cnf(refute_0_6,plain,
( ~ admin_indi_has_citizenship_for_file(admin,K,F)
| ~ admin_indi_has_compartments_for_file(admin,K,F)
| ~ admin_indi_has_level_for_file(admin,K,F)
| ~ admin_indi_has_need_to_know_for_file(admin,K,F)
| ~ state_file_is_not_working_paper(F)
| admin_indi_may_file(admin,K,F,read) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_7,plain,
( ~ admin_indi_has_citizenship_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_compartments_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_level_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile)
| ~ state_file_is_not_working_paper(not_secretfile)
| admin_indi_may_file(admin,babu,not_secretfile,read) ),
inference(subst,[],[refute_0_6:[bind(F,$fot(not_secretfile)),bind(K,$fot(babu))]]) ).
cnf(refute_0_8,plain,
( ~ admin_indi_has_citizenship_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_compartments_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_level_for_file(admin,babu,not_secretfile)
| ~ state_file_is_not_working_paper(not_secretfile)
| admin_indi_may_file(admin,babu,not_secretfile,read) ),
inference(resolve,[$cnf( admin_indi_has_need_to_know_for_file(admin,babu,not_secretfile) )],[refute_0_5,refute_0_7]) ).
cnf(refute_0_9,plain,
admin_indi_has_citizenship(admin,K,anycountry),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_10,plain,
admin_indi_has_citizenship(admin,X_36,anycountry),
inference(subst,[],[refute_0_9:[bind(K,$fot(X_36))]]) ).
cnf(refute_0_11,plain,
( ~ admin_file_has_citizenship(admin,F,L)
| ~ admin_indi_has_citizenship(admin,K,L)
| admin_indi_has_citizenship_for_file(admin,K,F) ),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_12,plain,
( ~ admin_file_has_citizenship(admin,X_35,anycountry)
| ~ admin_indi_has_citizenship(admin,X_36,anycountry)
| admin_indi_has_citizenship_for_file(admin,X_36,X_35) ),
inference(subst,[],[refute_0_11:[bind(F,$fot(X_35)),bind(K,$fot(X_36)),bind(L,$fot(anycountry))]]) ).
cnf(refute_0_13,plain,
( ~ admin_file_has_citizenship(admin,X_35,anycountry)
| admin_indi_has_citizenship_for_file(admin,X_36,X_35) ),
inference(resolve,[$cnf( admin_indi_has_citizenship(admin,X_36,anycountry) )],[refute_0_10,refute_0_12]) ).
cnf(refute_0_14,plain,
( ~ admin_file_has_citizenship(admin,not_secretfile,anycountry)
| admin_indi_has_citizenship_for_file(admin,X_36,not_secretfile) ),
inference(subst,[],[refute_0_13:[bind(X_35,$fot(not_secretfile))]]) ).
cnf(refute_0_15,plain,
system_file_needs_citizenship(system,not_secretfile,anycountry),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_16,plain,
admin_file_has_citizenship_h(admin,F,U,nil),
inference(canonicalize,[],[normalize_0_12]) ).
cnf(refute_0_17,plain,
admin_file_has_citizenship_h(admin,X_98,X_99,nil),
inference(subst,[],[refute_0_16:[bind(F,$fot(X_98)),bind(U,$fot(X_99))]]) ).
cnf(refute_0_18,plain,
( ~ admin_file_has_citizenship_h(admin,F,U,CL)
| ~ admin_file_has_compartments(admin,F,CL)
| ~ system_file_needs_citizenship(system,F,U)
| admin_file_has_citizenship(admin,F,U) ),
inference(canonicalize,[],[normalize_0_14]) ).
cnf(refute_0_19,plain,
( ~ admin_file_has_citizenship_h(admin,X_98,X_99,nil)
| ~ admin_file_has_compartments(admin,X_98,nil)
| ~ system_file_needs_citizenship(system,X_98,X_99)
| admin_file_has_citizenship(admin,X_98,X_99) ),
inference(subst,[],[refute_0_18:[bind(CL,$fot(nil)),bind(F,$fot(X_98)),bind(U,$fot(X_99))]]) ).
cnf(refute_0_20,plain,
( ~ admin_file_has_compartments(admin,X_98,nil)
| ~ system_file_needs_citizenship(system,X_98,X_99)
| admin_file_has_citizenship(admin,X_98,X_99) ),
inference(resolve,[$cnf( admin_file_has_citizenship_h(admin,X_98,X_99,nil) )],[refute_0_17,refute_0_19]) ).
cnf(refute_0_21,plain,
( ~ admin_file_has_compartments(admin,not_secretfile,nil)
| ~ system_file_needs_citizenship(system,not_secretfile,anycountry)
| admin_file_has_citizenship(admin,not_secretfile,anycountry) ),
inference(subst,[],[refute_0_20:[bind(X_98,$fot(not_secretfile)),bind(X_99,$fot(anycountry))]]) ).
cnf(refute_0_22,plain,
( ~ admin_file_has_compartments(admin,not_secretfile,nil)
| admin_file_has_citizenship(admin,not_secretfile,anycountry) ),
inference(resolve,[$cnf( system_file_needs_citizenship(system,not_secretfile,anycountry) )],[refute_0_15,refute_0_21]) ).
cnf(refute_0_23,plain,
system_file_needs_compartments(system,not_secretfile,nil),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_24,plain,
admin_file_has_compartments_h(admin,F,CL,nil),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_25,plain,
admin_file_has_compartments_h(admin,X_33,nil,nil),
inference(subst,[],[refute_0_24:[bind(CL,$fot(nil)),bind(F,$fot(X_33))]]) ).
cnf(refute_0_26,plain,
( ~ admin_file_has_compartments_h(admin,F,CL,CL)
| ~ system_file_needs_compartments(system,F,CL)
| admin_file_has_compartments(admin,F,CL) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_27,plain,
( ~ admin_file_has_compartments_h(admin,X_33,nil,nil)
| ~ system_file_needs_compartments(system,X_33,nil)
| admin_file_has_compartments(admin,X_33,nil) ),
inference(subst,[],[refute_0_26:[bind(CL,$fot(nil)),bind(F,$fot(X_33))]]) ).
cnf(refute_0_28,plain,
( ~ system_file_needs_compartments(system,X_33,nil)
| admin_file_has_compartments(admin,X_33,nil) ),
inference(resolve,[$cnf( admin_file_has_compartments_h(admin,X_33,nil,nil) )],[refute_0_25,refute_0_27]) ).
cnf(refute_0_29,plain,
( ~ system_file_needs_compartments(system,not_secretfile,nil)
| admin_file_has_compartments(admin,not_secretfile,nil) ),
inference(subst,[],[refute_0_28:[bind(X_33,$fot(not_secretfile))]]) ).
cnf(refute_0_30,plain,
admin_file_has_compartments(admin,not_secretfile,nil),
inference(resolve,[$cnf( system_file_needs_compartments(system,not_secretfile,nil) )],[refute_0_23,refute_0_29]) ).
cnf(refute_0_31,plain,
admin_file_has_citizenship(admin,not_secretfile,anycountry),
inference(resolve,[$cnf( admin_file_has_compartments(admin,not_secretfile,nil) )],[refute_0_30,refute_0_22]) ).
cnf(refute_0_32,plain,
admin_indi_has_citizenship_for_file(admin,X_36,not_secretfile),
inference(resolve,[$cnf( admin_file_has_citizenship(admin,not_secretfile,anycountry) )],[refute_0_31,refute_0_14]) ).
cnf(refute_0_33,plain,
admin_indi_has_citizenship_for_file(admin,babu,not_secretfile),
inference(subst,[],[refute_0_32:[bind(X_36,$fot(babu))]]) ).
cnf(refute_0_34,plain,
( ~ admin_indi_has_compartments_for_file(admin,babu,not_secretfile)
| ~ admin_indi_has_level_for_file(admin,babu,not_secretfile)
| ~ state_file_is_not_working_paper(not_secretfile)
| admin_indi_may_file(admin,babu,not_secretfile,read) ),
inference(resolve,[$cnf( admin_indi_has_citizenship_for_file(admin,babu,not_secretfile) )],[refute_0_33,refute_0_8]) ).
cnf(refute_0_35,plain,
admin_indi_has_compartments(admin,K,nil),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_36,plain,
admin_indi_has_compartments(admin,X_46,nil),
inference(subst,[],[refute_0_35:[bind(K,$fot(X_46))]]) ).
cnf(refute_0_37,plain,
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_indi_has_compartments(admin,K,CL)
| admin_indi_has_compartments_for_file(admin,K,F) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_38,plain,
( ~ admin_file_has_compartments(admin,X_45,nil)
| ~ admin_indi_has_compartments(admin,X_46,nil)
| admin_indi_has_compartments_for_file(admin,X_46,X_45) ),
inference(subst,[],[refute_0_37:[bind(CL,$fot(nil)),bind(F,$fot(X_45)),bind(K,$fot(X_46))]]) ).
cnf(refute_0_39,plain,
( ~ admin_file_has_compartments(admin,X_45,nil)
| admin_indi_has_compartments_for_file(admin,X_46,X_45) ),
inference(resolve,[$cnf( admin_indi_has_compartments(admin,X_46,nil) )],[refute_0_36,refute_0_38]) ).
cnf(refute_0_40,plain,
( ~ admin_file_has_compartments(admin,not_secretfile,nil)
| admin_indi_has_compartments_for_file(admin,X_48,not_secretfile) ),
inference(subst,[],[refute_0_39:[bind(X_45,$fot(not_secretfile)),bind(X_46,$fot(X_48))]]) ).
cnf(refute_0_41,plain,
admin_indi_has_compartments_for_file(admin,X_48,not_secretfile),
inference(resolve,[$cnf( admin_file_has_compartments(admin,not_secretfile,nil) )],[refute_0_30,refute_0_40]) ).
cnf(refute_0_42,plain,
admin_indi_has_compartments_for_file(admin,babu,not_secretfile),
inference(subst,[],[refute_0_41:[bind(X_48,$fot(babu))]]) ).
cnf(refute_0_43,plain,
( ~ admin_indi_has_level_for_file(admin,babu,not_secretfile)
| ~ state_file_is_not_working_paper(not_secretfile)
| admin_indi_may_file(admin,babu,not_secretfile,read) ),
inference(resolve,[$cnf( admin_indi_has_compartments_for_file(admin,babu,not_secretfile) )],[refute_0_42,refute_0_34]) ).
cnf(refute_0_44,plain,
admin_indi_has_level(admin,K,unclassified),
inference(canonicalize,[],[normalize_0_25]) ).
cnf(refute_0_45,plain,
admin_indi_has_level(admin,X_51,unclassified),
inference(subst,[],[refute_0_44:[bind(K,$fot(X_51))]]) ).
cnf(refute_0_46,plain,
( ~ admin_file_has_level(admin,F,L)
| ~ admin_indi_has_level(admin,K,L)
| admin_indi_has_level_for_file(admin,K,F) ),
inference(canonicalize,[],[normalize_0_27]) ).
cnf(refute_0_47,plain,
( ~ admin_file_has_level(admin,X_50,unclassified)
| ~ admin_indi_has_level(admin,X_51,unclassified)
| admin_indi_has_level_for_file(admin,X_51,X_50) ),
inference(subst,[],[refute_0_46:[bind(F,$fot(X_50)),bind(K,$fot(X_51)),bind(L,$fot(unclassified))]]) ).
cnf(refute_0_48,plain,
( ~ admin_file_has_level(admin,X_50,unclassified)
| admin_indi_has_level_for_file(admin,X_51,X_50) ),
inference(resolve,[$cnf( admin_indi_has_level(admin,X_51,unclassified) )],[refute_0_45,refute_0_47]) ).
cnf(refute_0_49,plain,
( ~ admin_file_has_level(admin,not_secretfile,unclassified)
| admin_indi_has_level_for_file(admin,X_51,not_secretfile) ),
inference(subst,[],[refute_0_48:[bind(X_50,$fot(not_secretfile))]]) ).
cnf(refute_0_50,plain,
system_file_needs_level(system,not_secretfile,unclassified),
inference(canonicalize,[],[normalize_0_28]) ).
cnf(refute_0_51,plain,
admin_file_has_level_h(admin,F,L,nil),
inference(canonicalize,[],[normalize_0_30]) ).
cnf(refute_0_52,plain,
admin_file_has_level_h(admin,X_92,X_93,nil),
inference(subst,[],[refute_0_51:[bind(F,$fot(X_92)),bind(L,$fot(X_93))]]) ).
cnf(refute_0_53,plain,
( ~ admin_file_has_compartments(admin,F,CL)
| ~ admin_file_has_level_h(admin,F,L,CL)
| ~ system_file_needs_level(system,F,L)
| admin_file_has_level(admin,F,L) ),
inference(canonicalize,[],[normalize_0_32]) ).
cnf(refute_0_54,plain,
( ~ admin_file_has_compartments(admin,X_92,nil)
| ~ admin_file_has_level_h(admin,X_92,X_93,nil)
| ~ system_file_needs_level(system,X_92,X_93)
| admin_file_has_level(admin,X_92,X_93) ),
inference(subst,[],[refute_0_53:[bind(CL,$fot(nil)),bind(F,$fot(X_92)),bind(L,$fot(X_93))]]) ).
cnf(refute_0_55,plain,
( ~ admin_file_has_compartments(admin,X_92,nil)
| ~ system_file_needs_level(system,X_92,X_93)
| admin_file_has_level(admin,X_92,X_93) ),
inference(resolve,[$cnf( admin_file_has_level_h(admin,X_92,X_93,nil) )],[refute_0_52,refute_0_54]) ).
cnf(refute_0_56,plain,
( ~ admin_file_has_compartments(admin,not_secretfile,nil)
| ~ system_file_needs_level(system,not_secretfile,unclassified)
| admin_file_has_level(admin,not_secretfile,unclassified) ),
inference(subst,[],[refute_0_55:[bind(X_92,$fot(not_secretfile)),bind(X_93,$fot(unclassified))]]) ).
cnf(refute_0_57,plain,
( ~ admin_file_has_compartments(admin,not_secretfile,nil)
| admin_file_has_level(admin,not_secretfile,unclassified) ),
inference(resolve,[$cnf( system_file_needs_level(system,not_secretfile,unclassified) )],[refute_0_50,refute_0_56]) ).
cnf(refute_0_58,plain,
admin_file_has_level(admin,not_secretfile,unclassified),
inference(resolve,[$cnf( admin_file_has_compartments(admin,not_secretfile,nil) )],[refute_0_30,refute_0_57]) ).
cnf(refute_0_59,plain,
admin_indi_has_level_for_file(admin,X_51,not_secretfile),
inference(resolve,[$cnf( admin_file_has_level(admin,not_secretfile,unclassified) )],[refute_0_58,refute_0_49]) ).
cnf(refute_0_60,plain,
admin_indi_has_level_for_file(admin,babu,not_secretfile),
inference(subst,[],[refute_0_59:[bind(X_51,$fot(babu))]]) ).
cnf(refute_0_61,plain,
( ~ state_file_is_not_working_paper(not_secretfile)
| admin_indi_may_file(admin,babu,not_secretfile,read) ),
inference(resolve,[$cnf( admin_indi_has_level_for_file(admin,babu,not_secretfile) )],[refute_0_60,refute_0_43]) ).
cnf(refute_0_62,plain,
state_file_is_not_working_paper(not_secretfile),
inference(canonicalize,[],[normalize_0_33]) ).
cnf(refute_0_63,plain,
admin_indi_may_file(admin,babu,not_secretfile,read),
inference(resolve,[$cnf( state_file_is_not_working_paper(not_secretfile) )],[refute_0_62,refute_0_61]) ).
cnf(refute_0_64,plain,
~ admin_indi_may_file(admin,babu,not_secretfile,read),
inference(canonicalize,[],[normalize_0_34]) ).
cnf(refute_0_65,plain,
$false,
inference(resolve,[$cnf( admin_indi_may_file(admin,babu,not_secretfile,read) )],[refute_0_63,refute_0_64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWV438+1 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.13 % Command : metis --show proof --show saturation %s
% 0.12/0.33 % Computer : n009.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 : Wed Jun 15 14:05:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45
% 0.18/0.45 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.18/0.46
%------------------------------------------------------------------------------