%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n015.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:38:40 EDT 2022
% Result : Theorem 1.05s 1.29s
% Output : Refutation 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV437+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n015.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 : 600
% 0.13/0.34 % DateTime : Thu Jun 16 02:30:25 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.37 ----- Otter 3.2, August 2001 -----
% 0.19/0.37 The process was started by sandbox2 on n015.cluster.edu,
% 0.19/0.37 Thu Jun 16 02:30:26 2022
% 0.19/0.37 The command was "./sos". The process ID is 995.
% 0.19/0.37
% 0.19/0.37 set(prolog_style_variables).
% 0.19/0.37 set(auto).
% 0.19/0.37 dependent: set(auto1).
% 0.19/0.37 dependent: set(process_input).
% 0.19/0.37 dependent: clear(print_kept).
% 0.19/0.37 dependent: clear(print_new_demod).
% 0.19/0.37 dependent: clear(print_back_demod).
% 0.19/0.37 dependent: clear(print_back_sub).
% 0.19/0.37 dependent: set(control_memory).
% 0.19/0.37 dependent: assign(max_mem, 12000).
% 0.19/0.37 dependent: assign(pick_given_ratio, 4).
% 0.19/0.37 dependent: assign(stats_level, 1).
% 0.19/0.37 dependent: assign(pick_semantic_ratio, 3).
% 0.19/0.37 dependent: assign(sos_limit, 5000).
% 0.19/0.37 dependent: assign(max_weight, 60).
% 0.19/0.37 clear(print_given).
% 0.19/0.37
% 0.19/0.37 formula_list(usable).
% 0.19/0.37
% 0.19/0.37 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=11.
% 0.19/0.37
% 0.19/0.37 This is a Horn set without equality. The strategy will
% 0.19/0.37 be hyperresolution, with satellites in sos and nuclei
% 0.19/0.37 in usable.
% 0.19/0.37
% 0.19/0.37 dependent: set(hyper_res).
% 0.19/0.37 dependent: clear(order_hyper).
% 0.19/0.37
% 0.19/0.37 ------------> process usable:
% 0.19/0.37
% 0.19/0.37 ------------> process sos:
% 0.19/0.37
% 0.19/0.37 ======= end of input processing =======
% 1.05/1.28
% 1.05/1.28 Stopped by limit on insertions
% 1.05/1.28
% 1.05/1.28
% 1.05/1.28 Failed to model usable list: disabling FINDER
% 1.05/1.28
% 1.05/1.28
% 1.05/1.28
% 1.05/1.28 -------------- Softie stats --------------
% 1.05/1.28
% 1.05/1.28 UPDATE_STOP: 300
% 1.05/1.28 SFINDER_TIME_LIMIT: 2
% 1.05/1.28 SHORT_CLAUSE_CUTOFF: 4
% 1.05/1.28 number of clauses in intial UL: 30
% 1.05/1.28 number of clauses initially in problem: 88
% 1.05/1.28 percentage of clauses intially in UL: 34
% 1.05/1.28 percentage of distinct symbols occuring in initial UL: 71
% 1.05/1.28 percent of all initial clauses that are short: 98
% 1.05/1.28 absolute distinct symbol count: 89
% 1.05/1.28 distinct predicate count: 55
% 1.05/1.28 distinct function count: 1
% 1.05/1.28 distinct constant count: 33
% 1.05/1.28
% 1.05/1.28 ---------- no more Softie stats ----------
% 1.05/1.28
% 1.05/1.28
% 1.05/1.28
% 1.05/1.28 =========== start of search ===========
% 1.05/1.29
% 1.05/1.29 -------- PROOF --------
% 1.05/1.29 % SZS status Theorem
% 1.05/1.29 % SZS output start Refutation
% 1.05/1.29
% 1.05/1.29 ----> UNIT CONFLICT at 0.90 sec ----> 206 [binary,205.1,30.1] {-} $F.
% 1.05/1.29
% 1.05/1.29 Length of proof is 42. Level of proof is 10.
% 1.05/1.29
% 1.05/1.29 ---------------- PROOF ----------------
% 1.05/1.29 % SZS status Theorem
% 1.05/1.29 % SZS output start Refutation
% 1.05/1.29
% 1.05/1.29 1 [] {+} -loca_level_direct_below(A,B,C)| -loca_level_below(A,D,B)|loca_level_below(A,D,C).
% 1.05/1.29 2 [] {+} -system_compartment_has_sso(system,A,B)|admin_compartment_has_sso(admin,A,B).
% 1.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 10 [] {+} -system_indi_is_polygraph_admin(system,A)| -polygraph_admin_indi_has_polygraph(A,B)|admin_indi_has_polygraph(admin,B).
% 1.05/1.29 11 [] {+} -system_indi_is_credit_admin(system,A)| -credit_admin_indi_has_credit(A,B)|admin_indi_has_credit(admin,B).
% 1.05/1.29 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.05/1.29 13 [] {+} -system_indi_is_hr_admin(system,A)| -hr_admin_indi_has_employment(A,B)|admin_indi_has_employment(admin,B).
% 1.05/1.29 14 [] {+} -system_indi_has_citizenship(system,A,B)|admin_indi_has_citizenship(admin,A,B).
% 1.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 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.05/1.29 27 [] {+} -admin_indi_has_citizenship(admin,A,usa)|admin_indi_has_citizenship_for_file(admin,A,B).
% 1.05/1.29 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.05/1.29 30 [] {+} -admin_indi_may_file(admin,alice,secretfile,read).
% 1.05/1.29 32 [] {-} loca_level_direct_below(A,sbu,confidential).
% 1.05/1.29 33 [] {-} loca_level_direct_below(A,confidential,secret).
% 1.05/1.29 34 [] {-} loca_level_direct_below(A,secret,topsecret).
% 1.05/1.29 35 [] {-} loca_level_below(A,B,B).
% 1.05/1.29 36 [] {-} admin_file_has_compartments_h(admin,A,B,nil).
% 1.05/1.29 37 [] {-} admin_file_has_level_h(admin,A,B,nil).
% 1.05/1.29 39 [] {-} admin_indi_has_background(admin,A,unclassified).
% 1.05/1.29 42 [] {-} admin_indi_has_compartments(admin,A,nil).
% 1.05/1.29 43 [] {-} system_indi_is_oca(system,oca).
% 1.05/1.29 44 [] {-} oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes).
% 1.05/1.29 45 [] {-} oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no).
% 1.05/1.29 46 [] {-} system_compartment_has_sso(system,compartmentb,sso_compartmentb).
% 1.05/1.29 47 [] {-} oca_compartment_has_scg(oca,compartmentb,scg_compartmentb).
% 1.05/1.29 48 [] {-} sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb).
% 1.05/1.29 49 [] {-} system_compartment_has_sso(system,compartmenta,sso_compartmenta).
% 1.05/1.29 50 [] {-} oca_compartment_has_scg(oca,compartmenta,scg_compartmenta).
% 1.05/1.29 51 [] {-} sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta).
% 1.05/1.29 52 [] {-} state_file_is_not_working_paper(secretfile).
% 1.05/1.29 53 [] {-} system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 54 [] {-} sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 55 [] {-} sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 56 [] {-} system_file_needs_level(system,secretfile,secret).
% 1.05/1.29 57 [] {-} sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb).
% 1.05/1.29 58 [] {-} sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta).
% 1.05/1.29 62 [] {-} state_file_has_owner(secretfile,owner_secretfile).
% 1.05/1.29 68 [] {-} system_indi_is_polygraph_admin(system,polygraph_admin).
% 1.05/1.29 69 [] {-} system_indi_is_credit_admin(system,credit_admin).
% 1.05/1.29 70 [] {-} system_indi_is_background_admin(system,background_admin).
% 1.05/1.29 71 [] {-} system_indi_is_hr_admin(system,hr_admin).
% 1.05/1.29 72 [] {-} system_indi_is_level_admin(system,level_admin).
% 1.05/1.29 73 [] {-} system_indi_has_citizenship(system,alice,usa).
% 1.05/1.29 74 [] {-} polygraph_admin_indi_has_polygraph(polygraph_admin,alice).
% 1.05/1.29 75 [] {-} credit_admin_indi_has_credit(credit_admin,alice).
% 1.05/1.29 76 [] {-} background_admin_indi_has_background(background_admin,alice,topsecret).
% 1.05/1.29 77 [] {-} hr_admin_indi_has_employment(hr_admin,alice).
% 1.05/1.29 78 [] {-} system_indi_needs_level(system,alice,secret).
% 1.05/1.29 79 [] {-} level_admin_indi_has_level(level_admin,alice,topsecret).
% 1.05/1.29 80 [] {-} system_indi_needs_compartment(system,alice,compartmentb).
% 1.05/1.29 81 [] {-} system_indi_needs_compartment(system,alice,compartmenta).
% 1.05/1.29 82 [] {-} sso_indi_has_compartment(sso_compartmentb,alice,compartmentb).
% 1.05/1.29 83 [] {-} sso_indi_has_compartment(sso_compartmenta,alice,compartmenta).
% 1.05/1.29 84 [] {-} owner_indi_has_need_to_know(owner_secretfile,alice,secretfile).
% 1.05/1.29 89 [hyper,74,10,68] {-} admin_indi_has_polygraph(admin,alice).
% 1.05/1.29 90 [hyper,75,11,69] {-} admin_indi_has_credit(admin,alice).
% 1.05/1.29 91 [hyper,77,13,71] {-} admin_indi_has_employment(admin,alice).
% 1.05/1.29 92 [hyper,35,1,34] {-} loca_level_below(A,secret,topsecret).
% 1.05/1.29 93 [hyper,35,1,33] {-} loca_level_below(A,confidential,secret).
% 1.05/1.29 94 [hyper,35,1,32] {-} loca_level_below(A,sbu,confidential).
% 1.05/1.29 96 [hyper,46,2] {-} admin_compartment_has_sso(admin,compartmentb,sso_compartmentb).
% 1.05/1.29 97 [hyper,49,2] {-} admin_compartment_has_sso(admin,compartmenta,sso_compartmenta).
% 1.05/1.29 99 [hyper,73,14] {-} admin_indi_has_citizenship(admin,alice,usa).
% 1.05/1.29 100 [hyper,44,21,43,90] {-} admin_indi_has_credit_for_compartment(admin,alice,compartmentb).
% 1.05/1.29 101 [hyper,44,19,43,89] {-} admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb).
% 1.05/1.29 102 [hyper,76,12,70,35] {-} admin_indi_has_background(admin,alice,topsecret).
% 1.05/1.29 103 [hyper,45,22,43] {-} admin_indi_has_credit_for_compartment(admin,A,compartmenta).
% 1.05/1.29 104 [hyper,45,20,43] {-} admin_indi_has_polygraph_for_compartment(admin,A,compartmenta).
% 1.05/1.29 105 [hyper,45,17,43,39] {-} admin_indi_has_background_for_compartment(admin,A,compartmenta).
% 1.05/1.29 106 [hyper,84,25,62] {-} admin_indi_has_need_to_know_for_file(admin,alice,secretfile).
% 1.05/1.29 110 [hyper,92,12,70,76] {-} admin_indi_has_background(admin,alice,secret).
% 1.05/1.29 111 [hyper,93,1,34] {-} loca_level_below(A,confidential,topsecret).
% 1.05/1.29 112 [hyper,94,1,33] {-} loca_level_below(A,sbu,secret).
% 1.05/1.29 115 [hyper,96,3,43,47,48] {-} admin_compartment_has_scg(admin,compartmentb,scg_compartmentb).
% 1.05/1.29 116 [hyper,97,5,55,36] {-} admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil)).
% 1.05/1.29 117 [hyper,97,3,43,50,51] {-} admin_compartment_has_scg(admin,compartmenta,scg_compartmenta).
% 1.05/1.29 121 [hyper,99,27] {-} admin_indi_has_citizenship_for_file(admin,alice,A).
% 1.05/1.29 122 [hyper,102,17,43,44] {-} admin_indi_has_background_for_compartment(admin,alice,compartmentb).
% 1.05/1.29 123 [hyper,110,15,78,99,89,91,90,35,72,79,92] {-} admin_indi_has_level(admin,alice,secret).
% 1.05/1.29 124 [hyper,111,12,70,76] {-} admin_indi_has_background(admin,alice,confidential).
% 1.05/1.29 125 [hyper,112,1,34] {-} loca_level_below(A,sbu,topsecret).
% 1.05/1.29 130 [hyper,117,7,97,58,37] {-} admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil)).
% 1.05/1.29 135 [hyper,124,15,78,99,89,91,90,93,72,79,111] {-} admin_indi_has_level(admin,alice,confidential).
% 1.05/1.29 136 [hyper,125,12,70,76] {-} admin_indi_has_background(admin,alice,sbu).
% 1.05/1.29 139 [hyper,116,5,96,54] {-} admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 141 [hyper,135,18,43,44] {-} admin_indi_has_level_for_compartment(admin,alice,compartmentb).
% 1.05/1.29 142 [hyper,136,15,78,99,89,91,90,112,72,79,125] {-} admin_indi_has_level(admin,alice,sbu).
% 1.05/1.29 146 [hyper,142,18,43,45] {-} admin_indi_has_level_for_compartment(admin,alice,compartmenta).
% 1.05/1.29 147 [hyper,146,16,81,91,99,104,103,97,83,105,42] {-} admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)).
% 1.05/1.29 153 [hyper,147,16,80,91,99,101,100,96,82,122,141] {-} admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 157 [hyper,130,7,96,115,57] {-} admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 198 [hyper,139,4,53] {-} admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))).
% 1.05/1.29 199 [hyper,198,23,153] {-} admin_indi_has_compartments_for_file(admin,alice,secretfile).
% 1.05/1.29 201 [hyper,198,6,56,157] {-} admin_file_has_level(admin,secretfile,secret).
% 1.05/1.29 202 [hyper,201,24,123] {-} admin_indi_has_level_for_file(admin,alice,secretfile).
% 1.05/1.29 205 [hyper,202,28,52,121,106,199] {-} admin_indi_may_file(admin,alice,secretfile,read).
% 1.05/1.29 206 [binary,205.1,30.1] {-} $F.
% 1.05/1.29
% 1.05/1.29 % SZS output end Refutation
% 1.05/1.29 ------------ end of proof -------------
% 1.05/1.29
% 1.05/1.29
% 1.05/1.29 Search stopped by max_proofs option.
% 1.05/1.29
% 1.05/1.29
% 1.05/1.29 Search stopped by max_proofs option.
% 1.05/1.29
% 1.05/1.29 ============ end of search ============
% 1.05/1.29
% 1.05/1.29 That finishes the proof of the theorem.
% 1.05/1.29
% 1.05/1.29 Process 995 finished Thu Jun 16 02:30:26 2022
%------------------------------------------------------------------------------