%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : SWV437+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n022.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 : Thu Aug 31 22:27:32 EDT 2023
% Result : Theorem 1.56s 0.60s
% Output : CNFRefutation 1.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV437+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : gkc %s
% 0.13/0.34 % Computer : n022.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 : Tue Aug 29 09:55:23 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.20/0.40
% 0.20/0.40 input clause set summed statistics:
% 0.20/0.40 ----------------------------------
% 0.20/0.40 in_clause_count: 88
% 0.20/0.40 in_rule_clause_count: 45
% 0.20/0.40 in_fact_clause_count: 43
% 0.20/0.40 in_answer_clause_count: 0
% 0.20/0.40 in_ground_clause_count: 47
% 0.20/0.40 in_unit_clause_count: 59
% 0.20/0.40 in_horn_clause_count: 88
% 0.20/0.40 in_pos_clause_count: 58
% 0.20/0.40 in_neg_clause_count: 1
% 0.20/0.40 in_poseq_clause_count: 0
% 0.20/0.40 in_negeq_clause_count: 0
% 0.20/0.40 in_unitposeq_clause_count: 0
% 0.20/0.40 in_chain_clause_count: 0
% 0.20/0.40 in_min_length: 1
% 0.20/0.40 in_max_length: 11
% 0.20/0.40 in_min_depth: 1
% 0.20/0.40 in_max_depth: 3
% 0.20/0.40 in_min_size: 2
% 0.20/0.40 in_max_size: 45
% 0.20/0.40 in_min_vars: 0
% 0.20/0.40 in_max_vars: 7
% 0.20/0.40 in_extaxiom_count: 41
% 0.20/0.40 in_axiom_count: 0
% 0.20/0.40 in_assumption_count: 46
% 0.20/0.40 in_goal_count: 1
% 0.20/0.40 in_neg_goal_count: 1
% 0.20/0.40 in_pos_goal_count: 0
% 0.20/0.40 in_posunit_goal_count: 0
% 0.20/0.40
% 0.20/0.40 auto guide:
% 0.20/0.40 -----------
% 0.20/0.40 {
% 0.20/0.40 "print":1,
% 0.20/0.40 "print_level": 15,
% 0.20/0.40 "max_size": 0,
% 0.20/0.40 "max_depth": 0,
% 0.20/0.40 "max_length": 0,
% 0.20/0.40 "max_dseconds": 0,
% 0.20/0.40 "equality":0,
% 0.20/0.40 "runs":[
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.20/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":20},
% 0.20/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "max_depth":5, "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "max_weight":40, "query_preference":0},
% 0.20/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.20/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":10},
% 0.20/0.40 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":20},
% 0.20/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "max_depth":5, "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "max_weight":40, "query_preference":0},
% 0.20/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.20/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":50},
% 0.20/0.40 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":20},
% 0.20/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "max_depth":5, "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "max_weight":40, "query_preference":0},
% 0.20/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.40
% 0.20/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":250},
% 0.20/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":250},
% 0.20/0.40 {"max_dseconds":250, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":250},
% 0.20/0.40 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":250},
% 0.20/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "weight_select_ratio":20},
% 0.20/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.40
% 0.20/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1250},
% 0.20/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":1250},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1250},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1250},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "weight_select_ratio":20},
% 0.20/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0}
% 0.20/0.40
% 0.20/0.40 ]}
% 0.20/0.40
% 0.20/0.40
% 0.20/0.40 **** run 1 fork 0 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 0.20/0.40
% 0.20/0.40 **** run 2 fork 1 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.20/0.40
% 0.20/0.40 **** run 3 fork 2 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.40
% 0.20/0.40 **** run 4 fork 3 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.40
% 0.20/0.40 **** run 5 fork 4 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.20/0.40
% 0.20/0.40 **** run 6 fork 5 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.40
% 0.20/0.40 **** run 7 fork 6 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 0.20/0.40
% 0.20/0.40 **** run 8 fork 7 starts with strategy
% 0.20/0.40 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.20/0.43
% 0.20/0.43 fork 1: search finished without proof.
% 0.20/0.46
% 0.20/0.46 **** run 10 fork 1 starts with strategy
% 0.20/0.46 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 0.20/0.52
% 0.20/0.52 fork 0: search finished without proof.
% 0.20/0.52
% 0.20/0.52 fork 2: search finished without proof.
% 0.20/0.52
% 0.20/0.52 fork 4: search finished without proof.
% 0.20/0.52
% 0.20/0.52 fork 6: search finished without proof.
% 0.20/0.52
% 0.20/0.52 fork 3: search finished without proof.
% 0.20/0.53
% 0.20/0.53
% 0.20/0.53 fork 5: search terminated without proof.
% 0.20/0.53
% 0.20/0.53
% 0.20/0.53 fork 7: search terminated without proof.
% 0.20/0.54
% 0.20/0.54 **** run 15 fork 6 starts with strategy
% 0.20/0.54 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 0.20/0.54
% 0.20/0.54 **** run 13 fork 4 starts with strategy
% 0.20/0.54 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 0.20/0.54
% 0.20/0.54 **** run 9 fork 0 starts with strategy
% 0.20/0.54 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 0.20/0.55
% 0.20/0.55 **** run 12 fork 3 starts with strategy
% 0.20/0.55 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 0.20/0.55
% 0.20/0.55 **** run 11 fork 2 starts with strategy
% 0.20/0.55 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 0.20/0.55
% 0.20/0.55 **** run 14 fork 5 starts with strategy
% 0.20/0.55
% 0.20/0.55 **** run 16 fork 7 starts with strategy
% 0.20/0.55 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 0.20/0.55 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 0.20/0.58
% 0.20/0.58 fork 3: search finished without proof.
% 0.20/0.59
% 0.20/0.59 **** run 20 fork 3 starts with strategy
% 0.20/0.59 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 1.56/0.60
% 1.56/0.60
% 1.56/0.60 result: proof found
% 1.56/0.60 for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.56/0.60 by run 9 fork 0 strategy {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 1.56/0.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.56/0.60
% 1.56/0.60 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.56/0.60 fof('$inc_ax27_$sk', plain, ((((((((((admin_indi_has_compartments(admin,X4,cons(X2,X3)) | ~admin_indi_has_compartments(admin,X4,X3)) | ~admin_indi_has_level_for_compartment(admin,X4,X2)) | ~admin_indi_has_background_for_compartment(admin,X4,X2)) | ~sso_indi_has_compartment(X1,X4,X2)) | ~admin_compartment_has_sso(admin,X2,X1)) | ~admin_indi_has_credit_for_compartment(admin,X4,X2)) | ~admin_indi_has_polygraph_for_compartment(admin,X4,X2)) | ~admin_indi_has_citizenship(admin,X4,usa)) | ~admin_indi_has_employment(admin,X4)) | ~system_indi_needs_compartment(system,X4,X2)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax27'])).
% 1.56/0.60 fof('$inc_ax27', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('ax71', hypothesis, system_indi_has_citizenship(system,alice,usa),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax23_$sk', plain, (admin_indi_has_citizenship(admin,X2,X1) | ~system_indi_has_citizenship(system,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax23'])).
% 1.56/0.60 fof('$inc_ax23', axiom, (! [K,U] : (system_indi_has_citizenship(system,K,U) => admin_indi_has_citizenship(admin,K,U))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax21_$sk', plain, ((admin_indi_has_employment(admin,X2) | ~hr_admin_indi_has_employment(X1,X2)) | ~system_indi_is_hr_admin(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax21'])).
% 1.56/0.60 fof('$inc_ax21', axiom, (! [K,HR] : (system_indi_is_hr_admin(system,HR) => (hr_admin_indi_has_employment(HR,K) => admin_indi_has_employment(admin,K)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax69', hypothesis, system_indi_is_hr_admin(system,hr_admin),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax75', hypothesis, hr_admin_indi_has_employment(hr_admin,alice),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax78', hypothesis, system_indi_needs_compartment(system,alice,compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax30_$sk', plain, (((admin_indi_has_polygraph_for_compartment(admin,X6,X5) | ~admin_indi_has_polygraph(admin,X6)) | ~oca_compartment_is_compartment(X1,X5,X2,X3,X4,yes)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax30'])).
% 1.56/0.60 fof('$inc_ax30', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('ax42', hypothesis, oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax41', hypothesis, system_indi_is_oca(system,oca),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax17_$sk', plain, ((admin_indi_has_polygraph(admin,X2) | ~polygraph_admin_indi_has_polygraph(X1,X2)) | ~system_indi_is_polygraph_admin(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax17'])).
% 1.56/0.60 fof('$inc_ax17', axiom, (! [K,PA] : (system_indi_is_polygraph_admin(system,PA) => (polygraph_admin_indi_has_polygraph(PA,K) => admin_indi_has_polygraph(admin,K)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax66', hypothesis, system_indi_is_polygraph_admin(system,polygraph_admin),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax72', hypothesis, polygraph_admin_indi_has_polygraph(polygraph_admin,alice),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax32_$sk', plain, (((admin_indi_has_credit_for_compartment(admin,X6,X5) | ~admin_indi_has_credit(admin,X6)) | ~oca_compartment_is_compartment(X1,X5,X2,X3,yes,X4)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax32'])).
% 1.56/0.60 fof('$inc_ax32', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax18_$sk', plain, ((admin_indi_has_credit(admin,X2) | ~credit_admin_indi_has_credit(X1,X2)) | ~system_indi_is_credit_admin(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax18'])).
% 1.56/0.60 fof('$inc_ax18', axiom, (! [K,CA] : (system_indi_is_credit_admin(system,CA) => (credit_admin_indi_has_credit(CA,K) => admin_indi_has_credit(admin,K)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax67', hypothesis, system_indi_is_credit_admin(system,credit_admin),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax73', hypothesis, credit_admin_indi_has_credit(credit_admin,alice),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax20_$sk', plain, (((admin_indi_has_background(admin,X4,X3) | ~loca_level_below(admin,X3,X2)) | ~background_admin_indi_has_background(X1,X4,X2)) | ~system_indi_is_background_admin(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax20'])).
% 1.56/0.60 fof('$inc_ax20', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax4_$sk', plain, loca_level_below(X2,X1,X1),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax4'])).
% 1.56/0.60 fof('$inc_ax4', axiom, (! [K,L] : loca_level_below(K,L,L)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax68', hypothesis, system_indi_is_background_admin(system,background_admin),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax74', hypothesis, background_admin_indi_has_background(background_admin,alice,topsecret),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax28_$sk', plain, (((admin_indi_has_background_for_compartment(admin,X7,X6) | ~admin_indi_has_background(admin,X7,X5)) | ~oca_compartment_is_compartment(X1,X6,X2,X5,X3,X4)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax28'])).
% 1.56/0.60 fof('$inc_ax28', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax25_$sk', plain, ((((((((((admin_indi_has_level(admin,X5,X4) | ~admin_indi_has_background(admin,X5,X4)) | ~loca_level_below(admin,X4,X3)) | ~level_admin_indi_has_level(X2,X5,X3)) | ~system_indi_is_level_admin(system,X2)) | ~loca_level_below(admin,X4,X1)) | ~admin_indi_has_credit(admin,X5)) | ~admin_indi_has_employment(admin,X5)) | ~admin_indi_has_polygraph(admin,X5)) | ~admin_indi_has_citizenship(admin,X5,usa)) | ~system_indi_needs_level(system,X5,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax25'])).
% 1.56/0.60 fof('$inc_ax25', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('ax76', hypothesis, system_indi_needs_level(system,alice,secret),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax5_$sk', plain, ((loca_level_below(X4,X3,X2) | ~loca_level_below(X4,X3,X1)) | ~loca_level_direct_below(X4,X1,X2)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax5'])).
% 1.56/0.60 fof('$inc_ax5', axiom, (! [K,L,L1,L11] : (loca_level_direct_below(K,L1,L11) => (loca_level_below(K,L,L1) => loca_level_below(K,L,L11)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax2_$sk', plain, loca_level_direct_below(X1,confidential,secret),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax2'])).
% 1.56/0.60 fof('$inc_ax2', axiom, (! [K] : loca_level_direct_below(K,confidential,secret)),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax3_$sk', plain, loca_level_direct_below(X1,secret,topsecret),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax3'])).
% 1.56/0.60 fof('$inc_ax3', axiom, (! [K] : loca_level_direct_below(K,secret,topsecret)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax77', hypothesis, level_admin_indi_has_level(level_admin,alice,topsecret),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax70', hypothesis, system_indi_is_level_admin(system,level_admin),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax29_$sk', plain, (((admin_indi_has_level_for_compartment(admin,X7,X6) | ~admin_indi_has_level(admin,X7,X5)) | ~oca_compartment_is_compartment(X1,X6,X5,X2,X3,X4)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax29'])).
% 1.56/0.60 fof('$inc_ax29', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('ax79', hypothesis, system_indi_needs_compartment(system,alice,compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax1_$sk', plain, loca_level_direct_below(X1,sbu,confidential),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax1'])).
% 1.56/0.60 fof('$inc_ax1', axiom, (! [K] : loca_level_direct_below(K,sbu,confidential)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax43', hypothesis, oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax31_$sk', plain, ((admin_indi_has_polygraph_for_compartment(admin,X6,X5) | ~oca_compartment_is_compartment(X1,X5,X2,X3,X4,no)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax31'])).
% 1.56/0.60 fof('$inc_ax31', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax33_$sk', plain, ((admin_indi_has_credit_for_compartment(admin,X6,X5) | ~oca_compartment_is_compartment(X1,X5,X2,X3,no,X4)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax33'])).
% 1.56/0.60 fof('$inc_ax33', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax19_$sk', plain, admin_indi_has_background(admin,X1,unclassified),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax19'])).
% 1.56/0.60 fof('$inc_ax19', axiom, (! [K] : admin_indi_has_background(admin,K,unclassified)),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax26_$sk', plain, admin_indi_has_compartments(admin,X1,nil),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax26'])).
% 1.56/0.60 fof('$inc_ax26', axiom, (! [K] : admin_indi_has_compartments(admin,K,nil)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax47', hypothesis, system_compartment_has_sso(system,compartmenta,sso_compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax6_$sk', plain, (admin_compartment_has_sso(admin,X2,X1) | ~system_compartment_has_sso(system,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax6'])).
% 1.56/0.60 fof('$inc_ax6', axiom, (! [C,SSO] : (system_compartment_has_sso(system,C,SSO) => admin_compartment_has_sso(admin,C,SSO))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax81', hypothesis, sso_indi_has_compartment(sso_compartmenta,alice,compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax44', hypothesis, system_compartment_has_sso(system,compartmentb,sso_compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax80', hypothesis, sso_indi_has_compartment(sso_compartmentb,alice,compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax34_$sk', plain, ((admin_indi_has_compartments_for_file(admin,X3,X2) | ~admin_indi_has_compartments(admin,X3,X1)) | ~admin_file_has_compartments(admin,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax34'])).
% 1.56/0.60 fof('$inc_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)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax10_$sk', plain, (((admin_file_has_compartments_h(admin,X5,X4,cons(X2,X3)) | ~admin_file_has_compartments_h(admin,X5,X4,X3)) | ~sso_file_has_compartments(X1,X5,X4)) | ~admin_compartment_has_sso(admin,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax10'])).
% 1.56/0.60 fof('$inc_ax10', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax9_$sk', plain, admin_file_has_compartments_h(admin,X2,X1,nil),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax9'])).
% 1.56/0.60 fof('$inc_ax9', axiom, (! [F,CL] : admin_file_has_compartments_h(admin,F,CL,nil)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax53', hypothesis, sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax52', hypothesis, sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax8_$sk', plain, ((admin_file_has_compartments(admin,X2,X1) | ~admin_file_has_compartments_h(admin,X2,X1,X1)) | ~system_file_needs_compartments(system,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax8'])).
% 1.56/0.60 fof('$inc_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)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax51', hypothesis, system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax35_$sk', plain, ((admin_indi_has_level_for_file(admin,X3,X2) | ~admin_indi_has_level(admin,X3,X1)) | ~admin_file_has_level(admin,X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax35'])).
% 1.56/0.60 fof('$inc_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)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax7_$sk', plain, ((((admin_compartment_has_scg(admin,X4,X3) | ~sso_compartment_has_scg(X2,X4,X3)) | ~admin_compartment_has_sso(admin,X4,X2)) | ~oca_compartment_has_scg(X1,X4,X3)) | ~system_indi_is_oca(system,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax7'])).
% 1.56/0.60 fof('$inc_ax7', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('ax49', hypothesis, sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax48', hypothesis, oca_compartment_has_scg(oca,compartmenta,scg_compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax13_$sk', plain, ((((admin_file_has_level_h(admin,X6,X5,cons(X3,X4)) | ~admin_file_has_level_h(admin,X6,X5,X4)) | ~sso_file_has_level(X1,X6,X5,X2)) | ~admin_compartment_has_scg(admin,X3,X2)) | ~admin_compartment_has_sso(admin,X3,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax13'])).
% 1.56/0.60 fof('$inc_ax13', axiom, (! [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.56/0.60 input).
% 1.56/0.60 fof('$inc_ax12_$sk', plain, admin_file_has_level_h(admin,X2,X1,nil),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax12'])).
% 1.56/0.60 fof('$inc_ax12', axiom, (! [F,L] : admin_file_has_level_h(admin,F,L,nil)),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax56', hypothesis, sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax55', hypothesis, sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax46', hypothesis, sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax45', hypothesis, oca_compartment_has_scg(oca,compartmentb,scg_compartmentb),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax11_$sk', plain, (((admin_file_has_level(admin,X3,X2) | ~admin_file_has_level_h(admin,X3,X2,X1)) | ~admin_file_has_compartments(admin,X3,X1)) | ~system_file_needs_level(system,X3,X2)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax11'])).
% 1.56/0.60 fof('$inc_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))))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax54', hypothesis, system_file_needs_level(system,secretfile,secret),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax39_$sk', plain, (((((admin_indi_may_file(admin,X2,X1,read) | ~admin_indi_has_compartments_for_file(admin,X2,X1)) | ~admin_indi_has_level_for_file(admin,X2,X1)) | ~admin_indi_has_need_to_know_for_file(admin,X2,X1)) | ~admin_indi_has_citizenship_for_file(admin,X2,X1)) | ~state_file_is_not_working_paper(X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax39'])).
% 1.56/0.60 fof('$inc_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))))))),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax38_$sk', plain, (admin_indi_has_citizenship_for_file(admin,X2,X1) | ~admin_indi_has_citizenship(admin,X2,usa)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax38'])).
% 1.56/0.60 fof('$inc_ax38', axiom, (! [K,F] : (admin_indi_has_citizenship(admin,K,usa) => admin_indi_has_citizenship_for_file(admin,K,F))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax82', hypothesis, owner_indi_has_need_to_know(owner_secretfile,alice,secretfile),
% 1.56/0.60 input).
% 1.56/0.60 fof('$inc_ax36_$sk', plain, ((admin_indi_has_need_to_know_for_file(admin,X3,X2) | ~owner_indi_has_need_to_know(X1,X3,X2)) | ~state_file_has_owner(X2,X1)),
% 1.56/0.60 inference(negpush_and_skolemize,[],['$inc_ax36'])).
% 1.56/0.60 fof('$inc_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)))),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax60', hypothesis, state_file_has_owner(secretfile,owner_secretfile),
% 1.56/0.60 input).
% 1.56/0.60 fof('alicereadsecret_$sk', plain, ~admin_indi_may_file(admin,alice,secretfile,read),
% 1.56/0.60 inference(negpush_and_skolemize,[],['alicereadsecret'])).
% 1.56/0.60 fof('alicereadsecret', conjecture, admin_indi_may_file(admin,alice,secretfile,read),
% 1.56/0.60 input).
% 1.56/0.60 fof('ax50', hypothesis, state_file_is_not_working_paper(secretfile),
% 1.56/0.60 input).
% 1.56/0.60 cnf('1', plain, (admin_indi_has_compartments(admin,X,cons(Y,Z)) | ~system_indi_needs_compartment(system,X,Y) | ~admin_indi_has_polygraph_for_compartment(admin,X,Y) | ~admin_indi_has_credit_for_compartment(admin,X,Y) | ~admin_indi_has_background_for_compartment(admin,X,Y) | ~admin_indi_has_level_for_compartment(admin,X,Y) | ~admin_indi_has_compartments(admin,X,Z) | ~admin_indi_has_citizenship(admin,X,usa) | ~admin_compartment_has_sso(admin,Y,U) | ~sso_indi_has_compartment(U,X,Y) | ~admin_indi_has_employment(admin,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax27_$sk'])).
% 1.56/0.60 cnf('2', plain, (system_indi_has_citizenship(system,alice,usa)),
% 1.56/0.60 inference(cnf_transformation,[],['ax71'])).
% 1.56/0.60 cnf('3', plain, (~system_indi_has_citizenship(system,X,Y) | admin_indi_has_citizenship(admin,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax23_$sk'])).
% 1.56/0.60 cnf('4', plain, (admin_indi_has_citizenship(admin,alice,usa)),
% 1.56/0.60 inference(resolution,[],['2','3'])).
% 1.56/0.60 cnf('5', plain, (~system_indi_is_hr_admin(system,X) | admin_indi_has_employment(admin,Y) | ~hr_admin_indi_has_employment(X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax21_$sk'])).
% 1.56/0.60 cnf('6', plain, (system_indi_is_hr_admin(system,hr_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax69'])).
% 1.56/0.60 cnf('7', plain, (~hr_admin_indi_has_employment(hr_admin,X) | admin_indi_has_employment(admin,X)),
% 1.56/0.60 inference(resolution,[],['5','6'])).
% 1.56/0.60 cnf('8', plain, (hr_admin_indi_has_employment(hr_admin,alice)),
% 1.56/0.60 inference(cnf_transformation,[],['ax75'])).
% 1.56/0.60 cnf('9', plain, (admin_indi_has_employment(admin,alice)),
% 1.56/0.60 inference(resolution,[],['7','8'])).
% 1.56/0.60 cnf('10', plain, (admin_indi_has_compartments(admin,alice,cons(X,Y)) | ~system_indi_needs_compartment(system,alice,X) | ~admin_indi_has_polygraph_for_compartment(admin,alice,X) | ~admin_indi_has_credit_for_compartment(admin,alice,X) | ~admin_indi_has_background_for_compartment(admin,alice,X) | ~admin_indi_has_level_for_compartment(admin,alice,X) | ~admin_indi_has_compartments(admin,alice,Y) | ~admin_compartment_has_sso(admin,X,Z) | ~sso_indi_has_compartment(Z,alice,X)),
% 1.56/0.60 inference(resolution,[then_simplify],['1','4','9'])).
% 1.56/0.60 cnf('11', plain, (system_indi_needs_compartment(system,alice,compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax78'])).
% 1.56/0.60 cnf('12', plain, (~oca_compartment_is_compartment(X,Y,Z,U,V,yes) | admin_indi_has_polygraph_for_compartment(admin,W,Y) | ~admin_indi_has_polygraph(admin,W) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax30_$sk'])).
% 1.56/0.60 cnf('13', plain, (oca_compartment_is_compartment(oca,compartmentb,confidential,topsecret,yes,yes)),
% 1.56/0.60 inference(cnf_transformation,[],['ax42'])).
% 1.56/0.60 cnf('14', plain, (system_indi_is_oca(system,oca)),
% 1.56/0.60 inference(cnf_transformation,[],['ax41'])).
% 1.56/0.60 cnf('15', plain, (admin_indi_has_polygraph_for_compartment(admin,X,compartmentb) | ~admin_indi_has_polygraph(admin,X)),
% 1.56/0.60 inference(resolution,[then_simplify],['12','13','14'])).
% 1.56/0.60 cnf('16', plain, (~system_indi_is_polygraph_admin(system,X) | admin_indi_has_polygraph(admin,Y) | ~polygraph_admin_indi_has_polygraph(X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax17_$sk'])).
% 1.56/0.60 cnf('17', plain, (system_indi_is_polygraph_admin(system,polygraph_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax66'])).
% 1.56/0.60 cnf('18', plain, (~polygraph_admin_indi_has_polygraph(polygraph_admin,X) | admin_indi_has_polygraph(admin,X)),
% 1.56/0.60 inference(resolution,[],['16','17'])).
% 1.56/0.60 cnf('19', plain, (polygraph_admin_indi_has_polygraph(polygraph_admin,alice)),
% 1.56/0.60 inference(cnf_transformation,[],['ax72'])).
% 1.56/0.60 cnf('20', plain, (admin_indi_has_polygraph(admin,alice)),
% 1.56/0.60 inference(resolution,[],['18','19'])).
% 1.56/0.60 cnf('21', plain, (admin_indi_has_polygraph_for_compartment(admin,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[],['15','20'])).
% 1.56/0.60 cnf('22', plain, (~oca_compartment_is_compartment(X,Y,Z,U,yes,V) | admin_indi_has_credit_for_compartment(admin,W,Y) | ~admin_indi_has_credit(admin,W) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax32_$sk'])).
% 1.56/0.60 cnf('23', plain, (admin_indi_has_credit_for_compartment(admin,X,compartmentb) | ~admin_indi_has_credit(admin,X)),
% 1.56/0.60 inference(resolution,[then_simplify],['22','13','14'])).
% 1.56/0.60 cnf('24', plain, (~system_indi_is_credit_admin(system,X) | admin_indi_has_credit(admin,Y) | ~credit_admin_indi_has_credit(X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax18_$sk'])).
% 1.56/0.60 cnf('25', plain, (system_indi_is_credit_admin(system,credit_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax67'])).
% 1.56/0.60 cnf('26', plain, (~credit_admin_indi_has_credit(credit_admin,X) | admin_indi_has_credit(admin,X)),
% 1.56/0.60 inference(resolution,[],['24','25'])).
% 1.56/0.60 cnf('27', plain, (credit_admin_indi_has_credit(credit_admin,alice)),
% 1.56/0.60 inference(cnf_transformation,[],['ax73'])).
% 1.56/0.60 cnf('28', plain, (admin_indi_has_credit(admin,alice)),
% 1.56/0.60 inference(resolution,[],['26','27'])).
% 1.56/0.60 cnf('29', plain, (admin_indi_has_credit_for_compartment(admin,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[],['23','28'])).
% 1.56/0.60 cnf('30', plain, (~loca_level_below(admin,X,Y) | admin_indi_has_background(admin,Z,X) | ~background_admin_indi_has_background(U,Z,Y) | ~system_indi_is_background_admin(system,U)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax20_$sk'])).
% 1.56/0.60 cnf('31', plain, (loca_level_below(X,Y,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax4_$sk'])).
% 1.56/0.60 cnf('32', plain, (admin_indi_has_background(admin,X,Y) | ~background_admin_indi_has_background(Z,X,Y) | ~system_indi_is_background_admin(system,Z)),
% 1.56/0.60 inference(resolution,[],['30','31'])).
% 1.56/0.60 cnf('33', plain, (system_indi_is_background_admin(system,background_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax68'])).
% 1.56/0.60 cnf('34', plain, (~background_admin_indi_has_background(background_admin,X,Y) | admin_indi_has_background(admin,X,Y)),
% 1.56/0.60 inference(resolution,[],['32','33'])).
% 1.56/0.60 cnf('35', plain, (background_admin_indi_has_background(background_admin,alice,topsecret)),
% 1.56/0.60 inference(cnf_transformation,[],['ax74'])).
% 1.56/0.60 cnf('36', plain, (admin_indi_has_background(admin,alice,topsecret)),
% 1.56/0.60 inference(resolution,[],['34','35'])).
% 1.56/0.60 cnf('37', plain, (~oca_compartment_is_compartment(X,Y,Z,U,V,W) | ~admin_indi_has_background(admin,X2006,U) | admin_indi_has_background_for_compartment(admin,X2006,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax28_$sk'])).
% 1.56/0.60 cnf('38', plain, (~oca_compartment_is_compartment(X,Y,Z,topsecret,U,V) | admin_indi_has_background_for_compartment(admin,alice,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['36','37'])).
% 1.56/0.60 cnf('39', plain, (admin_indi_has_background_for_compartment(admin,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[then_simplify],['38','13','14'])).
% 1.56/0.60 cnf('40', plain, (~system_indi_needs_level(system,X,Y) | ~admin_indi_has_citizenship(admin,X,usa) | ~admin_indi_has_background(admin,X,Z) | ~loca_level_below(admin,Z,Y) | ~loca_level_below(admin,Z,U) | admin_indi_has_level(admin,X,Z) | ~level_admin_indi_has_level(V,X,U) | ~system_indi_is_level_admin(system,V) | ~admin_indi_has_employment(admin,X) | ~admin_indi_has_credit(admin,X) | ~admin_indi_has_polygraph(admin,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax25_$sk'])).
% 1.56/0.60 cnf('41', plain, (admin_indi_has_credit(admin,alice)),
% 1.56/0.60 inference(resolution,[],['26','27'])).
% 1.56/0.60 cnf('42', plain, (admin_indi_has_polygraph(admin,alice)),
% 1.56/0.60 inference(resolution,[],['18','19'])).
% 1.56/0.60 cnf('43', plain, (~system_indi_needs_level(system,alice,X) | ~admin_indi_has_background(admin,alice,Y) | admin_indi_has_level(admin,alice,Y) | ~loca_level_below(admin,Y,Z) | ~loca_level_below(admin,Y,X) | ~level_admin_indi_has_level(U,alice,Z) | ~system_indi_is_level_admin(system,U)),
% 1.56/0.60 inference(resolution,[then_simplify],['40','4','9','41','42'])).
% 1.56/0.60 cnf('44', plain, (system_indi_needs_level(system,alice,secret)),
% 1.56/0.60 inference(cnf_transformation,[],['ax76'])).
% 1.56/0.60 cnf('45', plain, (~admin_indi_has_background(admin,alice,X) | admin_indi_has_level(admin,alice,X) | ~loca_level_below(admin,X,secret) | ~loca_level_below(admin,X,Y) | ~level_admin_indi_has_level(Z,alice,Y) | ~system_indi_is_level_admin(system,Z)),
% 1.56/0.60 inference(resolution,[],['43','44'])).
% 1.56/0.60 cnf('46', plain, (~loca_level_below(X,Y,Z) | ~loca_level_direct_below(X,Z,U) | loca_level_below(X,Y,U)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax5_$sk'])).
% 1.56/0.60 cnf('47', plain, (~loca_level_direct_below(X,Y,Z) | loca_level_below(X,Y,Z)),
% 1.56/0.60 inference(resolution,[],['46','31'])).
% 1.56/0.60 cnf('48', plain, (loca_level_direct_below(X,confidential,secret)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax2_$sk'])).
% 1.56/0.60 cnf('49', plain, (loca_level_below(X,confidential,secret)),
% 1.56/0.60 inference(resolution,[],['47','48'])).
% 1.56/0.60 cnf('50', plain, (~loca_level_direct_below(X,secret,Y) | loca_level_below(X,confidential,Y)),
% 1.56/0.60 inference(resolution,[],['49','46'])).
% 1.56/0.60 cnf('51', plain, (loca_level_direct_below(X,secret,topsecret)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax3_$sk'])).
% 1.56/0.60 cnf('52', plain, (loca_level_below(X,confidential,topsecret)),
% 1.56/0.60 inference(resolution,[],['50','51'])).
% 1.56/0.60 cnf('53', plain, (admin_indi_has_background(admin,X,confidential) | ~background_admin_indi_has_background(Y,X,topsecret) | ~system_indi_is_background_admin(system,Y)),
% 1.56/0.60 inference(resolution,[],['30','52'])).
% 1.56/0.60 cnf('54', plain, (system_indi_is_background_admin(system,background_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax68'])).
% 1.56/0.60 cnf('55', plain, (admin_indi_has_background(admin,alice,confidential)),
% 1.56/0.60 inference(resolution,[then_simplify],['53','35','54'])).
% 1.56/0.60 cnf('56', plain, (loca_level_below(X3,confidential,secret)),
% 1.56/0.60 inference(resolution,[],['47','48'])).
% 1.56/0.60 cnf('57', plain, (admin_indi_has_level(admin,alice,confidential) | ~loca_level_below(admin,confidential,X) | ~level_admin_indi_has_level(Y,alice,X) | ~system_indi_is_level_admin(system,Y)),
% 1.56/0.60 inference(resolution,[then_simplify],['45','55','56'])).
% 1.56/0.60 cnf('58', plain, (admin_indi_has_level(admin,alice,confidential) | ~level_admin_indi_has_level(X,alice,topsecret) | ~system_indi_is_level_admin(system,X)),
% 1.56/0.60 inference(resolution,[],['57','52'])).
% 1.56/0.60 cnf('59', plain, (level_admin_indi_has_level(level_admin,alice,topsecret)),
% 1.56/0.60 inference(cnf_transformation,[],['ax77'])).
% 1.56/0.60 cnf('60', plain, (system_indi_is_level_admin(system,level_admin)),
% 1.56/0.60 inference(cnf_transformation,[],['ax70'])).
% 1.56/0.60 cnf('61', plain, (admin_indi_has_level(admin,alice,confidential)),
% 1.56/0.60 inference(resolution,[then_simplify],['58','59','60'])).
% 1.56/0.60 cnf('62', plain, (~oca_compartment_is_compartment(X,Y,Z,U,V,W) | ~admin_indi_has_level(admin,X2006,Z) | admin_indi_has_level_for_compartment(admin,X2006,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax29_$sk'])).
% 1.56/0.60 cnf('63', plain, (~oca_compartment_is_compartment(X,Y,confidential,Z,U,V) | admin_indi_has_level_for_compartment(admin,alice,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['61','62'])).
% 1.56/0.60 cnf('64', plain, (admin_indi_has_level_for_compartment(admin,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[then_simplify],['63','13','14'])).
% 1.56/0.60 cnf('65', plain, (admin_indi_has_compartments(admin,alice,cons(compartmentb,X)) | ~admin_indi_has_compartments(admin,alice,X) | ~admin_compartment_has_sso(admin,compartmentb,Y) | ~sso_indi_has_compartment(Y,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[then_simplify],['10','11','21','29','39','64'])).
% 1.56/0.60 cnf('66', plain, (system_indi_needs_compartment(system,alice,compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax79'])).
% 1.56/0.60 cnf('67', plain, (loca_level_direct_below(X,sbu,confidential)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax1_$sk'])).
% 1.56/0.60 cnf('68', plain, (loca_level_below(X,sbu,confidential)),
% 1.56/0.60 inference(resolution,[],['47','67'])).
% 1.56/0.60 cnf('69', plain, (~loca_level_direct_below(X,confidential,Y) | loca_level_below(X,sbu,Y)),
% 1.56/0.60 inference(resolution,[],['68','46'])).
% 1.56/0.60 cnf('70', plain, (loca_level_below(X,sbu,secret)),
% 1.56/0.60 inference(resolution,[],['69','48'])).
% 1.56/0.60 cnf('71', plain, (~loca_level_direct_below(X,secret,Y) | loca_level_below(X,sbu,Y)),
% 1.56/0.60 inference(resolution,[],['70','46'])).
% 1.56/0.60 cnf('72', plain, (loca_level_below(X,sbu,topsecret)),
% 1.56/0.60 inference(resolution,[],['71','51'])).
% 1.56/0.60 cnf('73', plain, (admin_indi_has_background(admin,X,sbu) | ~background_admin_indi_has_background(Y,X,topsecret) | ~system_indi_is_background_admin(system,Y)),
% 1.56/0.60 inference(resolution,[],['30','72'])).
% 1.56/0.60 cnf('74', plain, (admin_indi_has_background(admin,alice,sbu)),
% 1.56/0.60 inference(resolution,[then_simplify],['73','35','54'])).
% 1.56/0.60 cnf('75', plain, (loca_level_below(X3,sbu,secret)),
% 1.56/0.60 inference(resolution,[],['69','48'])).
% 1.56/0.60 cnf('76', plain, (admin_indi_has_level(admin,alice,sbu) | ~loca_level_below(admin,sbu,X) | ~level_admin_indi_has_level(Y,alice,X) | ~system_indi_is_level_admin(system,Y)),
% 1.56/0.60 inference(resolution,[then_simplify],['45','74','75'])).
% 1.56/0.60 cnf('77', plain, (admin_indi_has_level(admin,alice,sbu) | ~level_admin_indi_has_level(X,alice,topsecret) | ~system_indi_is_level_admin(system,X)),
% 1.56/0.60 inference(resolution,[],['76','72'])).
% 1.56/0.60 cnf('78', plain, (admin_indi_has_level(admin,alice,sbu)),
% 1.56/0.60 inference(resolution,[then_simplify],['77','59','60'])).
% 1.56/0.60 cnf('79', plain, (~oca_compartment_is_compartment(X,Y,sbu,Z,U,V) | admin_indi_has_level_for_compartment(admin,alice,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['78','62'])).
% 1.56/0.60 cnf('80', plain, (oca_compartment_is_compartment(oca,compartmenta,sbu,unclassified,no,no)),
% 1.56/0.60 inference(cnf_transformation,[],['ax43'])).
% 1.56/0.60 cnf('81', plain, (admin_indi_has_level_for_compartment(admin,alice,compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['79','80','14'])).
% 1.56/0.60 cnf('82', plain, (~oca_compartment_is_compartment(X,Y,Z,U,V,no) | admin_indi_has_polygraph_for_compartment(admin,W,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax31_$sk'])).
% 1.56/0.60 cnf('83', plain, (admin_indi_has_polygraph_for_compartment(admin,X3,compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['82','80','14'])).
% 1.56/0.60 cnf('84', plain, (~oca_compartment_is_compartment(X,Y,Z,U,no,V) | admin_indi_has_credit_for_compartment(admin,W,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax33_$sk'])).
% 1.56/0.60 cnf('85', plain, (admin_indi_has_credit_for_compartment(admin,X3,compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['84','80','14'])).
% 1.56/0.60 cnf('86', plain, (admin_indi_has_background(admin,X,unclassified)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax19_$sk'])).
% 1.56/0.60 cnf('87', plain, (~oca_compartment_is_compartment(X,Y,Z,unclassified,U,V) | admin_indi_has_background_for_compartment(admin,W,Y) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['37','86'])).
% 1.56/0.60 cnf('88', plain, (admin_indi_has_background_for_compartment(admin,X3,compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['87','80','14'])).
% 1.56/0.60 cnf('89', plain, (admin_indi_has_compartments(admin,alice,cons(compartmenta,X)) | ~admin_indi_has_compartments(admin,alice,X) | ~admin_compartment_has_sso(admin,compartmenta,Y) | ~sso_indi_has_compartment(Y,alice,compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['10','66','81','83','85','88'])).
% 1.56/0.60 cnf('90', plain, (admin_indi_has_compartments(admin,X,nil)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax26_$sk'])).
% 1.56/0.60 cnf('91', plain, (admin_indi_has_compartments(admin,alice,cons(compartmenta,nil)) | ~admin_compartment_has_sso(admin,compartmenta,X) | ~sso_indi_has_compartment(X,alice,compartmenta)),
% 1.56/0.60 inference(resolution,[],['89','90'])).
% 1.56/0.60 cnf('92', plain, (system_compartment_has_sso(system,compartmenta,sso_compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax47'])).
% 1.56/0.60 cnf('93', plain, (~system_compartment_has_sso(system,X,Y) | admin_compartment_has_sso(admin,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax6_$sk'])).
% 1.56/0.60 cnf('94', plain, (admin_compartment_has_sso(admin,compartmenta,sso_compartmenta)),
% 1.56/0.60 inference(resolution,[],['92','93'])).
% 1.56/0.60 cnf('95', plain, (sso_indi_has_compartment(sso_compartmenta,alice,compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax81'])).
% 1.56/0.60 cnf('96', plain, (admin_indi_has_compartments(admin,alice,cons(compartmenta,nil))),
% 1.56/0.60 inference(resolution,[then_simplify],['91','94','95'])).
% 1.56/0.60 cnf('97', plain, (admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil))) | ~admin_compartment_has_sso(admin,compartmentb,X) | ~sso_indi_has_compartment(X,alice,compartmentb)),
% 1.56/0.60 inference(resolution,[],['65','96'])).
% 1.56/0.60 cnf('98', plain, (system_compartment_has_sso(system,compartmentb,sso_compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax44'])).
% 1.56/0.60 cnf('99', plain, (admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)),
% 1.56/0.60 inference(resolution,[],['98','93'])).
% 1.56/0.60 cnf('100', plain, (sso_indi_has_compartment(sso_compartmentb,alice,compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax80'])).
% 1.56/0.60 cnf('101', plain, (admin_indi_has_compartments(admin,alice,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(resolution,[then_simplify],['97','99','100'])).
% 1.56/0.60 cnf('102', plain, (~admin_indi_has_compartments(admin,X,Y) | ~admin_file_has_compartments(admin,Z,Y) | admin_indi_has_compartments_for_file(admin,X,Z)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax34_$sk'])).
% 1.56/0.60 cnf('103', plain, (~admin_file_has_compartments(admin,X,cons(compartmentb,cons(compartmenta,nil))) | admin_indi_has_compartments_for_file(admin,alice,X)),
% 1.56/0.60 inference(resolution,[],['101','102'])).
% 1.56/0.60 cnf('104', plain, (admin_file_has_compartments_h(admin,X,Y,cons(Z,U)) | ~admin_file_has_compartments_h(admin,X,Y,U) | ~admin_compartment_has_sso(admin,Z,V) | ~sso_file_has_compartments(V,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax10_$sk'])).
% 1.56/0.60 cnf('105', plain, (admin_file_has_compartments_h(admin,X,Y,nil)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax9_$sk'])).
% 1.56/0.60 cnf('106', plain, (admin_file_has_compartments_h(admin,X,Y,cons(Z,nil)) | ~admin_compartment_has_sso(admin,Z,U) | ~sso_file_has_compartments(U,X,Y)),
% 1.56/0.60 inference(resolution,[],['104','105'])).
% 1.56/0.60 cnf('107', plain, (admin_file_has_compartments_h(admin,X,Y,cons(compartmenta,nil)) | ~sso_file_has_compartments(sso_compartmenta,X,Y)),
% 1.56/0.60 inference(resolution,[],['106','94'])).
% 1.56/0.60 cnf('108', plain, (sso_file_has_compartments(sso_compartmenta,secretfile,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(cnf_transformation,[],['ax53'])).
% 1.56/0.60 cnf('109', plain, (admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmenta,nil))),
% 1.56/0.60 inference(resolution,[],['107','108'])).
% 1.56/0.60 cnf('110', plain, (admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(X,cons(compartmenta,nil))) | ~sso_file_has_compartments(Y,secretfile,cons(compartmentb,cons(compartmenta,nil))) | ~admin_compartment_has_sso(admin,X,Y)),
% 1.56/0.60 inference(resolution,[],['109','104'])).
% 1.56/0.60 cnf('111', plain, (sso_file_has_compartments(sso_compartmentb,secretfile,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(cnf_transformation,[],['ax52'])).
% 1.56/0.60 cnf('112', plain, (admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(X,cons(compartmenta,nil))) | ~admin_compartment_has_sso(admin,X,sso_compartmentb)),
% 1.56/0.60 inference(resolution,[],['110','111'])).
% 1.56/0.60 cnf('113', plain, (admin_file_has_compartments_h(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)),cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(resolution,[],['112','99'])).
% 1.56/0.60 cnf('114', plain, (~admin_file_has_compartments_h(admin,X,Y,Y) | ~system_file_needs_compartments(system,X,Y) | admin_file_has_compartments(admin,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax8_$sk'])).
% 1.56/0.60 cnf('115', plain, (system_file_needs_compartments(system,secretfile,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(cnf_transformation,[],['ax51'])).
% 1.56/0.60 cnf('116', plain, (admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(resolution,[then_simplify],['113','114','115'])).
% 1.56/0.60 cnf('117', plain, (loca_level_below(X,secret,topsecret)),
% 1.56/0.60 inference(resolution,[],['47','51'])).
% 1.56/0.60 cnf('118', plain, (admin_indi_has_background(admin,X,secret) | ~background_admin_indi_has_background(Y,X,topsecret) | ~system_indi_is_background_admin(system,Y)),
% 1.56/0.60 inference(resolution,[],['30','117'])).
% 1.56/0.60 cnf('119', plain, (admin_indi_has_background(admin,alice,secret)),
% 1.56/0.60 inference(resolution,[then_simplify],['118','35','54'])).
% 1.56/0.60 cnf('120', plain, (loca_level_below(X0,X1,X1)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax4_$sk'])).
% 1.56/0.60 cnf('121', plain, (admin_indi_has_level(admin,alice,secret) | ~loca_level_below(admin,secret,X) | ~level_admin_indi_has_level(Y,alice,X) | ~system_indi_is_level_admin(system,Y)),
% 1.56/0.60 inference(resolution,[then_simplify],['45','119','120'])).
% 1.56/0.60 cnf('122', plain, (admin_indi_has_level(admin,alice,secret) | ~level_admin_indi_has_level(X,alice,topsecret) | ~system_indi_is_level_admin(system,X)),
% 1.56/0.60 inference(resolution,[],['121','117'])).
% 1.56/0.60 cnf('123', plain, (admin_indi_has_level(admin,alice,secret)),
% 1.56/0.60 inference(resolution,[then_simplify],['122','59','60'])).
% 1.56/0.60 cnf('124', plain, (~admin_indi_has_level(admin,X,Y) | ~admin_file_has_level(admin,Z,Y) | admin_indi_has_level_for_file(admin,X,Z)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax35_$sk'])).
% 1.56/0.60 cnf('125', plain, (admin_indi_has_level_for_file(admin,alice,X) | ~admin_file_has_level(admin,X,secret)),
% 1.56/0.60 inference(resolution,[],['123','124'])).
% 1.56/0.60 cnf('126', plain, (~admin_compartment_has_sso(admin,X,Y) | admin_compartment_has_scg(admin,X,Z) | ~oca_compartment_has_scg(U,X,Z) | ~sso_compartment_has_scg(Y,X,Z) | ~system_indi_is_oca(system,U)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax7_$sk'])).
% 1.56/0.60 cnf('127', plain, (~sso_compartment_has_scg(sso_compartmenta,compartmenta,X) | admin_compartment_has_scg(admin,compartmenta,X) | ~oca_compartment_has_scg(Y,compartmenta,X) | ~system_indi_is_oca(system,Y)),
% 1.56/0.60 inference(resolution,[],['126','94'])).
% 1.56/0.60 cnf('128', plain, (sso_compartment_has_scg(sso_compartmenta,compartmenta,scg_compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax49'])).
% 1.56/0.60 cnf('129', plain, (admin_compartment_has_scg(admin,compartmenta,scg_compartmenta) | ~oca_compartment_has_scg(X,compartmenta,scg_compartmenta) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['127','128'])).
% 1.56/0.60 cnf('130', plain, (oca_compartment_has_scg(oca,compartmenta,scg_compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax48'])).
% 1.56/0.60 cnf('131', plain, (admin_compartment_has_scg(admin,compartmenta,scg_compartmenta)),
% 1.56/0.60 inference(resolution,[then_simplify],['129','130','14'])).
% 1.56/0.60 cnf('132', plain, (admin_file_has_level_h(admin,X,Y,cons(Z,U)) | ~admin_file_has_level_h(admin,X,Y,U) | ~sso_file_has_level(V,X,Y,W) | ~admin_compartment_has_scg(admin,Z,W) | ~admin_compartment_has_sso(admin,Z,V)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax13_$sk'])).
% 1.56/0.60 cnf('133', plain, (admin_file_has_level_h(admin,X,Y,nil)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax12_$sk'])).
% 1.56/0.60 cnf('134', plain, (admin_file_has_level_h(admin,X,Y,cons(Z,nil)) | ~sso_file_has_level(U,X,Y,V) | ~admin_compartment_has_scg(admin,Z,V) | ~admin_compartment_has_sso(admin,Z,U)),
% 1.56/0.60 inference(resolution,[],['132','133'])).
% 1.56/0.60 cnf('135', plain, (admin_file_has_level_h(admin,X,Y,cons(compartmenta,nil)) | ~sso_file_has_level(Z,X,Y,scg_compartmenta) | ~admin_compartment_has_sso(admin,compartmenta,Z)),
% 1.56/0.60 inference(resolution,[],['131','134'])).
% 1.56/0.60 cnf('136', plain, (admin_file_has_level_h(admin,X,Y,cons(compartmenta,nil)) | ~sso_file_has_level(sso_compartmenta,X,Y,scg_compartmenta)),
% 1.56/0.60 inference(resolution,[],['135','94'])).
% 1.56/0.60 cnf('137', plain, (sso_file_has_level(sso_compartmenta,secretfile,secret,scg_compartmenta)),
% 1.56/0.60 inference(cnf_transformation,[],['ax56'])).
% 1.56/0.60 cnf('138', plain, (admin_file_has_level_h(admin,secretfile,secret,cons(compartmenta,nil))),
% 1.56/0.60 inference(resolution,[],['136','137'])).
% 1.56/0.60 cnf('139', plain, (admin_file_has_level_h(admin,secretfile,secret,cons(X,cons(compartmenta,nil))) | ~sso_file_has_level(Y,secretfile,secret,Z) | ~admin_compartment_has_scg(admin,X,Z) | ~admin_compartment_has_sso(admin,X,Y)),
% 1.56/0.60 inference(resolution,[],['138','132'])).
% 1.56/0.60 cnf('140', plain, (sso_file_has_level(sso_compartmentb,secretfile,secret,scg_compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax55'])).
% 1.56/0.60 cnf('141', plain, (admin_file_has_level_h(admin,secretfile,secret,cons(X,cons(compartmenta,nil))) | ~admin_compartment_has_scg(admin,X,scg_compartmentb) | ~admin_compartment_has_sso(admin,X,sso_compartmentb)),
% 1.56/0.60 inference(resolution,[],['139','140'])).
% 1.56/0.60 cnf('142', plain, (~sso_compartment_has_scg(sso_compartmentb,compartmentb,X) | admin_compartment_has_scg(admin,compartmentb,X) | ~oca_compartment_has_scg(Y,compartmentb,X) | ~system_indi_is_oca(system,Y)),
% 1.56/0.60 inference(resolution,[],['126','99'])).
% 1.56/0.60 cnf('143', plain, (sso_compartment_has_scg(sso_compartmentb,compartmentb,scg_compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax46'])).
% 1.56/0.60 cnf('144', plain, (admin_compartment_has_scg(admin,compartmentb,scg_compartmentb) | ~oca_compartment_has_scg(X,compartmentb,scg_compartmentb) | ~system_indi_is_oca(system,X)),
% 1.56/0.60 inference(resolution,[],['142','143'])).
% 1.56/0.60 cnf('145', plain, (oca_compartment_has_scg(oca,compartmentb,scg_compartmentb)),
% 1.56/0.60 inference(cnf_transformation,[],['ax45'])).
% 1.56/0.60 cnf('146', plain, (admin_compartment_has_scg(admin,compartmentb,scg_compartmentb)),
% 1.56/0.60 inference(resolution,[then_simplify],['144','145','14'])).
% 1.56/0.60 cnf('147', plain, (admin_compartment_has_sso(admin,compartmentb,sso_compartmentb)),
% 1.56/0.60 inference(resolution,[],['98','93'])).
% 1.56/0.60 cnf('148', plain, (admin_file_has_level_h(admin,secretfile,secret,cons(compartmentb,cons(compartmenta,nil)))),
% 1.56/0.60 inference(resolution,[then_simplify],['141','146','147'])).
% 1.56/0.60 cnf('149', plain, (~admin_file_has_level_h(admin,X,Y,Z) | ~system_file_needs_level(system,X,Y) | ~admin_file_has_compartments(admin,X,Z) | admin_file_has_level(admin,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax11_$sk'])).
% 1.56/0.60 cnf('150', plain, (system_file_needs_level(system,secretfile,secret)),
% 1.56/0.60 inference(cnf_transformation,[],['ax54'])).
% 1.56/0.60 cnf('151', plain, (~admin_file_has_compartments(admin,secretfile,cons(compartmentb,cons(compartmenta,nil))) | admin_file_has_level(admin,secretfile,secret)),
% 1.56/0.60 inference(resolution,[then_simplify],['148','149','150'])).
% 1.56/0.60 cnf('152', plain, (admin_file_has_level(admin,secretfile,secret)),
% 1.56/0.60 inference(resolution,[],['116','151'])).
% 1.56/0.60 cnf('153', plain, (admin_indi_has_level_for_file(admin,alice,secretfile)),
% 1.56/0.60 inference(resolution,[],['125','152'])).
% 1.56/0.60 cnf('154', plain, (admin_indi_may_file(admin,X,Y,read) | ~admin_indi_has_citizenship_for_file(admin,X,Y) | ~admin_indi_has_need_to_know_for_file(admin,X,Y) | ~admin_indi_has_level_for_file(admin,X,Y) | ~admin_indi_has_compartments_for_file(admin,X,Y) | ~state_file_is_not_working_paper(Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax39_$sk'])).
% 1.56/0.60 cnf('155', plain, (~admin_indi_has_citizenship(admin,X,usa) | admin_indi_has_citizenship_for_file(admin,X,Y)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax38_$sk'])).
% 1.56/0.60 cnf('156', plain, (admin_indi_has_citizenship_for_file(admin,alice,X)),
% 1.56/0.60 inference(resolution,[],['4','155'])).
% 1.56/0.60 cnf('157', plain, (admin_indi_may_file(admin,alice,X,read) | ~admin_indi_has_need_to_know_for_file(admin,alice,X) | ~admin_indi_has_level_for_file(admin,alice,X) | ~admin_indi_has_compartments_for_file(admin,alice,X) | ~state_file_is_not_working_paper(X)),
% 1.56/0.60 inference(resolution,[],['154','156'])).
% 1.56/0.60 cnf('158', plain, (owner_indi_has_need_to_know(owner_secretfile,alice,secretfile)),
% 1.56/0.60 inference(cnf_transformation,[],['ax82'])).
% 1.56/0.60 cnf('159', plain, (admin_indi_has_need_to_know_for_file(admin,X,Y) | ~owner_indi_has_need_to_know(Z,X,Y) | ~state_file_has_owner(Y,Z)),
% 1.56/0.60 inference(cnf_transformation,[],['$inc_ax36_$sk'])).
% 1.56/0.60 cnf('160', plain, (state_file_has_owner(secretfile,owner_secretfile)),
% 1.56/0.60 inference(cnf_transformation,[],['ax60'])).
% 1.56/0.60 cnf('161', plain, (admin_indi_has_need_to_know_for_file(admin,alice,secretfile)),
% 1.56/0.60 inference(resolution,[then_simplify],['158','159','160'])).
% 1.56/0.60 cnf('162', plain, (~admin_indi_may_file(admin,alice,secretfile,read)),
% 1.56/0.60 inference(cnf_transformation,[],['alicereadsecret_$sk'])).
% 1.56/0.60 cnf('163', plain, (state_file_is_not_working_paper(secretfile)),
% 1.56/0.60 inference(cnf_transformation,[],['ax50'])).
% 1.56/0.60 cnf('164', plain, (~admin_indi_has_level_for_file(admin,alice,secretfile) | ~admin_indi_has_compartments_for_file(admin,alice,secretfile)),
% 1.56/0.60 inference(resolution,[then_simplify],['157','161','162','163'])).
% 1.56/0.60 cnf('165', plain, (~admin_indi_has_compartments_for_file(admin,alice,secretfile)),
% 1.56/0.60 inference(resolution,[],['153','164'])).
% 1.56/0.60 cnf('166', plain, ($false),
% 1.56/0.60 inference(resolution,[then_simplify],['103','116','165'])).
% 1.56/0.60
% 1.56/0.60 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.56/0.60
% 1.56/0.60 run 9 fork 0 statistics:
% 1.56/0.60 ----------------------------------
% 1.56/0.60 this run seconds: 0.017235
% 1.56/0.60 total seconds: 0.182031
% 1.56/0.60 stat_given_used: 575
% 1.56/0.60 stat_given_used_at_endgame: 0
% 1.56/0.60 stat_given_candidates: 776
% 1.56/0.60 stat_given_candidates_at_endgame: 0
% 1.56/0.60 stat_given_candidates_h: 0
% 1.56/0.60 stat_binres_derived_cl: 659
% 1.56/0.60 stat_binres_derived_cl_h: 0
% 1.56/0.60 stat_factor_derived_cl: 4
% 1.56/0.60 stat_para_derived_cl: 0
% 1.56/0.60 stat_tautologies_discarded: 0
% 1.56/0.60 stat_forward_subsumed: 86
% 1.56/0.60 stat_derived_cut: 177
% 1.56/0.60 stat_derived_rewritten: 0
% 1.56/0.60 stat_weight_discarded_building: 0
% 1.56/0.60 stat_weight_discarded_cl: 0
% 1.56/0.60 stat_internlimit_discarded_cl: 0
% 1.56/0.60 stat_simplified: 0 simplified 0 derived 0 given
% 1.56/0.60 stat_kept_cl: 576
% 1.56/0.60 stat_built_cl: 1726
% 1.56/0.60 stat_hyperres_partial_cl: 0
% 1.56/0.60 stat_made_rewriters: 0
% 1.56/0.60 stat_backward_subsumed: 0
% 1.56/0.60 stat_propagated_subsumed: 0
% 1.56/0.60 stat_clsubs_attempted: 7139
% 1.56/0.60 stat_clsubs_fact_groundunit_found: 63
% 1.56/0.60 stat_clsubs_rule_groundunit_found: 6
% 1.56/0.60 stat_clsubs_top_meta_attempted: 110417
% 1.56/0.60 stat_clsubs_top_meta_failed: 103278
% 1.56/0.60 stat_clsubs_top_meta_nonpref_attempted: 110417
% 1.56/0.60 stat_clsubs_top_meta_nonpref_succeeded: 47981
% 1.56/0.60 stat_clsubs_top_meta_pref_attempted: 47981
% 1.56/0.60 stat_clsubs_top_meta_pref1_succeeded: 7610
% 1.56/0.60 stat_clsubs_top_meta_pref2_succeeded: 7262
% 1.56/0.60 stat_clsubs_top_meta_pref3_succeeded: 7139
% 1.56/0.60 stat_clsubs_top_meta_pref_succeeded: 7139
% 1.56/0.60 stat_clsubs_meta_attempted: 13743
% 1.56/0.60 stat_clsubs_meta_failed: 6501
% 1.56/0.60 stat_clsubs_predsymbs_attempted: 0
% 1.56/0.60 stat_clsubs_unit_attempted: 1185
% 1.56/0.60 stat_clsubs_full_attempted: 5954
% 1.56/0.60 stat_forwardsubs_attempted: 663
% 1.56/0.60 stat_lit_hash_added: 623
% 1.56/0.60 stat_lit_hash_computed: 7040
% 1.56/0.60 stat_lit_hash_match_found: 428
% 1.56/0.60 stat_lit_hash_match_miss: 9124
% 1.56/0.60 stat_lit_hash_cut_ok: 265
% 1.56/0.60 stat_lit_strong_cut_ok: 11
% 1.56/0.60 stat_lit_hash_subsume_ok: 86
% 1.56/0.60 clqueue els 10000000 used 1
% 1.56/0.60 clactive els 10000000 used 576
% 1.56/0.60 clactivesubsume els 10000000 used 2179
% 1.56/0.60 queue_termbuf els 200000000 used 36500
% 1.56/0.60 hyper_termbuf els 100000000 used 1
% 1.56/0.60 active_termbuf els 100000000 used 25103
% 1.56/0.60 varstack els 5000 last used 1
% 1.56/0.60 given_termbuf els 10000000 last used 1
% 1.56/0.60 simplified_termbuf els 10000000 last used 1
% 1.56/0.60 derived_termbuf els 10000000 last used 23
% 1.56/0.60 wr_mallocs: 3039
% 1.56/0.60 wr_callocs: 21
% 1.56/0.60 wr_reallocs: 154
% 1.56/0.60 wr_frees: 2
% 1.56/0.60 wr_malloc_bytes: 4162683188
% 1.56/0.60 wr_calloc_bytes: 112065536
% 1.56/0.60 wr_realloc_bytes: 89120
% 1.56/0.60 wr_realloc_freebytes: 0
% 1.56/0.60 ----------------------------------
%------------------------------------------------------------------------------