%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:10:52 AM UTC 2026
% Result : Theorem 1.05s 0.67s
% Output : CNFRefutation 1.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT067+1 : TPTP v9.3.0. Released v5.5.0.
% 0.00/0.04 % Command : gkc %s
% 0.10/0.37 % Computer : n006.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 7 13:50:46 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.20/0.50
% 0.20/0.50 input clause set summed statistics:
% 0.20/0.50 ----------------------------------
% 0.20/0.50 in_clause_count: 180
% 0.20/0.50 in_rule_clause_count: 170
% 0.20/0.50 in_fact_clause_count: 10
% 0.20/0.50 in_answer_clause_count: 0
% 0.20/0.50 in_ground_clause_count: 127
% 0.20/0.50 in_unit_clause_count: 130
% 0.20/0.50 in_horn_clause_count: 171
% 0.20/0.50 in_pos_clause_count: 129
% 0.20/0.50 in_neg_clause_count: 19
% 0.20/0.50 in_poseq_clause_count: 0
% 0.20/0.50 in_negeq_clause_count: 0
% 0.20/0.50 in_unitposeq_clause_count: 0
% 0.20/0.50 in_chain_clause_count: 0
% 0.20/0.50 in_min_length: 1
% 0.20/0.50 in_max_length: 20
% 0.20/0.50 in_min_depth: 1
% 0.20/0.50 in_max_depth: 3
% 0.20/0.50 in_min_size: 2
% 0.20/0.50 in_max_size: 117
% 0.20/0.50 in_min_vars: 0
% 0.20/0.50 in_max_vars: 15
% 0.20/0.50 in_extaxiom_count: 0
% 0.20/0.50 in_axiom_count: 178
% 0.20/0.50 in_assumption_count: 0
% 0.20/0.50 in_goal_count: 2
% 0.20/0.50 in_neg_goal_count: 1
% 0.20/0.50 in_pos_goal_count: 1
% 0.20/0.50 in_posunit_goal_count: 1
% 0.20/0.50
% 0.20/0.50 auto guide:
% 0.20/0.50 -----------
% 0.20/0.50 {
% 0.20/0.50 "print":1,
% 0.20/0.50 "print_level": 15,
% 0.20/0.50 "max_size": 0,
% 0.20/0.50 "max_depth": 0,
% 0.20/0.50 "max_length": 0,
% 0.20/0.50 "max_dseconds": 0,
% 0.20/0.50 "equality":0,
% 0.20/0.50 "runs":[
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.20/0.50 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.50 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.20/0.50 {"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.50 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.50 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.50 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.50 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.20/0.50
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":1},
% 0.20/0.50 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.20/0.50 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.50 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.20/0.50 {"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.50 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":10},
% 0.20/0.50 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.50 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.50 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.50 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.20/0.50
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "double"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":1},
% 0.20/0.50 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.20/0.50 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.20/0.50 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.20/0.50 {"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.50 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":50},
% 0.20/0.50 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.20/0.50 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.20/0.50 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.20/0.50 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.20/0.50 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.20/0.50
% 0.20/0.50 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.20/0.50 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.50 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.50 {"max_dseconds":250, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.50 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":250, "strategy":["unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.20/0.50
% 0.20/0.50 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["unit"], "query_preference":2},
% 0.20/0.50 {"max_dseconds":1250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0}
% 0.20/0.50
% 0.20/0.50 ]}
% 0.20/0.50
% 0.20/0.50
% 0.20/0.50 **** run 1 fork 0 starts with strategy
% 0.20/0.50 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.20/0.50
% 0.20/0.50 **** run 2 fork 1 starts with strategy
% 0.20/0.50 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.20/0.51
% 0.20/0.51 **** run 3 fork 2 starts with strategy
% 0.20/0.51 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.20/0.51
% 0.20/0.51 **** run 4 fork 3 starts with strategy
% 0.20/0.51 {"max_dseconds":1,"sine":5,"strategy":["unit"],"query_preference":0}
% 0.20/0.51
% 0.20/0.51 **** run 5 fork 4 starts with strategy
% 0.20/0.51 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.51
% 0.20/0.51 **** run 6 fork 5 starts with strategy
% 0.20/0.51 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.52
% 0.20/0.52 **** run 7 fork 6 starts with strategy
% 0.20/0.52 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.20/0.52
% 0.20/0.52 **** run 8 fork 7 starts with strategy
% 0.20/0.52 {"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.20/0.53
% 0.20/0.53 fork 1: search finished without proof.
% 0.20/0.54
% 0.20/0.54 fork 2: search finished without proof.
% 0.20/0.54
% 0.20/0.54 fork 3: search finished without proof.
% 0.73/0.61
% 0.73/0.61 **** run 10 fork 1 starts with strategy
% 0.73/0.61 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.73/0.62
% 0.73/0.62 **** run 11 fork 2 starts with strategy
% 0.73/0.62 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 0.73/0.62
% 0.73/0.62 **** run 12 fork 3 starts with strategy
% 0.73/0.62 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 1.05/0.67
% 1.05/0.67 fork 5: search finished without proof.
% 1.05/0.67
% 1.05/0.67
% 1.05/0.67 result: proof found
% 1.05/0.67 for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/0.67 by run 11 fork 2 strategy {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 1.05/0.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/0.67
% 1.05/0.67 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/0.67 fof('co1_$sk', plain, (~ssRequisitionCreated(ssMUELLER,X8,X7,X6,ssINF,X5,X4,X3,X2,X1) & ssRequisition(X16,X15,X14,X13,ssINF,X12,X11,X10,X9)),
% 1.05/0.67 inference(negpush_and_skolemize,[],['co1'])).
% 1.05/0.67 fof('co1', conjecture, (? [U,V,W,X,Y,Z,X1,X2,X3] : (ssRequisition(Y,Z,X1,U,ssINF,W,X,X2,X3) => ssRequisitionCreated(ssMUELLER,Y,Z,X1,ssINF,V,W,X,X2,X3))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax149_$sk', plain, (ssRequisitionCreated(X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) | (~ssAccess(X10,authObj(ssM_BANF_EKG,ssEKGRP,X5)) | (~ssAccess(X10,authObj(ssM_BANF_BSA,ssBSART,X9)) | (~ssAccess(X10,authObj(ssM_BANF_WRK,ssWERKS,X6)) | (~ssAccess(X10,ssME51N) | (~ssStandardPurchase(X9) | ~ssRequisition(X9,X8,X7,X6,X5,X4,X3,X2,X1))))))),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax149'])).
% 1.05/0.67 fof('ax149', axiom, (! [U,V,W,X,Y,Z,X1,X2,X3,X4] : ((((((ssRequisition(W,Z,X1,V,X,X2,Y,X3,X4) & ssStandardPurchase(W)) & ssAccess(U,ssME51N)) & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))) & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))) & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))) => ssRequisitionCreated(U,W,Z,X1,V,X,X2,Y,X3,X4))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax137_$sk', plain, (ssAccess(X4,authObj(X1,X2,X3)) | ~ssUserProfile(userProfileEntry(X4,authObj(X1,X2,X3)))),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax137'])).
% 1.05/0.67 fof('ax137', axiom, (! [U,V,W,X] : (ssUserProfile(userProfileEntry(U,authObj(V,W,X))) => ssAccess(U,authObj(V,W,X)))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax141_$sk', plain, (ssUserProfile(userProfileEntry(X7,authObj(X4,X5,X6))) | ((~ssHolds(X7,X1) | (~ssSingleRole(singleRoleEntry(X2,authObj(X4,X5,X6))) | ~ssCompositeRole(compositeRoleEntry(X1,X2)))) & ((~ssHolds(X7,X2) | ~ssSingleRole(singleRoleEntry(X2,authObj(X4,X5,X6)))) & (~ssHolds(X7,X3) | ~ssProfile(profileEntry(X3,authObj(X4,X5,X6))))))),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax141'])).
% 1.05/0.67 fof('ax141', axiom, (! [U,V,W,X,Y,Z,X1] : ((((ssProfile(profileEntry(V,authObj(Y,Z,X1))) & ssHolds(U,V)) | (ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1))) & ssHolds(U,W))) | ((ssCompositeRole(compositeRoleEntry(X,W)) & ssSingleRole(singleRoleEntry(W,authObj(Y,Z,X1)))) & ssHolds(U,X))) => ssUserProfile(userProfileEntry(U,authObj(Y,Z,X1))))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax16', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax114', axiom, ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax155_$sk', plain, ((~ssOrderCreated(X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) | (~ssRequisitionReleased(X10,X9,X8,X7,X6,X5,X4,X3,X2,X1) | ~ssRequisitionCreated(X10,X9,X8,X7,X6,X5,X4,X3,X2,X1))) & ssRequisition(X19,X18,X17,X16,X15,X14,X13,X12,X11)),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax155'])).
% 1.05/0.67 fof('ax155', axiom, ~(? [U,V,W,X,Y,Z,X1,X2,X3,X4] : (ssRequisition(Z,X1,X2,V,W,X,Y,X3,X4) => ((ssRequisitionCreated(U,Z,X1,X2,V,W,X,Y,X3,X4) & ssRequisitionReleased(U,Z,X1,X2,V,W,X,Y,X3,X4)) & ssOrderCreated(U,Z,X1,X2,V,W,X,Y,X3,X4)))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax138_$sk', plain, (ssAccess(X4,authObj(X1,X2,X3)) | ~ssUserProfile(userProfileEntry(X4,authObj(X1,X2,ssSTAR)))),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax138'])).
% 1.05/0.67 fof('ax138', axiom, (! [U,V,W,X] : (ssUserProfile(userProfileEntry(U,authObj(V,W,ssSTAR))) => ssAccess(U,authObj(V,W,X)))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax18', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax20', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax118', axiom, ssStandardPurchase(ssNB),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax142_$sk', plain, (ssAccess(X4,ssME51N) | (~ssAccess(X4,authObj(ssM_BANF_EKG,ssEKGRP,X1)) | (~ssAccess(X4,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | (~ssAccess(X4,authObj(ssM_BANF_BSA,ssBSART,X2)) | (~ssAccess(X4,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | (~ssAccess(X4,authObj(ssM_BANF_WRK,ssWERKS,X3)) | (~ssAccess(X4,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X4,authObj(ssS_TCODE,ssTCD,ssME51N))))))))),
% 1.05/0.67 inference(negpush_and_skolemize,[],['ax142'])).
% 1.05/0.67 fof('ax142', axiom, (! [U,V,W,X] : (((((((ssAccess(U,authObj(ssS_TCODE,ssTCD,ssME51N)) & ssAccess(U,authObj(ssM_BANF_WRK,ssACTVT,np__1))) & ssAccess(U,authObj(ssM_BANF_WRK,ssWERKS,V))) & ssAccess(U,authObj(ssM_BANF_BSA,ssACTVT,np__1))) & ssAccess(U,authObj(ssM_BANF_BSA,ssBSART,W))) & ssAccess(U,authObj(ssM_BANF_EKG,ssACTVT,np__1))) & ssAccess(U,authObj(ssM_BANF_EKG,ssEKGRP,X))) => ssAccess(U,ssME51N))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax17', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax12', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax13', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1))),
% 1.05/0.67 input).
% 1.05/0.67 fof('ax19', axiom, ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))),
% 1.05/0.67 input).
% 1.05/0.67 cnf('1', plain, (~ssRequisitionCreated(ssMUELLER,X,Y,Z,ssINF,U,V,W,X2006,X2007)),
% 1.05/0.67 inference(cnf_transformation,[],['co1_$sk'])).
% 1.05/0.67 cnf('2', plain, (ssRequisitionCreated(X,Y,Z,U,V,W,X2006,X2007,X2008,X2009) | ~ssRequisition(Y,Z,U,V,W,X2006,X2007,X2008,X2009) | ~ssAccess(X,authObj(ssM_BANF_EKG,ssEKGRP,W)) | ~ssAccess(X,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssAccess(X,authObj(ssM_BANF_WRK,ssWERKS,V)) | ~ssAccess(X,ssME51N) | ~ssStandardPurchase(Y)),
% 1.05/0.67 inference(cnf_transformation,[],['ax149_$sk'])).
% 1.05/0.67 cnf('3', plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF)) | ~ssAccess(ssMUELLER,ssME51N) | ~ssRequisition(X,Y,Z,ssINF,U,V,W,X2006,X2007) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X)) | ~ssStandardPurchase(X)),
% 1.05/0.67 inference(resolution,[],['1','2'])).
% 1.05/0.67 cnf('4', plain, (~ssUserProfile(userProfileEntry(X,authObj(Y,Z,U))) | ssAccess(X,authObj(Y,Z,U))),
% 1.05/0.67 inference(cnf_transformation,[],['ax137_$sk'])).
% 1.05/0.67 cnf('5', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) | ~ssAccess(ssMUELLER,ssME51N) | ~ssRequisition(X,Y,Z,ssINF,U,V,W,X2006,X2007) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X)) | ~ssStandardPurchase(X)),
% 1.05/0.67 inference(resolution,[],['3','4'])).
% 1.05/0.67 cnf('6', plain, (~ssSingleRole(singleRoleEntry(X,authObj(Y,Z,U))) | ssUserProfile(userProfileEntry(V,authObj(Y,Z,U))) | ~ssHolds(V,X)),
% 1.05/0.67 inference(cnf_transformation,[],['ax141_$sk'])).
% 1.05/0.67 cnf('7', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssRequisition(X,Y,Z,ssINF,U,V,W,X2006,X2007) | ~ssSingleRole(singleRoleEntry(X2008,authObj(ssM_BANF_WRK,ssWERKS,ssINF))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X)) | ~ssHolds(ssMUELLER,X2008) | ~ssStandardPurchase(X)),
% 1.05/0.67 inference(resolution,[],['5','6'])).
% 1.05/0.67 cnf('8', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssWERKS,ssINF)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax16'])).
% 1.05/0.67 cnf('9', plain, (ssHolds(ssMUELLER,ssZBANF_WRK_INF_ED)),
% 1.05/0.67 inference(cnf_transformation,[],['ax114'])).
% 1.05/0.67 cnf('10', plain, (ssRequisition(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 1.05/0.67 inference(cnf_transformation,[],['ax155_$sk'])).
% 1.05/0.67 cnf('11', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssStandardPurchase(Y)),
% 1.05/0.67 inference(resolution,[then_simplify],['7','8','9','10'])).
% 1.05/0.67 cnf('12', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssStandardPurchase(Y)),
% 1.05/0.67 inference(resolution,[],['11','4'])).
% 1.05/0.67 cnf('13', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssEKGRP,Y))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssHolds(ssMUELLER,X) | ~ssStandardPurchase(Z)),
% 1.05/0.67 inference(resolution,[],['12','6'])).
% 1.05/0.67 cnf('14', plain, (~ssUserProfile(userProfileEntry(X,authObj(Y,Z,ssSTAR))) | ssAccess(X,authObj(Y,Z,U))),
% 1.05/0.67 inference(cnf_transformation,[],['ax138_$sk'])).
% 1.05/0.67 cnf('15', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) | ~ssAccess(ssMUELLER,ssME51N) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssEKGRP,Y))) | ~ssHolds(ssMUELLER,X) | ~ssStandardPurchase(Z)),
% 1.05/0.67 inference(resolution,[],['13','14'])).
% 1.05/0.67 cnf('16', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_BSA,ssBSART,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssEKGRP,Z))) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y) | ~ssStandardPurchase(U)),
% 1.05/0.67 inference(resolution,[],['15','6'])).
% 1.05/0.67 cnf('17', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssBSART,ssSTAR)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax18'])).
% 1.05/0.67 cnf('18', plain, (~ssAccess(ssMUELLER,ssME51N) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssEKGRP,Y))) | ~ssHolds(ssMUELLER,X) | ~ssStandardPurchase(Z)),
% 1.05/0.67 inference(resolution,[then_simplify],['16','17','9'])).
% 1.05/0.67 cnf('19', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssEKGRP,ssI26)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax20'])).
% 1.05/0.67 cnf('20', plain, (ssStandardPurchase(ssNB)),
% 1.05/0.67 inference(cnf_transformation,[],['ax118'])).
% 1.05/0.67 cnf('21', plain, (~ssAccess(ssMUELLER,ssME51N)),
% 1.05/0.67 inference(resolution,[then_simplify],['18','19','9','20'])).
% 1.05/0.67 cnf('22', plain, (~ssAccess(X,authObj(ssM_BANF_EKG,ssEKGRP,Y)) | ~ssAccess(X,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(X,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssAccess(X,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(X,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssAccess(X,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(X,authObj(ssS_TCODE,ssTCD,ssME51N)) | ssAccess(X,ssME51N)),
% 1.05/0.67 inference(cnf_transformation,[],['ax142_$sk'])).
% 1.05/0.67 cnf('23', plain, (~ssAccess(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,Z))),
% 1.05/0.67 inference(resolution,[],['21','22'])).
% 1.05/0.67 cnf('24', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,Z))),
% 1.05/0.67 inference(resolution,[],['23','4'])).
% 1.05/0.67 cnf('25', plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssSingleRole(singleRoleEntry(X,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssHolds(ssMUELLER,X)),
% 1.05/0.67 inference(resolution,[],['24','6'])).
% 1.05/0.67 cnf('26', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssSingleRole(singleRoleEntry(X,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssHolds(ssMUELLER,X)),
% 1.05/0.67 inference(resolution,[],['25','14'])).
% 1.05/0.67 cnf('27', plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,V)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y)),
% 1.05/0.67 inference(resolution,[],['26','6'])).
% 1.05/0.67 cnf('28', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssSingleRole(singleRoleEntry(X,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,V)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y)),
% 1.05/0.67 inference(resolution,[],['27','4'])).
% 1.05/0.67 cnf('29', plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,np__1)) | ~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,V)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,W)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y) | ~ssHolds(ssMUELLER,Z)),
% 1.05/0.67 inference(resolution,[],['28','6'])).
% 1.05/0.67 cnf('30', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(X,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,V)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,W)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y) | ~ssHolds(ssMUELLER,Z)),
% 1.05/0.67 inference(resolution,[],['29','14'])).
% 1.05/0.67 cnf('31', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(U,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,V)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,W)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X2006)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y) | ~ssHolds(ssMUELLER,Z) | ~ssHolds(ssMUELLER,U)),
% 1.05/0.67 inference(resolution,[],['30','6'])).
% 1.05/0.67 cnf('32', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_BSA,ssACTVT,ssSTAR)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax17'])).
% 1.05/0.67 cnf('33', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssS_TCODE,ssTCD,ssME51N))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,V)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,W)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y) | ~ssHolds(ssMUELLER,Z)),
% 1.05/0.67 inference(resolution,[then_simplify],['31','32','9'])).
% 1.05/0.67 cnf('34', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssS_TCODE,ssTCD,ssME51N)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax12'])).
% 1.05/0.67 cnf('35', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_WRK,ssACTVT,np__1))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,U)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,V)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Y)),
% 1.05/0.67 inference(resolution,[then_simplify],['33','34','9'])).
% 1.05/0.67 cnf('36', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_WRK,ssACTVT,np__1)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax13'])).
% 1.05/0.67 cnf('37', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssHolds(ssMUELLER,X)),
% 1.05/0.67 inference(resolution,[then_simplify],['35','36','9'])).
% 1.05/0.67 cnf('38', plain, (ssSingleRole(singleRoleEntry(ssZBANF_WRK_INF_ED,authObj(ssM_BANF_EKG,ssACTVT,ssSTAR)))),
% 1.05/0.67 inference(cnf_transformation,[],['ax19'])).
% 1.05/0.67 cnf('39', plain, (~ssAccess(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,Z))),
% 1.05/0.67 inference(resolution,[then_simplify],['37','38','9'])).
% 1.05/0.67 cnf('40', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_EKG,ssEKGRP,X))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Y)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,Z))),
% 1.05/0.67 inference(resolution,[],['39','4'])).
% 1.05/0.67 cnf('41', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssEKGRP,Y))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,Z)) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssHolds(ssMUELLER,X)),
% 1.05/0.67 inference(resolution,[],['40','6'])).
% 1.05/0.67 cnf('42', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_BSA,ssBSART,X))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssEKGRP,Z))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,U)) | ~ssHolds(ssMUELLER,Y)),
% 1.05/0.67 inference(resolution,[],['41','4'])).
% 1.05/0.67 cnf('43', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_BSA,ssBSART,Y))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_EKG,ssEKGRP,U))) | ~ssAccess(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,V)) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Z)),
% 1.05/0.67 inference(resolution,[],['42','6'])).
% 1.05/0.67 cnf('44', plain, (~ssUserProfile(userProfileEntry(ssMUELLER,authObj(ssM_BANF_WRK,ssWERKS,X))) | ~ssSingleRole(singleRoleEntry(Y,authObj(ssM_BANF_EKG,ssEKGRP,Z))) | ~ssSingleRole(singleRoleEntry(U,authObj(ssM_BANF_BSA,ssBSART,V))) | ~ssHolds(ssMUELLER,Y) | ~ssHolds(ssMUELLER,U)),
% 1.05/0.67 inference(resolution,[],['43','4'])).
% 1.05/0.67 cnf('45', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_WRK,ssWERKS,Y))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_BSA,ssBSART,U))) | ~ssSingleRole(singleRoleEntry(V,authObj(ssM_BANF_EKG,ssEKGRP,W))) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Z) | ~ssHolds(ssMUELLER,V)),
% 1.05/0.67 inference(resolution,[],['44','6'])).
% 1.05/0.67 cnf('46', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_EKG,ssEKGRP,Y))) | ~ssSingleRole(singleRoleEntry(Z,authObj(ssM_BANF_BSA,ssBSART,U))) | ~ssHolds(ssMUELLER,X) | ~ssHolds(ssMUELLER,Z)),
% 1.05/0.67 inference(resolution,[then_simplify],['45','8','9'])).
% 1.05/0.67 cnf('47', plain, (~ssSingleRole(singleRoleEntry(X,authObj(ssM_BANF_BSA,ssBSART,Y))) | ~ssHolds(ssMUELLER,X)),
% 1.05/0.67 inference(resolution,[then_simplify],['46','19','9'])).
% 1.05/0.67 cnf('48', plain, ($false),
% 1.05/0.67 inference(resolution,[then_simplify],['47','17','9'])).
% 1.05/0.67
% 1.05/0.67 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.05/0.67
% 1.05/0.67 run 11 fork 2 statistics:
% 1.05/0.67 ----------------------------------
% 1.05/0.67 this run seconds: 0.024001
% 1.05/0.67 total seconds: 0.167476
% 1.05/0.67 stat_given_used: 209
% 1.05/0.67 stat_given_used_at_endgame: 0
% 1.05/0.67 stat_given_candidates: 338
% 1.05/0.67 stat_given_candidates_at_endgame: 0
% 1.05/0.67 stat_given_candidates_h: 0
% 1.05/0.67 stat_binres_derived_cl: 398
% 1.05/0.67 stat_binres_derived_cl_h: 0
% 1.05/0.67 stat_factor_derived_cl: 3
% 1.05/0.67 stat_para_derived_cl: 0
% 1.05/0.67 stat_tautologies_discarded: 0
% 1.05/0.67 stat_forward_subsumed: 0
% 1.05/0.67 stat_derived_cut: 27
% 1.05/0.67 stat_derived_rewritten: 0
% 1.05/0.67 stat_weight_discarded_building: 0
% 1.05/0.67 stat_weight_discarded_cl: 0
% 1.05/0.67 stat_internlimit_discarded_cl: 0
% 1.05/0.67 stat_simplified: 0 simplified 0 derived 0 given
% 1.05/0.67 stat_kept_cl: 400
% 1.05/0.67 stat_built_cl: 1174
% 1.05/0.67 stat_hyperres_partial_cl: 0
% 1.05/0.67 stat_made_rewriters: 0
% 1.05/0.67 stat_backward_subsumed: 0
% 1.05/0.67 stat_propagated_subsumed: 0
% 1.05/0.67 stat_clsubs_attempted: 2698
% 1.05/0.67 stat_clsubs_fact_groundunit_found: 0
% 1.05/0.67 stat_clsubs_rule_groundunit_found: 0
% 1.05/0.67 stat_clsubs_top_meta_attempted: 41881
% 1.05/0.67 stat_clsubs_top_meta_failed: 39183
% 1.05/0.67 stat_clsubs_top_meta_nonpref_attempted: 41881
% 1.05/0.67 stat_clsubs_top_meta_nonpref_succeeded: 15623
% 1.05/0.67 stat_clsubs_top_meta_pref_attempted: 15623
% 1.05/0.67 stat_clsubs_top_meta_pref1_succeeded: 4179
% 1.05/0.67 stat_clsubs_top_meta_pref2_succeeded: 3955
% 1.05/0.67 stat_clsubs_top_meta_pref3_succeeded: 2698
% 1.05/0.67 stat_clsubs_top_meta_pref_succeeded: 2698
% 1.05/0.67 stat_clsubs_meta_attempted: 15831
% 1.05/0.67 stat_clsubs_meta_failed: 6704
% 1.05/0.67 stat_clsubs_predsymbs_attempted: 0
% 1.05/0.67 stat_clsubs_unit_attempted: 3
% 1.05/0.67 stat_clsubs_full_attempted: 2695
% 1.05/0.67 stat_forwardsubs_attempted: 401
% 1.05/0.67 stat_lit_hash_added: 324
% 1.05/0.67 stat_lit_hash_computed: 12111
% 1.05/0.67 stat_lit_hash_match_found: 91
% 1.05/0.67 stat_lit_hash_match_miss: 17392
% 1.05/0.67 stat_lit_hash_cut_ok: 23
% 1.05/0.67 stat_lit_strong_cut_ok: 6
% 1.05/0.67 stat_lit_hash_subsume_ok: 0
% 1.05/0.67 clqueue els 10000000 used 1
% 1.05/0.67 clactive els 10000000 used 388
% 1.05/0.67 clactivesubsume els 10000000 used 1555
% 1.05/0.67 queue_termbuf els 200000000 used 62252
% 1.05/0.67 hyper_termbuf els 100000000 used 1
% 1.05/0.67 active_termbuf els 100000000 used 38386
% 1.05/0.67 varstack els 5000 last used 1
% 1.05/0.67 given_termbuf els 10000000 last used 1
% 1.05/0.67 simplified_termbuf els 10000000 last used 1
% 1.05/0.67 derived_termbuf els 10000000 last used 22
% 1.05/0.67 wr_mallocs: 6005
% 1.05/0.67 wr_callocs: 21
% 1.05/0.67 wr_reallocs: 44
% 1.05/0.67 wr_frees: 4
% 1.05/0.67 wr_malloc_bytes: 4162792212
% 1.05/0.67 wr_calloc_bytes: 112065536
% 1.05/0.67 wr_realloc_bytes: 64376
% 1.05/0.67 wr_realloc_freebytes: 0
% 1.05/0.67 ----------------------------------
%------------------------------------------------------------------------------