%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : SYN445+1 : TPTP v8.1.2. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n023.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 : Fri Sep 1 03:01:49 EDT 2023
% Result : Theorem 108.08s 14.14s
% Output : CNFRefutation 108.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN445+1 : TPTP v8.1.2. Released v2.1.0.
% 0.11/0.12 % Command : gkc %s
% 0.13/0.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Sat Aug 26 18:19:41 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.13/0.38
% 0.13/0.38 input clause set summed statistics:
% 0.13/0.38 ----------------------------------
% 0.13/0.38 in_clause_count: 180
% 0.13/0.38 in_rule_clause_count: 180
% 0.13/0.38 in_fact_clause_count: 0
% 0.13/0.38 in_answer_clause_count: 0
% 0.13/0.38 in_ground_clause_count: 127
% 0.13/0.38 in_unit_clause_count: 0
% 0.13/0.38 in_horn_clause_count: 122
% 0.13/0.38 in_pos_clause_count: 7
% 0.13/0.38 in_neg_clause_count: 47
% 0.13/0.38 in_poseq_clause_count: 0
% 0.13/0.38 in_negeq_clause_count: 0
% 0.13/0.38 in_unitposeq_clause_count: 0
% 0.13/0.38 in_chain_clause_count: 0
% 0.13/0.38 in_min_length: 2
% 0.13/0.38 in_max_length: 12
% 0.13/0.38 in_min_depth: 1
% 0.13/0.38 in_max_depth: 1
% 0.13/0.38 in_min_size: 4
% 0.13/0.38 in_max_size: 24
% 0.13/0.38 in_min_vars: 0
% 0.13/0.38 in_max_vars: 3
% 0.13/0.38 in_extaxiom_count: 0
% 0.13/0.38 in_axiom_count: 0
% 0.13/0.38 in_assumption_count: 0
% 0.13/0.38 in_goal_count: 180
% 0.13/0.38 in_neg_goal_count: 47
% 0.13/0.38 in_pos_goal_count: 7
% 0.13/0.38 in_posunit_goal_count: 0
% 0.13/0.38
% 0.13/0.38 auto guide:
% 0.13/0.38 -----------
% 0.13/0.38 {
% 0.13/0.38 "print":1,
% 0.13/0.38 "print_level": 15,
% 0.13/0.38 "max_size": 0,
% 0.13/0.38 "max_depth": 0,
% 0.13/0.38 "max_length": 0,
% 0.13/0.38 "max_dseconds": 0,
% 0.13/0.38 "equality":0,
% 0.13/0.38 "runs":[
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.13/0.38 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.13/0.38 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.13/0.38 {"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.13/0.38 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.13/0.38 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.13/0.38 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.13/0.38 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.13/0.38 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.13/0.38
% 0.13/0.38 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.13/0.38 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.13/0.38 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.13/0.38 {"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.13/0.38 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.13/0.38 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.13/0.38 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.13/0.38
% 0.13/0.38 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.13/0.38 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.13/0.38 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.13/0.38 {"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.13/0.38 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.13/0.38 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.13/0.38 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.13/0.38 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.13/0.38
% 0.13/0.38 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.13/0.38 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.13/0.38 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.13/0.38
% 0.13/0.38 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.13/0.38 {"max_dseconds":1250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0}
% 0.13/0.38
% 0.13/0.38 ]}
% 0.13/0.38
% 0.13/0.38
% 0.13/0.38 **** run 1 fork 0 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.13/0.38
% 0.13/0.38 **** run 2 fork 1 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.13/0.38
% 0.13/0.38 **** run 3 fork 2 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.13/0.38
% 0.13/0.38 **** run 4 fork 3 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"sine":5,"strategy":["unit"],"query_preference":0}
% 0.13/0.38
% 0.13/0.38 **** run 5 fork 4 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.13/0.38
% 0.13/0.38 **** run 6 fork 5 starts with strategy
% 0.13/0.38 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.13/0.39
% 0.13/0.39 **** run 8 fork 7 starts with strategy
% 0.13/0.39
% 0.13/0.39 **** run 7 fork 6 starts with strategy
% 0.13/0.39 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}{"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.13/0.39
% 0.19/0.42
% 0.19/0.42 fork 3: search finished without proof.
% 0.19/0.45
% 0.19/0.45 fork 7: search finished without proof.
% 0.19/0.45
% 0.19/0.45 **** run 12 fork 3 starts with strategy
% 0.19/0.45 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 0.19/0.48
% 0.19/0.48 **** run 16 fork 7 starts with strategy
% 0.19/0.48 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 0.19/0.50
% 0.19/0.50 fork 1: search finished without proof.
% 0.19/0.50
% 0.19/0.50 fork 5: search finished without proof.
% 0.19/0.51
% 0.19/0.51 fork 4: search finished without proof.
% 0.19/0.51
% 0.19/0.51 fork 2: search finished without proof.
% 0.19/0.52
% 0.19/0.52 fork 0: search finished without proof.
% 0.19/0.52
% 0.19/0.52 **** run 10 fork 1 starts with strategy
% 0.19/0.52 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.19/0.52
% 0.19/0.52 fork 6: search finished without proof.
% 0.19/0.52
% 0.19/0.52 **** run 14 fork 5 starts with strategy
% 0.19/0.52 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 0.19/0.53
% 0.19/0.53 **** run 13 fork 4 starts with strategy
% 0.19/0.53 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 0.19/0.53
% 0.19/0.53 **** run 11 fork 2 starts with strategy
% 0.19/0.53 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 0.19/0.53
% 0.19/0.53 **** run 9 fork 0 starts with strategy
% 0.19/0.53 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 0.19/0.54
% 0.19/0.54 **** run 15 fork 6 starts with strategy
% 0.19/0.54 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 0.19/0.55
% 0.19/0.55 fork 1: search finished without proof.
% 0.19/0.57
% 0.19/0.57 **** run 18 fork 1 starts with strategy
% 0.19/0.57 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"reverse_clauselist":1}
% 1.62/0.58
% 1.62/0.58
% 1.62/0.58 fork 3: search terminated without proof.
% 1.62/0.60
% 1.62/0.60 fork 7: search finished without proof.
% 1.62/0.60
% 1.62/0.60 **** run 20 fork 3 starts with strategy
% 1.62/0.60 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 1.62/0.60
% 1.62/0.60 fork 1: search finished without proof.
% 1.85/0.61
% 1.85/0.61 **** run 24 fork 7 starts with strategy
% 1.85/0.61 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":1}
% 1.85/0.62
% 1.85/0.62 **** run 26 fork 1 starts with strategy
% 1.85/0.62 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":2,"sine":1}
% 1.85/0.64
% 1.85/0.64 fork 3: search finished without proof.
% 1.85/0.64
% 1.85/0.64 fork 5: search finished without proof.
% 2.14/0.65
% 2.14/0.65
% 2.14/0.65 fork 4: search terminated without proof.
% 2.14/0.66
% 2.14/0.66 **** run 28 fork 3 starts with strategy
% 2.14/0.66 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":2,"query_preference":1}
% 2.14/0.66
% 2.14/0.66 **** run 22 fork 5 starts with strategy
% 2.14/0.66 {"max_dseconds":1,"strategy":["unit"],"query_preference":2}
% 2.14/0.66
% 2.14/0.66
% 2.14/0.66 fork 6: search terminated without proof.
% 2.14/0.67
% 2.14/0.67
% 2.14/0.67 fork 2: search terminated without proof.
% 2.14/0.67
% 2.14/0.67 fork 0: search finished without proof.
% 2.14/0.67
% 2.14/0.67 **** run 21 fork 4 starts with strategy
% 2.14/0.67 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 2.14/0.68
% 2.14/0.68 **** run 23 fork 6 starts with strategy
% 2.14/0.68 {"max_dseconds":1,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 2.14/0.68
% 2.14/0.68 **** run 17 fork 0 starts with strategy
% 2.14/0.68 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"depth_penalty":100}
% 2.14/0.69
% 2.14/0.69 **** run 19 fork 2 starts with strategy
% 2.14/0.69 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":2}
% 2.14/0.70
% 2.14/0.70 fork 5: search finished without proof.
% 2.14/0.72
% 2.14/0.72 fork 4: search finished without proof.
% 2.14/0.72
% 2.14/0.72 **** run 30 fork 5 starts with strategy
% 2.14/0.72 {"max_dseconds":1,"strategy":["query_focus","max_ground_weight"],"query_preference":1}
% 2.84/0.73
% 2.84/0.73
% 2.84/0.73 fork 7: search terminated without proof.
% 2.84/0.74
% 2.84/0.74 **** run 29 fork 4 starts with strategy
% 2.84/0.74
% 2.84/0.74 fork 1: search finished without proof.
% 2.84/0.74 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1}
% 2.84/0.75
% 2.84/0.75 **** run 32 fork 7 starts with strategy
% 2.84/0.75 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":2}
% 2.84/0.75
% 2.84/0.75 **** run 34 fork 1 starts with strategy
% 2.84/0.75 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 2.84/0.77
% 2.84/0.77 fork 4: search finished without proof.
% 2.84/0.78
% 2.84/0.78 fork 3: search finished without proof.
% 3.29/0.79
% 3.29/0.79 **** run 37 fork 4 starts with strategy
% 3.29/0.79 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 3.29/0.79
% 3.29/0.79 fork 7: search finished without proof.
% 3.29/0.80
% 3.29/0.80 **** run 36 fork 3 starts with strategy
% 3.29/0.80 {"weight_select_ratio":20,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 3.29/0.81
% 3.29/0.81 **** run 40 fork 7 starts with strategy
% 3.29/0.81 {"sine":2,"var_weight":70,"repeat_var_weight":70,"max_depth":0,"length_penalty":100,"query_preference":2,"strategy":["unit"],"max_dseconds":1}
% 3.29/0.81
% 3.29/0.81 fork 6: search finished without proof.
% 3.29/0.82
% 3.29/0.82 fork 1: search finished without proof.
% 3.29/0.82
% 3.29/0.82
% 3.29/0.82 fork 2: search terminated without proof.
% 3.29/0.82
% 3.29/0.82
% 3.29/0.82 fork 0: search terminated without proof.
% 3.29/0.83
% 3.29/0.83 **** run 31 fork 6 starts with strategy
% 3.29/0.83 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 3.29/0.83
% 3.29/0.83 **** run 42 fork 1 starts with strategy
% 3.29/0.83 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":1}
% 3.29/0.84
% 3.29/0.84 **** run 27 fork 2 starts with strategy
% 3.29/0.84 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":1,"query_preference":1}
% 3.29/0.84
% 3.29/0.84 **** run 25 fork 0 starts with strategy
% 3.29/0.84 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":2}
% 3.29/0.85
% 3.29/0.85 fork 7: search finished without proof.
% 3.29/0.85
% 3.29/0.85
% 3.29/0.85 fork 5: search terminated without proof.
% 3.89/0.86
% 3.89/0.86 **** run 48 fork 7 starts with strategy
% 3.89/0.86 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 3.89/0.87
% 3.89/0.87 **** run 38 fork 5 starts with strategy
% 3.89/0.87 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 4.24/0.91
% 4.24/0.91
% 4.24/0.91 fork 4: search terminated without proof.
% 4.24/0.92
% 4.24/0.92
% 4.24/0.92 fork 3: search terminated without proof.
% 4.24/0.93
% 4.24/0.93 **** run 45 fork 4 starts with strategy
% 4.24/0.93 {"max_dseconds":1,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 4.24/0.94
% 4.24/0.94 **** run 44 fork 3 starts with strategy
% 4.24/0.94 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":2}
% 4.53/0.96
% 4.53/0.96
% 4.53/0.96 fork 6: search terminated without proof.
% 4.53/0.96
% 4.53/0.96
% 4.53/0.96 fork 1: search terminated without proof.
% 4.53/0.96
% 4.53/0.96 fork 2: search finished without proof.
% 4.53/0.97
% 4.53/0.97 fork 4: search finished without proof.
% 4.53/0.97
% 4.53/0.97 fork 0: search finished without proof.
% 4.53/0.97
% 4.53/0.97 fork 3: search finished without proof.
% 4.53/0.98
% 4.53/0.98 **** run 39 fork 6 starts with strategy
% 4.53/0.98 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":1}
% 4.53/0.98
% 4.53/0.98 **** run 50 fork 1 starts with strategy
% 4.53/0.98 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 4.53/0.98
% 4.53/0.98 **** run 35 fork 2 starts with strategy
% 4.53/0.98 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 4.53/0.98
% 4.53/0.98 **** run 53 fork 4 starts with strategy
% 4.53/0.98 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 4.53/0.99
% 4.53/0.99 **** run 33 fork 0 starts with strategy
% 4.53/0.99 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1,"sine":1}
% 4.53/0.99
% 4.53/0.99 fork 7: search finished without proof.
% 4.53/0.99
% 4.53/0.99 **** run 52 fork 3 starts with strategy
% 4.53/0.99 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 4.53/0.99
% 4.53/0.99
% 4.53/0.99 fork 5: search terminated without proof.
% 4.53/1.01
% 4.53/1.01 **** run 56 fork 7 starts with strategy
% 4.53/1.01 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 4.53/1.01
% 4.53/1.01 **** run 46 fork 5 starts with strategy
% 4.53/1.01 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 4.53/1.01
% 4.53/1.01 fork 1: search finished without proof.
% 4.53/1.02
% 4.53/1.02 fork 2: search finished without proof.
% 4.53/1.02
% 4.53/1.02 fork 0: search finished without proof.
% 5.24/1.03
% 5.24/1.03 **** run 58 fork 1 starts with strategy
% 5.24/1.03 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 5.24/1.03
% 5.24/1.03 **** run 43 fork 2 starts with strategy
% 5.24/1.03 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 5.24/1.04
% 5.24/1.04 **** run 41 fork 0 starts with strategy
% 5.24/1.04 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 5.24/1.05 No candidate clauses found.
% 5.24/1.05
% 5.24/1.05
% 5.24/1.05 fork 5: search terminated without proof.
% 5.24/1.06
% 5.24/1.06 **** run 54 fork 5 starts with strategy
% 5.24/1.06 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 5.65/1.10
% 5.65/1.10
% 5.65/1.10 fork 6: search terminated without proof.
% 5.65/1.12
% 5.65/1.12 **** run 47 fork 6 starts with strategy
% 5.65/1.12 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 5.65/1.16
% 5.65/1.16 fork 2: search finished without proof.
% 6.29/1.17
% 6.29/1.17
% 6.29/1.17 fork 0: search terminated without proof.
% 6.29/1.17
% 6.29/1.17 **** run 51 fork 2 starts with strategy
% 6.29/1.17 {"weight_select_ratio":100,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 6.36/1.18
% 6.36/1.18 **** run 49 fork 0 starts with strategy
% 6.36/1.18 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 6.90/1.24
% 6.90/1.24
% 6.90/1.24 fork 6: search terminated without proof.
% 6.90/1.26
% 6.90/1.26 **** run 55 fork 6 starts with strategy
% 6.90/1.26 {"max_dseconds":10,"sine":5,"strategy":["unit"],"query_preference":0}
% 6.90/1.29
% 6.90/1.29 fork 6: search finished without proof.
% 6.90/1.30
% 6.90/1.30
% 6.90/1.30 fork 2: search terminated without proof.
% 6.90/1.30
% 6.90/1.30
% 6.90/1.30 fork 0: search terminated without proof.
% 6.90/1.31
% 6.90/1.31 **** run 63 fork 6 starts with strategy
% 6.90/1.31 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 6.90/1.32
% 6.90/1.32 **** run 59 fork 2 starts with strategy
% 6.90/1.32 {"max_dseconds":10,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 7.51/1.32
% 7.51/1.32 **** run 57 fork 0 starts with strategy
% 7.51/1.32 {"max_dseconds":10,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 7.51/1.35
% 7.51/1.35 fork 2: search finished without proof.
% 7.51/1.37
% 7.51/1.37 **** run 67 fork 2 starts with strategy
% 7.51/1.37 {"max_dseconds":10,"strategy":["unit"],"query_preference":0}
% 7.95/1.40
% 7.95/1.40 fork 2: search finished without proof.
% 7.95/1.42
% 7.95/1.42 **** run 75 fork 2 starts with strategy
% 7.95/1.42 {"max_dseconds":10,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 8.58/1.46
% 8.58/1.46 fork 2: search finished without proof.
% 8.58/1.47
% 8.58/1.47 **** run 83 fork 2 starts with strategy
% 8.58/1.47 {"max_dseconds":50,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 8.77/1.51
% 8.77/1.51 fork 2: search finished without proof.
% 9.13/1.53
% 9.13/1.53 **** run 91 fork 2 starts with strategy
% 9.13/1.53 {"max_dseconds":50,"strategy":["unit"],"query_preference":0}
% 9.27/1.57
% 9.27/1.57 fork 2: search finished without proof.
% 9.27/1.58
% 9.27/1.58 **** run 99 fork 2 starts with strategy
% 9.27/1.58 {"max_dseconds":50,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 9.88/1.62
% 9.88/1.62 fork 2: search finished without proof.
% 9.88/1.63
% 9.88/1.63 **** run 107 fork 2 starts with strategy
% 9.88/1.63 {"max_dseconds":250,"strategy":["negative_pref"],"query_preference":0}
% 12.58/2.02
% 12.58/2.02 fork 4: search finished without proof.
% 12.58/2.03
% 12.58/2.03 **** run 61 fork 4 starts with strategy
% 12.58/2.03 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 12.58/2.04
% 12.58/2.04
% 12.58/2.04 fork 7: search terminated without proof.
% 13.24/2.07
% 13.24/2.07 **** run 64 fork 7 starts with strategy
% 13.24/2.07 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0}
% 13.24/2.07
% 13.24/2.07 fork 4: search finished without proof.
% 13.24/2.09
% 13.24/2.09 **** run 69 fork 4 starts with strategy
% 13.24/2.09 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 13.24/2.09
% 13.24/2.09
% 13.24/2.09 fork 1: search terminated without proof.
% 13.41/2.10
% 13.41/2.10 fork 3: search finished without proof.
% 13.41/2.11
% 13.41/2.11 **** run 66 fork 1 starts with strategy
% 13.41/2.11 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0}
% 13.69/2.14
% 13.69/2.14 **** run 60 fork 3 starts with strategy
% 13.69/2.14 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 13.69/2.14
% 13.69/2.14 fork 1: search finished without proof.
% 13.69/2.15
% 13.69/2.15 **** run 74 fork 1 starts with strategy
% 13.69/2.15 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"sine":2}
% 13.69/2.19
% 13.69/2.19 fork 1: search finished without proof.
% 13.69/2.20
% 13.69/2.20 **** run 82 fork 1 starts with strategy
% 13.69/2.20 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 14.38/2.23
% 14.38/2.23 fork 5: search finished without proof.
% 14.38/2.25
% 14.38/2.25 **** run 62 fork 5 starts with strategy
% 14.38/2.25 {"max_dseconds":10,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 14.94/2.31
% 14.94/2.31 fork 6: search finished without proof.
% 14.94/2.32
% 14.94/2.32 fork 0: search finished without proof.
% 14.94/2.33
% 14.94/2.33 **** run 71 fork 6 starts with strategy
% 14.94/2.33 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":10}
% 14.94/2.34
% 14.94/2.34 **** run 65 fork 0 starts with strategy
% 14.94/2.34 {"max_dseconds":10,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 21.21/3.10
% 21.21/3.10 fork 7: search finished without proof.
% 21.44/3.11
% 21.44/3.11
% 21.44/3.11 fork 4: search terminated without proof.
% 21.44/3.12
% 21.44/3.12 **** run 72 fork 7 starts with strategy
% 21.44/3.12 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 21.59/3.13
% 21.59/3.13 **** run 77 fork 4 starts with strategy
% 21.59/3.13 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 21.59/3.14
% 21.59/3.14 fork 3: search finished without proof.
% 21.59/3.16
% 21.59/3.16 **** run 68 fork 3 starts with strategy
% 21.59/3.16 {"max_dseconds":10,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 22.26/3.27
% 22.26/3.27
% 22.26/3.27 fork 5: search terminated without proof.
% 22.82/3.29
% 22.82/3.29 **** run 70 fork 5 starts with strategy
% 22.82/3.29 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 22.82/3.34
% 22.82/3.34 fork 0: search finished without proof.
% 22.82/3.35
% 22.82/3.35 **** run 73 fork 0 starts with strategy
% 22.82/3.35 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 22.82/3.36
% 22.82/3.36
% 22.82/3.36 fork 6: search terminated without proof.
% 23.51/3.38
% 23.51/3.38 **** run 79 fork 6 starts with strategy
% 23.51/3.38 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0}
% 29.28/4.15
% 29.28/4.15
% 29.28/4.15 fork 7: search terminated without proof.
% 29.76/4.17
% 29.76/4.17 **** run 80 fork 7 starts with strategy
% 29.76/4.17 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 29.76/4.19
% 29.76/4.19
% 29.76/4.19 fork 4: search terminated without proof.
% 29.76/4.19
% 29.76/4.19
% 29.76/4.19 fork 3: search terminated without proof.
% 29.76/4.20
% 29.76/4.20 **** run 85 fork 4 starts with strategy
% 29.76/4.20 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 29.76/4.20
% 29.76/4.20 **** run 76 fork 3 starts with strategy
% 29.76/4.20 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":3}
% 29.76/4.23 No candidate clauses found.
% 29.76/4.23
% 29.76/4.23
% 29.76/4.23 fork 3: search terminated without proof.
% 29.76/4.24
% 29.76/4.24 fork 4: search finished without proof.
% 29.76/4.25
% 29.76/4.25 **** run 84 fork 3 starts with strategy
% 29.76/4.25 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 29.76/4.25
% 29.76/4.25 **** run 93 fork 4 starts with strategy
% 29.76/4.25 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 30.86/4.32
% 30.86/4.32
% 30.86/4.32 fork 5: search terminated without proof.
% 30.86/4.33
% 30.86/4.33 **** run 78 fork 5 starts with strategy
% 30.86/4.33 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 31.21/4.37
% 31.21/4.37 fork 5: search finished without proof.
% 31.21/4.38
% 31.21/4.38
% 31.21/4.38 fork 0: search terminated without proof.
% 31.21/4.38
% 31.21/4.38 **** run 86 fork 5 starts with strategy
% 31.21/4.38 {"max_dseconds":50,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 31.21/4.40
% 31.21/4.40 **** run 81 fork 0 starts with strategy
% 31.21/4.40 {"max_dseconds":50,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 53.91/7.27
% 53.91/7.27
% 53.91/7.27 fork 1: search terminated without proof.
% 54.32/7.28
% 54.32/7.28 **** run 90 fork 1 starts with strategy
% 54.32/7.28 {"max_dseconds":50,"strategy":["query_focus","unit"],"query_preference":0}
% 54.32/7.31
% 54.32/7.31 fork 1: search finished without proof.
% 54.32/7.33
% 54.32/7.33 **** run 98 fork 1 starts with strategy
% 54.32/7.33 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"sine":2}
% 55.03/7.36
% 55.03/7.36 fork 1: search finished without proof.
% 55.03/7.38
% 55.03/7.38 **** run 106 fork 1 starts with strategy
% 55.03/7.38 {"max_dseconds":250,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 63.51/8.48
% 63.51/8.48
% 63.51/8.48 fork 6: search terminated without proof.
% 63.51/8.49
% 63.51/8.49 **** run 87 fork 6 starts with strategy
% 63.51/8.49 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 68.17/9.06
% 68.17/9.06 fork 3: search finished without proof.
% 68.17/9.08
% 68.17/9.08 **** run 92 fork 3 starts with strategy
% 68.17/9.08 {"max_dseconds":50,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 68.73/9.11
% 68.73/9.11 fork 7: search finished without proof.
% 68.73/9.13
% 68.73/9.13 **** run 88 fork 7 starts with strategy
% 68.73/9.13 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0}
% 70.35/9.32
% 70.35/9.32
% 70.35/9.32 fork 4: search terminated without proof.
% 70.44/9.33
% 70.44/9.33 **** run 101 fork 4 starts with strategy
% 70.44/9.33 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 71.11/9.44
% 71.11/9.44
% 71.11/9.44 fork 5: search terminated without proof.
% 71.11/9.46
% 71.11/9.46 **** run 94 fork 5 starts with strategy
% 71.11/9.46 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":50}
% 71.66/9.52
% 71.66/9.52
% 71.66/9.52 fork 0: search terminated without proof.
% 71.66/9.54
% 71.66/9.54 **** run 89 fork 0 starts with strategy
% 71.66/9.54 {"max_dseconds":50,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 102.97/13.47
% 102.97/13.47 fork 6: search finished without proof.
% 103.43/13.49
% 103.43/13.49 **** run 95 fork 6 starts with strategy
% 103.43/13.49 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":50}
% 108.08/14.14
% 108.08/14.14
% 108.08/14.14 result: proof found
% 108.08/14.14 for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 108.08/14.14 by run 107 fork 2 strategy {"max_dseconds":250,"strategy":["negative_pref"],"query_preference":0}
% 108.08/14.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 108.08/14.14
% 108.08/14.14 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 108.08/14.14 fof('co1_$sk', plain, ((hskp25 | (hskp12 | hskp20)) & ((hskp16 | hskp26) & ((hskp12 | (hskp11 | hskp26)) & ((hskp23 | (hskp15 | hskp6)) & ((hskp24 | (hskp5 | hskp17)) & ((hskp10 | (hskp1 | hskp7)) & ((hskp10 | (hskp27 | hskp29)) & ((hskp28 | ((~c3_1(X1) | (~c2_1(X1) | ~c1_1(X1))) | ~ndr1_0)) & ((hskp21 | (hskp17 | ((~c3_1(X2) | (~c1_1(X2) | ~c0_1(X2))) | ~ndr1_0))) & ((hskp23 | (hskp26 | ((~c2_1(X3) | (~c1_1(X3) | ~c0_1(X3))) | ~ndr1_0))) & ((hskp8 | (hskp6 | ((~c2_1(X4) | (~c1_1(X4) | ~c0_1(X4))) | ~ndr1_0))) & ((hskp25 | (hskp15 | ((~c2_1(X5) | (~c1_1(X5) | c3_1(X5))) | ~ndr1_0))) & ((hskp4 | (((~c3_1(X6) | (~c2_1(X6) | ~c1_1(X6))) | ~ndr1_0) | ((~c2_1(X7) | (~c1_1(X7) | c3_1(X7))) | ~ndr1_0))) & ((hskp11 | (((~c3_1(X8) | (~c2_1(X8) | ~c0_1(X8))) | ~ndr1_0) | ((~c2_1(X9) | (~c0_1(X9) | c3_1(X9))) | ~ndr1_0))) & ((hskp24 | (hskp23 | ((~c1_1(X10) | (~c0_1(X10) | c3_1(X10))) | ~ndr1_0))) & ((hskp4 | (hskp17 | ((~c1_1(X11) | (~c0_1(X11) | c3_1(X11))) | ~ndr1_0))) & ((((~c3_1(X12) | (~c2_1(X12) | ~c0_1(X12))) | ~ndr1_0) | ((~c3_1(X13) | (~c1_1(X13) | c2_1(X13))) | ~ndr1_0)) & ((hskp22 | ((~c1_1(X14) | (c3_1(X14) | c2_1(X14))) | ~ndr1_0)) & ((hskp17 | (((~c3_1(X15) | (~c1_1(X15) | ~c0_1(X15))) | ~ndr1_0) | ((~c1_1(X16) | (c3_1(X16) | c2_1(X16))) | ~ndr1_0))) & ((((~c3_1(X17) | (~c1_1(X17) | ~c0_1(X17))) | ~ndr1_0) | (((~c3_1(X18) | (~c1_1(X18) | c2_1(X18))) | ~ndr1_0) | ((~c1_1(X19) | (c3_1(X19) | c2_1(X19))) | ~ndr1_0))) & ((hskp21 | ((~c0_1(X20) | (c3_1(X20) | c2_1(X20))) | ~ndr1_0)) & ((hskp3 | (hskp27 | ((~c3_1(X21) | (~c2_1(X21) | c1_1(X21))) | ~ndr1_0))) & ((hskp20 | (hskp11 | ((~c2_1(X22) | (~c0_1(X22) | c1_1(X22))) | ~ndr1_0))) & ((hskp12 | (hskp19 | ((~c2_1(X23) | (~c0_1(X23) | c1_1(X23))) | ~ndr1_0))) & ((hskp18 | (hskp17 | ((~c2_1(X24) | (~c0_1(X24) | c1_1(X24))) | ~ndr1_0))) & ((hskp4 | (((~c3_1(X25) | (~c0_1(X25) | c1_1(X25))) | ~ndr1_0) | ((~c2_1(X26) | (~c0_1(X26) | c1_1(X26))) | ~ndr1_0))) & ((hskp16 | (hskp11 | ((~c2_1(X27) | (c3_1(X27) | c1_1(X27))) | ~ndr1_0))) & ((hskp5 | (((~c1_1(X28) | (c3_1(X28) | c2_1(X28))) | ~ndr1_0) | ((~c2_1(X29) | (c3_1(X29) | c1_1(X29))) | ~ndr1_0))) & ((hskp17 | (((~c1_1(X30) | (c3_1(X30) | c2_1(X30))) | ~ndr1_0) | ((~c0_1(X31) | (c3_1(X31) | c1_1(X31))) | ~ndr1_0))) & ((hskp13 | (((~c2_1(X32) | (c3_1(X32) | c1_1(X32))) | ~ndr1_0) | ((~c0_1(X33) | (c3_1(X33) | c1_1(X33))) | ~ndr1_0))) & ((hskp16 | ((~c3_1(X34) | (c2_1(X34) | c1_1(X34))) | ~ndr1_0)) & ((hskp15 | (hskp6 | ((~c3_1(X35) | (c2_1(X35) | c1_1(X35))) | ~ndr1_0))) & ((hskp7 | (((~c1_1(X36) | (~c0_1(X36) | c2_1(X36))) | ~ndr1_0) | ((~c3_1(X37) | (c2_1(X37) | c1_1(X37))) | ~ndr1_0))) & ((hskp14 | (((~c3_1(X38) | (~c1_1(X38) | c2_1(X38))) | ~ndr1_0) | ((~c0_1(X39) | (c2_1(X39) | c1_1(X39))) | ~ndr1_0))) & ((hskp0 | (hskp14 | ((~c3_1(X40) | (~c2_1(X40) | c0_1(X40))) | ~ndr1_0))) & ((hskp3 | (((~c1_1(X41) | (c3_1(X41) | c2_1(X41))) | ~ndr1_0) | ((~c3_1(X42) | (~c2_1(X42) | c0_1(X42))) | ~ndr1_0))) & ((hskp13 | (((~c1_1(X43) | (~c0_1(X43) | c3_1(X43))) | ~ndr1_0) | ((~c2_1(X44) | (~c1_1(X44) | c0_1(X44))) | ~ndr1_0))) & ((hskp12 | (((~c0_1(X45) | (c3_1(X45) | c2_1(X45))) | ~ndr1_0) | ((~c2_1(X46) | (~c1_1(X46) | c0_1(X46))) | ~ndr1_0))) & ((hskp8 | (((~c2_1(X47) | (~c1_1(X47) | c3_1(X47))) | ~ndr1_0) | ((~c2_1(X48) | (c3_1(X48) | c0_1(X48))) | ~ndr1_0))) & ((hskp12 | (((~c3_1(X49) | (~c1_1(X49) | c2_1(X49))) | ~ndr1_0) | ((~c1_1(X50) | (c3_1(X50) | c0_1(X50))) | ~ndr1_0))) & ((hskp11 | (hskp10 | ((~c3_1(X51) | (c2_1(X51) | c0_1(X51))) | ~ndr1_0))) & ((hskp9 | (((~c2_1(X52) | (~c0_1(X52) | c3_1(X52))) | ~ndr1_0) | ((~c3_1(X53) | (c2_1(X53) | c0_1(X53))) | ~ndr1_0))) & ((hskp5 | (hskp8 | ((~c1_1(X54) | (c2_1(X54) | c0_1(X54))) | ~ndr1_0))) & ((hskp4 | (hskp7 | ((~c1_1(X55) | (c2_1(X55) | c0_1(X55))) | ~ndr1_0))) & ((hskp6 | (((~c1_1(X56) | (~c0_1(X56) | c3_1(X56))) | ~ndr1_0) | ((~c1_1(X57) | (c2_1(X57) | c0_1(X57))) | ~ndr1_0))) & ((hskp5 | (((~c3_1(X58) | (~c0_1(X58) | c1_1(X58))) | ~ndr1_0) | ((~c1_1(X59) | (c2_1(X59) | c0_1(X59))) | ~ndr1_0))) & ((hskp4 | (((~c2_1(X60) | (~c0_1(X60) | c1_1(X60))) | ~ndr1_0) | ((~c1_1(X61) | (c2_1(X61) | c0_1(X61))) | ~ndr1_0))) & ((hskp3 | (((~c1_1(X62) | (c3_1(X62) | c0_1(X62))) | ~ndr1_0) | ((~c1_1(X63) | (c2_1(X63) | c0_1(X63))) | ~ndr1_0))) & ((((~c3_1(X64) | (~c1_1(X64) | c0_1(X64))) | ~ndr1_0) | (((~c1_1(X65) | (c3_1(X65) | c0_1(X65))) | ~ndr1_0) | ((~c1_1(X66) | (c2_1(X66) | c0_1(X66))) | ~ndr1_0))) & ((((~c3_1(X67) | (~c2_1(X67) | c1_1(X67))) | ~ndr1_0) | (((~c1_1(X68) | (c2_1(X68) | c0_1(X68))) | ~ndr1_0) | ((c3_1(X69) | (c2_1(X69) | c0_1(X69))) | ~ndr1_0))) & ((hskp0 | (hskp2 | ((~c3_1(X70) | (c1_1(X70) | c0_1(X70))) | ~ndr1_0))) & ((hskp0 | (((~c3_1(X71) | (~c1_1(X71) | c2_1(X71))) | ~ndr1_0) | ((~c3_1(X72) | (c1_1(X72) | c0_1(X72))) | ~ndr1_0))) & ((hskp1 | (((~c3_1(X73) | (~c2_1(X73) | c1_1(X73))) | ~ndr1_0) | ((~c2_1(X74) | (c1_1(X74) | c0_1(X74))) | ~ndr1_0))) & ((((~c2_1(X75) | (~c1_1(X75) | c3_1(X75))) | ~ndr1_0) | (((~c1_1(X76) | (c2_1(X76) | c0_1(X76))) | ~ndr1_0) | ((~c2_1(X77) | (c1_1(X77) | c0_1(X77))) | ~ndr1_0))) & ((((~c2_1(X78) | (~c0_1(X78) | c3_1(X78))) | ~ndr1_0) | (((~c1_1(X79) | (c2_1(X79) | c0_1(X79))) | ~ndr1_0) | ((c3_1(X80) | (c1_1(X80) | c0_1(X80))) | ~ndr1_0))) & ((((~c3_1(X81) | (~c2_1(X81) | c0_1(X81))) | ~ndr1_0) | (((c3_1(X82) | (c2_1(X82) | c0_1(X82))) | ~ndr1_0) | ((c3_1(X83) | (c1_1(X83) | c0_1(X83))) | ~ndr1_0))) & ((hskp0 | (((~c1_1(X84) | (~c0_1(X84) | c2_1(X84))) | ~ndr1_0) | ((c2_1(X85) | (c1_1(X85) | c0_1(X85))) | ~ndr1_0))) & ((((~c3_1(X86) | (~c1_1(X86) | ~c0_1(X86))) | ~ndr1_0) | (((~c2_1(X87) | (~c0_1(X87) | c1_1(X87))) | ~ndr1_0) | ((c2_1(X88) | (c1_1(X88) | c0_1(X88))) | ~ndr1_0))) & ((((~c3_1(X89) | (~c1_1(X89) | c2_1(X89))) | ~ndr1_0) | (((c3_1(X90) | (c2_1(X90) | c1_1(X90))) | ~ndr1_0) | ((c2_1(X91) | (c1_1(X91) | c0_1(X91))) | ~ndr1_0))) & ((((~c2_1(X92) | (~c1_1(X92) | c0_1(X92))) | ~ndr1_0) | (((c3_1(X93) | (c2_1(X93) | c0_1(X93))) | ~ndr1_0) | ((c2_1(X94) | (c1_1(X94) | c0_1(X94))) | ~ndr1_0))) & (((c2_1(a354) & (c1_1(a354) & (c0_1(a354) & ndr1_0))) | ~hskp29) & (((c3_1(a353) & (c2_1(a353) & (c1_1(a353) & ndr1_0))) | ~hskp28) & (((c3_1(a334) & (c2_1(a334) & (c0_1(a334) & ndr1_0))) | ~hskp27) & (((~c3_1(a349) & (~c2_1(a349) & (c0_1(a349) & ndr1_0))) | ~hskp26) & (((~c3_1(a346) & (~c1_1(a346) & (~c0_1(a346) & ndr1_0))) | ~hskp25) & (((~c2_1(a342) & (~c1_1(a342) & (c3_1(a342) & ndr1_0))) | ~hskp24) & (((~c0_1(a341) & (c3_1(a341) & (c2_1(a341) & ndr1_0))) | ~hskp23) & (((~c3_1(a338) & (~c2_1(a338) & (~c1_1(a338) & ndr1_0))) | ~hskp22) & (((~c1_1(a336) & (~c0_1(a336) & (c3_1(a336) & ndr1_0))) | ~hskp21) & (((~c3_1(a333) & (~c2_1(a333) & (c1_1(a333) & ndr1_0))) | ~hskp20) & (((~c3_1(a330) & (c2_1(a330) & (c1_1(a330) & ndr1_0))) | ~hskp19) & (((~c3_1(a329) & (~c0_1(a329) & (c2_1(a329) & ndr1_0))) | ~hskp18) & (((~c3_1(a323) & (c2_1(a323) & (c0_1(a323) & ndr1_0))) | ~hskp17) & (((~c1_1(a321) & (c3_1(a321) & (c2_1(a321) & ndr1_0))) | ~hskp16) & (((~c2_1(a320) & (~c0_1(a320) & (c1_1(a320) & ndr1_0))) | ~hskp15) & (((~c0_1(a315) & (c2_1(a315) & (c1_1(a315) & ndr1_0))) | ~hskp14) & (((~c1_1(a313) & (c3_1(a313) & (c0_1(a313) & ndr1_0))) | ~hskp13) & (((~c2_1(a310) & (~c0_1(a310) & (c3_1(a310) & ndr1_0))) | ~hskp12) & (((~c2_1(a309) & (c3_1(a309) & (c1_1(a309) & ndr1_0))) | ~hskp11) & (((~c0_1(a308) & (c3_1(a308) & (c1_1(a308) & ndr1_0))) | ~hskp10) & (((~c3_1(a307) & (~c1_1(a307) & (c0_1(a307) & ndr1_0))) | ~hskp9) & (((~c1_1(a305) & (~c0_1(a305) & (c2_1(a305) & ndr1_0))) | ~hskp8) & (((~c2_1(a303) & (c1_1(a303) & (c0_1(a303) & ndr1_0))) | ~hskp7) & (((~c2_1(a302) & (~c1_1(a302) & (c0_1(a302) & ndr1_0))) | ~hskp6) & (((~c3_1(a301) & (~c1_1(a301) & (c2_1(a301) & ndr1_0))) | ~hskp5) & (((~c2_1(a300) & (~c1_1(a300) & (~c0_1(a300) & ndr1_0))) | ~hskp4) & (((~c2_1(a299) & (c3_1(a299) & (c0_1(a299) & ndr1_0))) | ~hskp3) & (((~c3_1(a297) & (~c0_1(a297) & (c1_1(a297) & ndr1_0))) | ~hskp2) & (((~c1_1(a295) & (c2_1(a295) & (c0_1(a295) & ndr1_0))) | ~hskp1) & ((~c3_1(a294) & (~c2_1(a294) & (~c0_1(a294) & ndr1_0))) | ~hskp0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 108.08/14.14 inference(negpush_and_skolemize,[],['co1'])).
% 108.08/14.14 fof('co1', conjecture, ~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0 | (((ndr1_0 & ~c0_1(a294)) & ~c2_1(a294)) & ~c3_1(a294))) & (~hskp1 | (((ndr1_0 & c0_1(a295)) & c2_1(a295)) & ~c1_1(a295)))) & (~hskp2 | (((ndr1_0 & c1_1(a297)) & ~c0_1(a297)) & ~c3_1(a297)))) & (~hskp3 | (((ndr1_0 & c0_1(a299)) & c3_1(a299)) & ~c2_1(a299)))) & (~hskp4 | (((ndr1_0 & ~c0_1(a300)) & ~c1_1(a300)) & ~c2_1(a300)))) & (~hskp5 | (((ndr1_0 & c2_1(a301)) & ~c1_1(a301)) & ~c3_1(a301)))) & (~hskp6 | (((ndr1_0 & c0_1(a302)) & ~c1_1(a302)) & ~c2_1(a302)))) & (~hskp7 | (((ndr1_0 & c0_1(a303)) & c1_1(a303)) & ~c2_1(a303)))) & (~hskp8 | (((ndr1_0 & c2_1(a305)) & ~c0_1(a305)) & ~c1_1(a305)))) & (~hskp9 | (((ndr1_0 & c0_1(a307)) & ~c1_1(a307)) & ~c3_1(a307)))) & (~hskp10 | (((ndr1_0 & c1_1(a308)) & c3_1(a308)) & ~c0_1(a308)))) & (~hskp11 | (((ndr1_0 & c1_1(a309)) & c3_1(a309)) & ~c2_1(a309)))) & (~hskp12 | (((ndr1_0 & c3_1(a310)) & ~c0_1(a310)) & ~c2_1(a310)))) & (~hskp13 | (((ndr1_0 & c0_1(a313)) & c3_1(a313)) & ~c1_1(a313)))) & (~hskp14 | (((ndr1_0 & c1_1(a315)) & c2_1(a315)) & ~c0_1(a315)))) & (~hskp15 | (((ndr1_0 & c1_1(a320)) & ~c0_1(a320)) & ~c2_1(a320)))) & (~hskp16 | (((ndr1_0 & c2_1(a321)) & c3_1(a321)) & ~c1_1(a321)))) & (~hskp17 | (((ndr1_0 & c0_1(a323)) & c2_1(a323)) & ~c3_1(a323)))) & (~hskp18 | (((ndr1_0 & c2_1(a329)) & ~c0_1(a329)) & ~c3_1(a329)))) & (~hskp19 | (((ndr1_0 & c1_1(a330)) & c2_1(a330)) & ~c3_1(a330)))) & (~hskp20 | (((ndr1_0 & c1_1(a333)) & ~c2_1(a333)) & ~c3_1(a333)))) & (~hskp21 | (((ndr1_0 & c3_1(a336)) & ~c0_1(a336)) & ~c1_1(a336)))) & (~hskp22 | (((ndr1_0 & ~c1_1(a338)) & ~c2_1(a338)) & ~c3_1(a338)))) & (~hskp23 | (((ndr1_0 & c2_1(a341)) & c3_1(a341)) & ~c0_1(a341)))) & (~hskp24 | (((ndr1_0 & c3_1(a342)) & ~c1_1(a342)) & ~c2_1(a342)))) & (~hskp25 | (((ndr1_0 & ~c0_1(a346)) & ~c1_1(a346)) & ~c3_1(a346)))) & (~hskp26 | (((ndr1_0 & c0_1(a349)) & ~c2_1(a349)) & ~c3_1(a349)))) & (~hskp27 | (((ndr1_0 & c0_1(a334)) & c2_1(a334)) & c3_1(a334)))) & (~hskp28 | (((ndr1_0 & c1_1(a353)) & c2_1(a353)) & c3_1(a353)))) & (~hskp29 | (((ndr1_0 & c0_1(a354)) & c1_1(a354)) & c2_1(a354)))) & (((! [U] : (ndr1_0 => ((c0_1(U) | c1_1(U)) | c2_1(U)))) | (! [V] : (ndr1_0 => ((c0_1(V) | c2_1(V)) | c3_1(V))))) | (! [W] : (ndr1_0 => ((c0_1(W) | ~c1_1(W)) | ~c2_1(W)))))) & (((! [X] : (ndr1_0 => ((c0_1(X) | c1_1(X)) | c2_1(X)))) | (! [Y] : (ndr1_0 => ((c1_1(Y) | c2_1(Y)) | c3_1(Y))))) | (! [Z] : (ndr1_0 => ((c2_1(Z) | ~c1_1(Z)) | ~c3_1(Z)))))) & (((! [X1] : (ndr1_0 => ((c0_1(X1) | c1_1(X1)) | c2_1(X1)))) | (! [X2] : (ndr1_0 => ((c1_1(X2) | ~c0_1(X2)) | ~c2_1(X2))))) | (! [X3] : (ndr1_0 => ((~c0_1(X3) | ~c1_1(X3)) | ~c3_1(X3)))))) & (((! [X4] : (ndr1_0 => ((c0_1(X4) | c1_1(X4)) | c2_1(X4)))) | (! [X5] : (ndr1_0 => ((c2_1(X5) | ~c0_1(X5)) | ~c1_1(X5))))) | hskp0)) & (((! [X6] : (ndr1_0 => ((c0_1(X6) | c1_1(X6)) | c3_1(X6)))) | (! [X7] : (ndr1_0 => ((c0_1(X7) | c2_1(X7)) | c3_1(X7))))) | (! [X8] : (ndr1_0 => ((c0_1(X8) | ~c2_1(X8)) | ~c3_1(X8)))))) & (((! [X9] : (ndr1_0 => ((c0_1(X9) | c1_1(X9)) | c3_1(X9)))) | (! [X10] : (ndr1_0 => ((c0_1(X10) | c2_1(X10)) | ~c1_1(X10))))) | (! [X11] : (ndr1_0 => ((c3_1(X11) | ~c0_1(X11)) | ~c2_1(X11)))))) & (((! [X12] : (ndr1_0 => ((c0_1(X12) | c1_1(X12)) | ~c2_1(X12)))) | (! [X13] : (ndr1_0 => ((c0_1(X13) | c2_1(X13)) | ~c1_1(X13))))) | (! [X14] : (ndr1_0 => ((c3_1(X14) | ~c1_1(X14)) | ~c2_1(X14)))))) & (((! [X15] : (ndr1_0 => ((c0_1(X15) | c1_1(X15)) | ~c2_1(X15)))) | (! [X16] : (ndr1_0 => ((c1_1(X16) | ~c2_1(X16)) | ~c3_1(X16))))) | hskp1)) & (((! [X17] : (ndr1_0 => ((c0_1(X17) | c1_1(X17)) | ~c3_1(X17)))) | (! [X18] : (ndr1_0 => ((c2_1(X18) | ~c1_1(X18)) | ~c3_1(X18))))) | hskp0)) & (((! [X19] : (ndr1_0 => ((c0_1(X19) | c1_1(X19)) | ~c3_1(X19)))) | hskp2) | hskp0)) & (((! [X20] : (ndr1_0 => ((c0_1(X20) | c2_1(X20)) | c3_1(X20)))) | (! [X21] : (ndr1_0 => ((c0_1(X21) | c2_1(X21)) | ~c1_1(X21))))) | (! [X22] : (ndr1_0 => ((c1_1(X22) | ~c2_1(X22)) | ~c3_1(X22)))))) & (((! [X23] : (ndr1_0 => ((c0_1(X23) | c2_1(X23)) | ~c1_1(X23)))) | (! [X24] : (ndr1_0 => ((c0_1(X24) | c3_1(X24)) | ~c1_1(X24))))) | (! [X25] : (ndr1_0 => ((c0_1(X25) | ~c1_1(X25)) | ~c3_1(X25)))))) & (((! [X26] : (ndr1_0 => ((c0_1(X26) | c2_1(X26)) | ~c1_1(X26)))) | (! [X27] : (ndr1_0 => ((c0_1(X27) | c3_1(X27)) | ~c1_1(X27))))) | hskp3)) & (((! [X28] : (ndr1_0 => ((c0_1(X28) | c2_1(X28)) | ~c1_1(X28)))) | (! [X29] : (ndr1_0 => ((c1_1(X29) | ~c0_1(X29)) | ~c2_1(X29))))) | hskp4)) & (((! [X30] : (ndr1_0 => ((c0_1(X30) | c2_1(X30)) | ~c1_1(X30)))) | (! [X31] : (ndr1_0 => ((c1_1(X31) | ~c0_1(X31)) | ~c3_1(X31))))) | hskp5)) & (((! [X32] : (ndr1_0 => ((c0_1(X32) | c2_1(X32)) | ~c1_1(X32)))) | (! [X33] : (ndr1_0 => ((c3_1(X33) | ~c0_1(X33)) | ~c1_1(X33))))) | hskp6)) & (((! [X34] : (ndr1_0 => ((c0_1(X34) | c2_1(X34)) | ~c1_1(X34)))) | hskp7) | hskp4)) & (((! [X35] : (ndr1_0 => ((c0_1(X35) | c2_1(X35)) | ~c1_1(X35)))) | hskp8) | hskp5)) & (((! [X36] : (ndr1_0 => ((c0_1(X36) | c2_1(X36)) | ~c3_1(X36)))) | (! [X37] : (ndr1_0 => ((c3_1(X37) | ~c0_1(X37)) | ~c2_1(X37))))) | hskp9)) & (((! [X38] : (ndr1_0 => ((c0_1(X38) | c2_1(X38)) | ~c3_1(X38)))) | hskp10) | hskp11)) & (((! [X39] : (ndr1_0 => ((c0_1(X39) | c3_1(X39)) | ~c1_1(X39)))) | (! [X40] : (ndr1_0 => ((c2_1(X40) | ~c1_1(X40)) | ~c3_1(X40))))) | hskp12)) & (((! [X41] : (ndr1_0 => ((c0_1(X41) | c3_1(X41)) | ~c2_1(X41)))) | (! [X42] : (ndr1_0 => ((c3_1(X42) | ~c1_1(X42)) | ~c2_1(X42))))) | hskp8)) & (((! [X43] : (ndr1_0 => ((c0_1(X43) | ~c1_1(X43)) | ~c2_1(X43)))) | (! [X44] : (ndr1_0 => ((c2_1(X44) | c3_1(X44)) | ~c0_1(X44))))) | hskp12)) & (((! [X45] : (ndr1_0 => ((c0_1(X45) | ~c1_1(X45)) | ~c2_1(X45)))) | (! [X46] : (ndr1_0 => ((c3_1(X46) | ~c0_1(X46)) | ~c1_1(X46))))) | hskp13)) & (((! [X47] : (ndr1_0 => ((c0_1(X47) | ~c2_1(X47)) | ~c3_1(X47)))) | (! [X48] : (ndr1_0 => ((c2_1(X48) | c3_1(X48)) | ~c1_1(X48))))) | hskp3)) & (((! [X49] : (ndr1_0 => ((c0_1(X49) | ~c2_1(X49)) | ~c3_1(X49)))) | hskp14) | hskp0)) & (((! [X50] : (ndr1_0 => ((c1_1(X50) | c2_1(X50)) | ~c0_1(X50)))) | (! [X51] : (ndr1_0 => ((c2_1(X51) | ~c1_1(X51)) | ~c3_1(X51))))) | hskp14)) & (((! [X52] : (ndr1_0 => ((c1_1(X52) | c2_1(X52)) | ~c3_1(X52)))) | (! [X53] : (ndr1_0 => ((c2_1(X53) | ~c0_1(X53)) | ~c1_1(X53))))) | hskp7)) & (((! [X54] : (ndr1_0 => ((c1_1(X54) | c2_1(X54)) | ~c3_1(X54)))) | hskp6) | hskp15)) & ((! [X55] : (ndr1_0 => ((c1_1(X55) | c2_1(X55)) | ~c3_1(X55)))) | hskp16)) & (((! [X56] : (ndr1_0 => ((c1_1(X56) | c3_1(X56)) | ~c0_1(X56)))) | (! [X57] : (ndr1_0 => ((c1_1(X57) | c3_1(X57)) | ~c2_1(X57))))) | hskp13)) & (((! [X58] : (ndr1_0 => ((c1_1(X58) | c3_1(X58)) | ~c0_1(X58)))) | (! [X59] : (ndr1_0 => ((c2_1(X59) | c3_1(X59)) | ~c1_1(X59))))) | hskp17)) & (((! [X60] : (ndr1_0 => ((c1_1(X60) | c3_1(X60)) | ~c2_1(X60)))) | (! [X61] : (ndr1_0 => ((c2_1(X61) | c3_1(X61)) | ~c1_1(X61))))) | hskp5)) & (((! [X62] : (ndr1_0 => ((c1_1(X62) | c3_1(X62)) | ~c2_1(X62)))) | hskp11) | hskp16)) & (((! [X63] : (ndr1_0 => ((c1_1(X63) | ~c0_1(X63)) | ~c2_1(X63)))) | (! [X64] : (ndr1_0 => ((c1_1(X64) | ~c0_1(X64)) | ~c3_1(X64))))) | hskp4)) & (((! [X65] : (ndr1_0 => ((c1_1(X65) | ~c0_1(X65)) | ~c2_1(X65)))) | hskp17) | hskp18)) & (((! [X66] : (ndr1_0 => ((c1_1(X66) | ~c0_1(X66)) | ~c2_1(X66)))) | hskp19) | hskp12)) & (((! [X67] : (ndr1_0 => ((c1_1(X67) | ~c0_1(X67)) | ~c2_1(X67)))) | hskp11) | hskp20)) & (((! [X68] : (ndr1_0 => ((c1_1(X68) | ~c2_1(X68)) | ~c3_1(X68)))) | hskp27) | hskp3)) & ((! [X69] : (ndr1_0 => ((c2_1(X69) | c3_1(X69)) | ~c0_1(X69)))) | hskp21)) & (((! [X70] : (ndr1_0 => ((c2_1(X70) | c3_1(X70)) | ~c1_1(X70)))) | (! [X71] : (ndr1_0 => ((c2_1(X71) | ~c1_1(X71)) | ~c3_1(X71))))) | (! [X72] : (ndr1_0 => ((~c0_1(X72) | ~c1_1(X72)) | ~c3_1(X72)))))) & (((! [X73] : (ndr1_0 => ((c2_1(X73) | c3_1(X73)) | ~c1_1(X73)))) | (! [X74] : (ndr1_0 => ((~c0_1(X74) | ~c1_1(X74)) | ~c3_1(X74))))) | hskp17)) & ((! [X75] : (ndr1_0 => ((c2_1(X75) | c3_1(X75)) | ~c1_1(X75)))) | hskp22)) & ((! [X76] : (ndr1_0 => ((c2_1(X76) | ~c1_1(X76)) | ~c3_1(X76)))) | (! [X77] : (ndr1_0 => ((~c0_1(X77) | ~c2_1(X77)) | ~c3_1(X77)))))) & (((! [X78] : (ndr1_0 => ((c3_1(X78) | ~c0_1(X78)) | ~c1_1(X78)))) | hskp17) | hskp4)) & (((! [X79] : (ndr1_0 => ((c3_1(X79) | ~c0_1(X79)) | ~c1_1(X79)))) | hskp23) | hskp24)) & (((! [X80] : (ndr1_0 => ((c3_1(X80) | ~c0_1(X80)) | ~c2_1(X80)))) | (! [X81] : (ndr1_0 => ((~c0_1(X81) | ~c2_1(X81)) | ~c3_1(X81))))) | hskp11)) & (((! [X82] : (ndr1_0 => ((c3_1(X82) | ~c1_1(X82)) | ~c2_1(X82)))) | (! [X83] : (ndr1_0 => ((~c1_1(X83) | ~c2_1(X83)) | ~c3_1(X83))))) | hskp4)) & (((! [X84] : (ndr1_0 => ((c3_1(X84) | ~c1_1(X84)) | ~c2_1(X84)))) | hskp15) | hskp25)) & (((! [X85] : (ndr1_0 => ((~c0_1(X85) | ~c1_1(X85)) | ~c2_1(X85)))) | hskp6) | hskp8)) & (((! [X86] : (ndr1_0 => ((~c0_1(X86) | ~c1_1(X86)) | ~c2_1(X86)))) | hskp26) | hskp23)) & (((! [X87] : (ndr1_0 => ((~c0_1(X87) | ~c1_1(X87)) | ~c3_1(X87)))) | hskp17) | hskp21)) & ((! [X88] : (ndr1_0 => ((~c1_1(X88) | ~c2_1(X88)) | ~c3_1(X88)))) | hskp28)) & ((hskp29 | hskp27) | hskp10)) & ((hskp7 | hskp1) | hskp10)) & ((hskp17 | hskp5) | hskp24)) & ((hskp6 | hskp15) | hskp23)) & ((hskp26 | hskp11) | hskp12)) & (hskp26 | hskp16)) & ((hskp20 | hskp12) | hskp25)),
% 108.08/14.14 input).
% 108.08/14.14 cnf('1', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c2_1(X0) | ~c3_1(X0) | c0_1(X2) | c0_1(X1) | c0_1(X0) | c1_1(X2) | c2_1(X1) | c3_1(X2) | c3_1(X1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('2', plain, (~$pr(hskp26) | $pr(ndr1_0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('3', plain, ($pr(hskp16) | $pr(hskp26)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('4', plain, ($pr(ndr1_0) | $pr(hskp16)),
% 108.08/14.14 inference(resolution,[],['2','3'])).
% 108.08/14.14 cnf('5', plain, (~$pr(hskp16) | $pr(ndr1_0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('6', plain, ($pr(ndr1_0)),
% 108.08/14.14 inference(simplify,[],['4','5'])).
% 108.08/14.14 cnf('7', plain, (~c2_1(X) | ~c3_1(X) | c0_1(Y) | c0_1(Z) | c0_1(X) | c1_1(Y) | c2_1(Z) | c3_1(Y) | c3_1(Z)),
% 108.08/14.14 inference(simplify,[then_simplify],['1','6','6','6'])).
% 108.08/14.14 cnf('8', plain, (~c2_1(X) | ~c3_1(X) | c0_1(Y) | c0_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['7'])).
% 108.08/14.14 cnf('9', plain, (~$pr(hskp26) | c0_1(a349)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('10', plain, ($pr(hskp16) | c0_1(a349)),
% 108.08/14.14 inference(resolution,[],['9','3'])).
% 108.08/14.14 cnf('11', plain, (~$pr(ndr1_0) | $pr(hskp21) | ~c0_1(X0) | c2_1(X0) | c3_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('12', plain, ($pr(hskp21) | ~c0_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['11','6'])).
% 108.08/14.14 cnf('13', plain, (c3_1(a349) | $pr(hskp16) | c2_1(a349) | $pr(hskp21)),
% 108.08/14.14 inference(resolution,[],['10','12'])).
% 108.08/14.14 cnf('14', plain, (~c2_1(a349) | ~$pr(hskp26)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('15', plain, (c3_1(a349) | $pr(hskp16) | $pr(hskp21) | ~$pr(hskp26)),
% 108.08/14.14 inference(resolution,[],['13','14'])).
% 108.08/14.14 cnf('16', plain, (~c3_1(a349) | ~$pr(hskp26)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('17', plain, (~$pr(hskp26) | $pr(hskp16) | $pr(hskp21)),
% 108.08/14.14 inference(simplify,[],['15','16'])).
% 108.08/14.14 cnf('18', plain, ($pr(hskp16) | $pr(hskp26)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('19', plain, ($pr(hskp16) | $pr(hskp21)),
% 108.08/14.14 inference(simplify,[],['17','18'])).
% 108.08/14.14 cnf('20', plain, (~$pr(hskp21) | c3_1(a336)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('21', plain, ($pr(hskp16) | c3_1(a336)),
% 108.08/14.14 inference(resolution,[],['19','20'])).
% 108.08/14.14 cnf('22', plain, (~$pr(ndr1_0) | $pr(hskp16) | ~c3_1(X0) | c1_1(X0) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('23', plain, ($pr(hskp16) | ~c3_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(simplify,[],['22','6'])).
% 108.08/14.14 cnf('24', plain, ($pr(hskp16) | c1_1(a336) | c2_1(a336)),
% 108.08/14.14 inference(resolution,[],['21','23'])).
% 108.08/14.14 cnf('25', plain, (~c1_1(a336) | ~$pr(hskp21)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('26', plain, (~$pr(hskp21) | $pr(hskp16) | c2_1(a336)),
% 108.08/14.14 inference(resolution,[],['24','25'])).
% 108.08/14.14 cnf('27', plain, ($pr(hskp16) | c2_1(a336)),
% 108.08/14.14 inference(resolution,[],['26','19'])).
% 108.08/14.14 cnf('28', plain, (~c3_1(a336) | c0_1(a336) | $pr(hskp16) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['8','27'])).
% 108.08/14.14 cnf('29', plain, ($pr(hskp16) | c3_1(a336)),
% 108.08/14.14 inference(resolution,[],['19','20'])).
% 108.08/14.14 cnf('30', plain, (c0_1(a336) | $pr(hskp16) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['28','29'])).
% 108.08/14.14 cnf('31', plain, (~c0_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('32', plain, (c0_1(a336) | $pr(hskp16) | c1_1(a300) | c2_1(a300) | c3_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['30','31'])).
% 108.08/14.14 cnf('33', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp1) | ~c2_1(X1) | ~c2_1(X0) | ~c3_1(X0) | c0_1(X1) | c1_1(X1) | c1_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('34', plain, ($pr(hskp1) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(X) | c1_1(X) | c1_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['33','6','6'])).
% 108.08/14.14 cnf('35', plain, ($pr(hskp1) | ~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 108.08/14.14 inference(factorization,[],['34'])).
% 108.08/14.14 cnf('36', plain, (~c3_1(a336) | c0_1(a336) | $pr(hskp16) | c1_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['35','27'])).
% 108.08/14.14 cnf('37', plain, (c0_1(a336) | $pr(hskp16) | c1_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(simplify,[],['36','29'])).
% 108.08/14.14 cnf('38', plain, (~c0_1(a336) | ~$pr(hskp21)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('39', plain, ($pr(hskp16) | c1_1(a336) | $pr(hskp1) | ~$pr(hskp21)),
% 108.08/14.14 inference(resolution,[],['37','38'])).
% 108.08/14.14 cnf('40', plain, (~c1_1(a336) | ~$pr(hskp21)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('41', plain, (~$pr(hskp21) | $pr(hskp16) | $pr(hskp1)),
% 108.08/14.14 inference(simplify,[],['39','40'])).
% 108.08/14.14 cnf('42', plain, ($pr(hskp16) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['41','19'])).
% 108.08/14.14 cnf('43', plain, (~$pr(hskp1) | c0_1(a295)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('44', plain, ($pr(hskp16) | c0_1(a295)),
% 108.08/14.14 inference(resolution,[],['42','43'])).
% 108.08/14.14 cnf('45', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp4) | ~c0_1(X1) | ~c0_1(X0) | ~c2_1(X1) | ~c3_1(X0) | c1_1(X1) | c1_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('46', plain, ($pr(hskp4) | ~c0_1(X) | ~c0_1(Y) | ~c2_1(X) | ~c3_1(Y) | c1_1(X) | c1_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['45','6','6'])).
% 108.08/14.14 cnf('47', plain, ($pr(hskp4) | ~c0_1(X) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(factorization,[],['46'])).
% 108.08/14.14 cnf('48', plain, (~c2_1(a295) | ~c3_1(a295) | c1_1(a295) | $pr(hskp16) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['44','47'])).
% 108.08/14.14 cnf('49', plain, (~$pr(hskp1) | c2_1(a295)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('50', plain, (c2_1(a295) | $pr(hskp16)),
% 108.08/14.14 inference(resolution,[],['42','49'])).
% 108.08/14.14 cnf('51', plain, (~c3_1(a295) | c1_1(a295) | $pr(hskp16) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['48','50'])).
% 108.08/14.14 cnf('52', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp13) | ~c0_1(X1) | ~c2_1(X0) | c1_1(X1) | c1_1(X0) | c3_1(X1) | c3_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('53', plain, ($pr(hskp13) | ~c0_1(X) | ~c2_1(Y) | c1_1(X) | c1_1(Y) | c3_1(X) | c3_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['52','6','6'])).
% 108.08/14.14 cnf('54', plain, ($pr(hskp13) | ~c0_1(X) | ~c2_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(factorization,[],['53'])).
% 108.08/14.14 cnf('55', plain, (~c2_1(a295) | c1_1(a295) | $pr(hskp16) | $pr(hskp13) | c3_1(a295)),
% 108.08/14.14 inference(resolution,[],['44','54'])).
% 108.08/14.14 cnf('56', plain, (c1_1(a295) | $pr(hskp16) | $pr(hskp13) | c3_1(a295)),
% 108.08/14.14 inference(simplify,[],['55','50'])).
% 108.08/14.14 cnf('57', plain, (~c1_1(a295) | ~$pr(hskp1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('58', plain, ($pr(hskp16) | $pr(hskp13) | c3_1(a295) | ~$pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['56','57'])).
% 108.08/14.14 cnf('59', plain, ($pr(hskp16) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['41','19'])).
% 108.08/14.14 cnf('60', plain, ($pr(hskp16) | $pr(hskp13) | c3_1(a295)),
% 108.08/14.14 inference(simplify,[],['58','59'])).
% 108.08/14.14 cnf('61', plain, (c1_1(a295) | $pr(hskp16) | $pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['51','60'])).
% 108.08/14.14 cnf('62', plain, ($pr(hskp16) | $pr(hskp13) | $pr(hskp4) | ~$pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['61','57'])).
% 108.08/14.14 cnf('63', plain, ($pr(hskp16) | $pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['62','59'])).
% 108.08/14.14 cnf('64', plain, (~$pr(hskp13) | c0_1(a313)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('65', plain, ($pr(hskp16) | c0_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['63','64'])).
% 108.08/14.14 cnf('66', plain, (~c2_1(a313) | ~c3_1(a313) | $pr(hskp16) | c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['65','47'])).
% 108.08/14.14 cnf('67', plain, (~$pr(hskp13) | c3_1(a313)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('68', plain, ($pr(hskp16) | c3_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['63','67'])).
% 108.08/14.14 cnf('69', plain, ($pr(hskp16) | c1_1(a313) | c2_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['68','23'])).
% 108.08/14.14 cnf('70', plain, (~$pr(hskp13) | ~c1_1(a313)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('71', plain, (~c1_1(a313) | $pr(hskp16) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['63','70'])).
% 108.08/14.14 cnf('72', plain, ($pr(hskp16) | c2_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['69','71'])).
% 108.08/14.14 cnf('73', plain, (~c3_1(a313) | $pr(hskp16) | c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['66','72'])).
% 108.08/14.14 cnf('74', plain, ($pr(hskp16) | c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['73','68'])).
% 108.08/14.14 cnf('75', plain, ($pr(hskp16) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['74','71'])).
% 108.08/14.14 cnf('76', plain, (c0_1(a336) | $pr(hskp16) | c3_1(a300) | c1_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(simplify,[],['32','75'])).
% 108.08/14.14 cnf('77', plain, ($pr(hskp16) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['74','71'])).
% 108.08/14.14 cnf('78', plain, (~$pr(hskp4) | ~c2_1(a300)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('79', plain, (~c2_1(a300) | $pr(hskp16)),
% 108.08/14.14 inference(resolution,[],['77','78'])).
% 108.08/14.14 cnf('80', plain, (c0_1(a336) | $pr(hskp16) | c3_1(a300) | c1_1(a300)),
% 108.08/14.14 inference(simplify,[],['76','79'])).
% 108.08/14.14 cnf('81', plain, (~$pr(hskp21) | $pr(hskp16) | c3_1(a300) | c1_1(a300)),
% 108.08/14.14 inference(resolution,[],['80','38'])).
% 108.08/14.14 cnf('82', plain, ($pr(hskp16) | c3_1(a300) | c1_1(a300)),
% 108.08/14.14 inference(resolution,[],['81','19'])).
% 108.08/14.14 cnf('83', plain, (~c1_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('84', plain, ($pr(hskp16) | c3_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['82','83'])).
% 108.08/14.14 cnf('85', plain, ($pr(hskp16) | c3_1(a300)),
% 108.08/14.14 inference(simplify,[],['84','75'])).
% 108.08/14.14 cnf('86', plain, ($pr(hskp16) | c1_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['85','23'])).
% 108.08/14.14 cnf('87', plain, ($pr(hskp16) | c1_1(a300)),
% 108.08/14.14 inference(simplify,[],['86','79'])).
% 108.08/14.14 cnf('88', plain, ($pr(hskp16) | ~$pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['87','83'])).
% 108.08/14.14 cnf('89', plain, ($pr(hskp16)),
% 108.08/14.14 inference(simplify,[],['88','75'])).
% 108.08/14.14 cnf('90', plain, (~$pr(hskp16) | c2_1(a321)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('91', plain, (c2_1(a321)),
% 108.08/14.14 inference(resolution,[],['89','90'])).
% 108.08/14.14 cnf('92', plain, (~$pr(hskp16) | c3_1(a321)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('93', plain, (c3_1(a321)),
% 108.08/14.14 inference(resolution,[],['89','92'])).
% 108.08/14.14 cnf('94', plain, (~$pr(hskp16) | ~c1_1(a321)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('95', plain, (~c1_1(a321)),
% 108.08/14.14 inference(resolution,[],['89','94'])).
% 108.08/14.14 cnf('96', plain, (c0_1(a321) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[then_simplify],['91','35','93','95'])).
% 108.08/14.14 cnf('97', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c0_1(X0) | ~c1_1(X1) | ~c2_1(X0) | ~c3_1(X1) | ~c3_1(X0) | c2_1(X1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('98', plain, (~c0_1(X) | ~c1_1(Y) | ~c2_1(X) | ~c3_1(Y) | ~c3_1(X) | c2_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['97','6','6'])).
% 108.08/14.14 cnf('99', plain, (c2_1(a321)),
% 108.08/14.14 inference(resolution,[],['89','90'])).
% 108.08/14.14 cnf('100', plain, ($pr(hskp1) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['96','98','99','93'])).
% 108.08/14.14 cnf('101', plain, ($pr(hskp10) | $pr(hskp1) | $pr(hskp7)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('102', plain, (~$pr(hskp7) | c1_1(a303)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('103', plain, ($pr(hskp10) | c1_1(a303) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['101','102'])).
% 108.08/14.14 cnf('104', plain, (~c3_1(a303) | $pr(hskp10) | $pr(hskp1) | c2_1(a303)),
% 108.08/14.14 inference(resolution,[],['100','103'])).
% 108.08/14.14 cnf('105', plain, (~$pr(hskp7) | c0_1(a303)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('106', plain, ($pr(hskp10) | c0_1(a303) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['101','105'])).
% 108.08/14.14 cnf('107', plain, ($pr(hskp10) | c3_1(a303) | $pr(hskp21) | $pr(hskp1) | c2_1(a303)),
% 108.08/14.14 inference(resolution,[],['106','12'])).
% 108.08/14.14 cnf('108', plain, (~$pr(hskp7) | ~c2_1(a303)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('109', plain, (~c2_1(a303) | $pr(hskp10) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['101','108'])).
% 108.08/14.14 cnf('110', plain, ($pr(hskp10) | c3_1(a303) | $pr(hskp21) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['107','109'])).
% 108.08/14.14 cnf('111', plain, ($pr(hskp10) | $pr(hskp21) | $pr(hskp1) | c2_1(a303)),
% 108.08/14.14 inference(resolution,[],['104','110'])).
% 108.08/14.14 cnf('112', plain, ($pr(hskp10) | $pr(hskp21) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['111','109'])).
% 108.08/14.14 cnf('113', plain, ($pr(hskp10) | c3_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['112','20'])).
% 108.08/14.14 cnf('114', plain, (~$pr(ndr1_0) | $pr(hskp11) | $pr(hskp10) | ~c3_1(X0) | c0_1(X0) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('115', plain, ($pr(hskp11) | $pr(hskp10) | ~c3_1(X) | c0_1(X) | c2_1(X)),
% 108.08/14.14 inference(simplify,[],['114','6'])).
% 108.08/14.14 cnf('116', plain, (c0_1(a336) | $pr(hskp11) | $pr(hskp10) | c2_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['113','115'])).
% 108.08/14.14 cnf('117', plain, (~$pr(hskp21) | $pr(hskp11) | $pr(hskp10) | c2_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['116','38'])).
% 108.08/14.14 cnf('118', plain, ($pr(hskp11) | $pr(hskp10) | c2_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['117','112'])).
% 108.08/14.14 cnf('119', plain, (~c3_1(a336) | c0_1(a336) | $pr(hskp11) | $pr(hskp10) | c1_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['118','35'])).
% 108.08/14.14 cnf('120', plain, (c0_1(a336) | $pr(hskp11) | $pr(hskp10) | c1_1(a336) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['119','113'])).
% 108.08/14.14 cnf('121', plain, ($pr(hskp11) | $pr(hskp10) | c1_1(a336) | $pr(hskp1) | ~$pr(hskp21)),
% 108.08/14.14 inference(resolution,[],['120','38'])).
% 108.08/14.14 cnf('122', plain, (~$pr(hskp21) | $pr(hskp11) | $pr(hskp10) | $pr(hskp1)),
% 108.08/14.14 inference(simplify,[],['121','40'])).
% 108.08/14.14 cnf('123', plain, ($pr(hskp11) | $pr(hskp10) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['122','112'])).
% 108.08/14.14 cnf('124', plain, ($pr(hskp11) | $pr(hskp10) | c0_1(a295)),
% 108.08/14.14 inference(resolution,[],['123','43'])).
% 108.08/14.14 cnf('125', plain, (~c2_1(a295) | c1_1(a295) | $pr(hskp11) | $pr(hskp10) | $pr(hskp4) | ~c0_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(resolution,[],['124','46'])).
% 108.08/14.14 cnf('126', plain, (c2_1(a295) | $pr(hskp11) | $pr(hskp10)),
% 108.08/14.14 inference(resolution,[],['123','49'])).
% 108.08/14.14 cnf('127', plain, (c1_1(a295) | $pr(hskp11) | $pr(hskp10) | $pr(hskp4) | ~c0_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(resolution,[],['125','126'])).
% 108.08/14.14 cnf('128', plain, (c0_1(a321) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['91','8','93'])).
% 108.08/14.14 cnf('129', plain, ($pr(hskp4) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['128','47','99','93','95'])).
% 108.08/14.14 cnf('130', plain, (~c0_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('131', plain, (~$pr(hskp0) | c1_1(a294) | c2_1(a294) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['129','130'])).
% 108.08/14.14 cnf('132', plain, (~c2_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('133', plain, (~$pr(hskp0) | c1_1(a294) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['131','132'])).
% 108.08/14.14 cnf('134', plain, (~$pr(ndr1_0) | $pr(hskp14) | $pr(hskp0) | ~c2_1(X0) | ~c3_1(X0) | c0_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('135', plain, ($pr(hskp14) | $pr(hskp0) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 108.08/14.14 inference(simplify,[],['134','6'])).
% 108.08/14.14 cnf('136', plain, ($pr(hskp14) | c0_1(a321) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['91','135','93'])).
% 108.08/14.14 cnf('137', plain, ($pr(hskp14) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['136','47','99','93','95'])).
% 108.08/14.14 cnf('138', plain, (c1_1(a294) | $pr(hskp14) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['133','137'])).
% 108.08/14.14 cnf('139', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c1_1(X1) | ~c2_1(X0) | ~c3_1(X0) | c0_1(X2) | c0_1(X1) | c1_1(X0) | c2_1(X2) | c2_1(X1) | c3_1(X2)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('140', plain, (~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Z) | c0_1(X) | c1_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Z)),
% 108.08/14.14 inference(simplify,[then_simplify],['139','6','6','6'])).
% 108.08/14.14 cnf('141', plain, (~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(X) | c1_1(Y) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(factorization,[],['140'])).
% 108.08/14.14 cnf('142', plain, (c2_1(a294) | $pr(hskp14) | c0_1(a294) | c3_1(a294) | $pr(hskp4) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(resolution,[],['138','141'])).
% 108.08/14.14 cnf('143', plain, (c2_1(a294) | $pr(hskp14) | c0_1(a294) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['142','91','93','95'])).
% 108.08/14.14 cnf('144', plain, (c2_1(a294) | $pr(hskp14) | c3_1(a294) | $pr(hskp4) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['143','130'])).
% 108.08/14.14 cnf('145', plain, (~$pr(hskp0) | $pr(hskp14) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['144','132'])).
% 108.08/14.14 cnf('146', plain, (~$pr(ndr1_0) | $pr(hskp11) | $pr(hskp20) | ~c0_1(X0) | ~c2_1(X0) | c1_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('147', plain, ($pr(hskp11) | $pr(hskp20) | ~c0_1(X) | ~c2_1(X) | c1_1(X)),
% 108.08/14.14 inference(simplify,[],['146','6'])).
% 108.08/14.14 cnf('148', plain, ($pr(hskp11) | $pr(hskp20) | $pr(hskp1)),
% 108.08/14.14 inference(resolution,[then_simplify],['96','147','99','95'])).
% 108.08/14.14 cnf('149', plain, ($pr(hskp11) | c0_1(a295) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['148','43'])).
% 108.08/14.14 cnf('150', plain, (~c2_1(a295) | c1_1(a295) | $pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['149','147'])).
% 108.08/14.14 cnf('151', plain, (c2_1(a295) | $pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['148','49'])).
% 108.08/14.14 cnf('152', plain, (c1_1(a295) | $pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['150','151'])).
% 108.08/14.14 cnf('153', plain, (~$pr(hskp1) | $pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['152','57'])).
% 108.08/14.14 cnf('154', plain, ($pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['153','148'])).
% 108.08/14.14 cnf('155', plain, (~$pr(hskp11) | c1_1(a309)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('156', plain, ($pr(hskp20) | c1_1(a309)),
% 108.08/14.14 inference(resolution,[],['154','155'])).
% 108.08/14.14 cnf('157', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp0) | ~c1_1(X0) | ~c3_1(X1) | ~c3_1(X0) | c0_1(X1) | c1_1(X1) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('158', plain, ($pr(hskp0) | ~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['157','6','6'])).
% 108.08/14.14 cnf('159', plain, (~c3_1(a309) | c2_1(a309) | $pr(hskp20) | $pr(hskp0) | ~c3_1(X3) | c0_1(X3) | c1_1(X3)),
% 108.08/14.14 inference(resolution,[],['156','158'])).
% 108.08/14.14 cnf('160', plain, (~$pr(hskp11) | c3_1(a309)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('161', plain, (c3_1(a309) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['154','160'])).
% 108.08/14.14 cnf('162', plain, (c2_1(a309) | $pr(hskp20) | $pr(hskp0) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 108.08/14.14 inference(simplify,[],['159','161'])).
% 108.08/14.14 cnf('163', plain, (c3_1(a321)),
% 108.08/14.14 inference(resolution,[],['89','92'])).
% 108.08/14.14 cnf('164', plain, (c2_1(a309) | c0_1(a321) | $pr(hskp20) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['162','163','95'])).
% 108.08/14.14 cnf('165', plain, (c2_1(a309) | $pr(hskp20) | $pr(hskp0) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['164','98','99','93'])).
% 108.08/14.14 cnf('166', plain, (~c3_1(a309) | c2_1(a309) | $pr(hskp20) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['165','156'])).
% 108.08/14.14 cnf('167', plain, (c2_1(a309) | $pr(hskp20) | $pr(hskp0)),
% 108.08/14.14 inference(simplify,[],['166','161'])).
% 108.08/14.14 cnf('168', plain, (~c2_1(a309) | ~$pr(hskp11)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('169', plain, ($pr(hskp20) | $pr(hskp0) | ~$pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['167','168'])).
% 108.08/14.14 cnf('170', plain, ($pr(hskp11) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['153','148'])).
% 108.08/14.14 cnf('171', plain, ($pr(hskp20) | $pr(hskp0)),
% 108.08/14.14 inference(simplify,[],['169','170'])).
% 108.08/14.14 cnf('172', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c1_1(X0) | ~c3_1(X0) | c0_1(X2) | c1_1(X2) | c1_1(X1) | c2_1(X2) | c2_1(X1) | c2_1(X0) | c3_1(X1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('173', plain, (~c1_1(X) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c1_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Z)),
% 108.08/14.14 inference(simplify,[then_simplify],['172','6','6','6'])).
% 108.08/14.14 cnf('174', plain, (~c1_1(X) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['173'])).
% 108.08/14.14 cnf('175', plain, (~c3_1(a309) | c2_1(a309) | $pr(hskp20) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['156','174'])).
% 108.08/14.14 cnf('176', plain, (c2_1(a309) | $pr(hskp20) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['175','161'])).
% 108.08/14.14 cnf('177', plain, (~$pr(hskp0) | c2_1(a309) | c1_1(a294) | c2_1(a294) | c3_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['176','130'])).
% 108.08/14.14 cnf('178', plain, (~$pr(hskp0) | c2_1(a309) | c1_1(a294) | c3_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['177','132'])).
% 108.08/14.14 cnf('179', plain, (c2_1(a309) | c1_1(a294) | c3_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['171','178'])).
% 108.08/14.14 cnf('180', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c1_1(X2) | ~c1_1(X1) | ~c1_1(X0) | ~c3_1(X0) | c0_1(X2) | c0_1(X1) | c0_1(X0) | c2_1(X2) | c3_1(X1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('181', plain, (~c1_1(X) | ~c1_1(Y) | ~c1_1(Z) | ~c3_1(Z) | c0_1(X) | c0_1(Y) | c0_1(Z) | c2_1(X) | c3_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['180','6','6','6'])).
% 108.08/14.14 cnf('182', plain, (~c1_1(X) | ~c1_1(Y) | ~c3_1(X) | c0_1(X) | c0_1(Y) | c2_1(X) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['181'])).
% 108.08/14.14 cnf('183', plain, (~c3_1(a309) | c2_1(a309) | c0_1(a309) | $pr(hskp20) | ~c1_1(X3) | c0_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['156','182'])).
% 108.08/14.14 cnf('184', plain, (c2_1(a309) | c0_1(a309) | $pr(hskp20) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['183','161'])).
% 108.08/14.14 cnf('185', plain, (c2_1(a309) | c0_1(a309) | c0_1(a294) | c3_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['179','184'])).
% 108.08/14.14 cnf('186', plain, (c2_1(a309) | c0_1(a309) | c3_1(a294) | $pr(hskp20) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['185','130'])).
% 108.08/14.14 cnf('187', plain, (~c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('188', plain, (~$pr(hskp0) | c2_1(a309) | c0_1(a309) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['186','187'])).
% 108.08/14.14 cnf('189', plain, ($pr(hskp20) | $pr(hskp0)),
% 108.08/14.14 inference(simplify,[],['169','170'])).
% 108.08/14.14 cnf('190', plain, (c2_1(a309) | c0_1(a309) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['188','189'])).
% 108.08/14.14 cnf('191', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c0_1(X0) | ~c1_1(X2) | ~c1_1(X1) | ~c1_1(X0) | ~c3_1(X1) | ~c3_1(X0) | c2_1(X2) | c2_1(X1) | c3_1(X2)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('192', plain, (~c0_1(X) | ~c1_1(Y) | ~c1_1(Z) | ~c1_1(X) | ~c3_1(Z) | ~c3_1(X) | c2_1(Y) | c2_1(Z) | c3_1(Y)),
% 108.08/14.14 inference(simplify,[then_simplify],['191','6','6','6'])).
% 108.08/14.14 cnf('193', plain, (~c0_1(X) | ~c1_1(Y) | ~c1_1(X) | ~c3_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['192'])).
% 108.08/14.14 cnf('194', plain, (~c3_1(a309) | ~c1_1(a309) | c2_1(a309) | $pr(hskp20) | ~c1_1(X3) | c2_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['190','193'])).
% 108.08/14.14 cnf('195', plain, (~c1_1(a309) | c2_1(a309) | $pr(hskp20) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['194','161'])).
% 108.08/14.14 cnf('196', plain, (c2_1(a309) | $pr(hskp20) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['195','156'])).
% 108.08/14.14 cnf('197', plain, (c0_1(a321) | c0_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X) | c3_1(X) | c3_1(Y)),
% 108.08/14.14 inference(resolution,[then_simplify],['91','7','93'])).
% 108.08/14.14 cnf('198', plain, (~$pr(hskp0) | c2_1(a294) | c3_1(a294) | c0_1(a321) | c0_1(X3) | c1_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['197','130'])).
% 108.08/14.14 cnf('199', plain, (~$pr(hskp0) | c3_1(a294) | c0_1(a321) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['198','132'])).
% 108.08/14.14 cnf('200', plain, (c3_1(a294) | c0_1(a321) | $pr(hskp20) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['199','171'])).
% 108.08/14.14 cnf('201', plain, (c3_1(a294) | c0_1(a321) | $pr(hskp20) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['200','130'])).
% 108.08/14.14 cnf('202', plain, (~$pr(hskp0) | c1_1(a294) | c0_1(a321) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['201','187'])).
% 108.08/14.14 cnf('203', plain, (c1_1(a294) | c0_1(a321) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['202','189'])).
% 108.08/14.14 cnf('204', plain, (c1_1(a294) | $pr(hskp20) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['203','98','99','93'])).
% 108.08/14.14 cnf('205', plain, (~c3_1(a309) | c2_1(a309) | c1_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['204','156'])).
% 108.08/14.14 cnf('206', plain, (c2_1(a309) | c1_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['205','161'])).
% 108.08/14.14 cnf('207', plain, (c2_1(a309) | c2_1(a294) | c3_1(a294) | $pr(hskp20)),
% 108.08/14.14 inference(resolution,[],['196','206'])).
% 108.08/14.14 cnf('208', plain, (~c2_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('209', plain, (c2_1(a309) | c3_1(a294) | $pr(hskp20) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['207','208'])).
% 108.08/14.14 cnf('210', plain, (~$pr(hskp0) | c2_1(a309) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['209','187'])).
% 108.08/14.14 cnf('211', plain, (c2_1(a309) | $pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['210','189'])).
% 108.08/14.14 cnf('212', plain, ($pr(hskp20) | ~$pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['211','168'])).
% 108.08/14.14 cnf('213', plain, ($pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['212','170'])).
% 108.08/14.14 cnf('214', plain, (~$pr(hskp20) | c1_1(a333)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('215', plain, (c1_1(a333)),
% 108.08/14.14 inference(resolution,[],['213','214'])).
% 108.08/14.14 cnf('216', plain, (c0_1(a333) | c3_1(a333) | c2_1(a333) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(resolution,[],['215','141'])).
% 108.08/14.14 cnf('217', plain, (c0_1(a333) | c3_1(a333) | c2_1(a333)),
% 108.08/14.14 inference(resolution,[then_simplify],['216','91','93','95'])).
% 108.08/14.14 cnf('218', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp0) | ~c0_1(X0) | ~c1_1(X0) | c0_1(X1) | c1_1(X1) | c2_1(X1) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('219', plain, ($pr(hskp0) | ~c0_1(X) | ~c1_1(X) | c0_1(Y) | c1_1(Y) | c2_1(Y) | c2_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['218','6','6'])).
% 108.08/14.14 cnf('220', plain, (c1_1(a333)),
% 108.08/14.14 inference(resolution,[],['213','214'])).
% 108.08/14.14 cnf('221', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp0) | c0_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['217','219','220'])).
% 108.08/14.14 cnf('222', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp21)),
% 108.08/14.14 inference(resolution,[],['217','12'])).
% 108.08/14.14 cnf('223', plain, (~c2_1(a333) | ~$pr(hskp20)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('224', plain, ($pr(hskp20)),
% 108.08/14.14 inference(simplify,[],['212','170'])).
% 108.08/14.14 cnf('225', plain, (c3_1(a333) | $pr(hskp21)),
% 108.08/14.14 inference(resolution,[then_simplify],['222','223','224'])).
% 108.08/14.14 cnf('226', plain, (~c3_1(a333) | ~$pr(hskp20)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('227', plain, ($pr(hskp21)),
% 108.08/14.14 inference(resolution,[then_simplify],['225','226','224'])).
% 108.08/14.14 cnf('228', plain, (c3_1(a333) | c1_1(a336) | c2_1(a333) | c2_1(a336) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['221','38','227'])).
% 108.08/14.14 cnf('229', plain, (c3_1(a333) | c2_1(a333) | c2_1(a336) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['228','25','227'])).
% 108.08/14.14 cnf('230', plain, (c3_1(a333) | c2_1(a336) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['229','223','224'])).
% 108.08/14.14 cnf('231', plain, ($pr(hskp21)),
% 108.08/14.14 inference(resolution,[then_simplify],['225','226','224'])).
% 108.08/14.14 cnf('232', plain, (c3_1(a336)),
% 108.08/14.14 inference(resolution,[],['231','20'])).
% 108.08/14.14 cnf('233', plain, (c0_1(a336) | $pr(hskp14) | c3_1(a333) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['230','135','232'])).
% 108.08/14.14 cnf('234', plain, ($pr(hskp14) | c3_1(a333) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['233','38','227'])).
% 108.08/14.14 cnf('235', plain, ($pr(hskp14) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['234','226','224'])).
% 108.08/14.14 cnf('236', plain, ($pr(hskp14) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['145','235'])).
% 108.08/14.14 cnf('237', plain, (~c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('238', plain, ($pr(hskp14) | $pr(hskp4) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['236','237'])).
% 108.08/14.14 cnf('239', plain, ($pr(hskp14) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['238','235'])).
% 108.08/14.14 cnf('240', plain, (~$pr(hskp14) | c1_1(a315)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('241', plain, (c1_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['239','240'])).
% 108.08/14.14 cnf('242', plain, (~$pr(ndr1_0) | $pr(hskp0) | $pr(hskp2) | ~c3_1(X0) | c0_1(X0) | c1_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('243', plain, ($pr(hskp0) | $pr(hskp2) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 108.08/14.14 inference(simplify,[],['242','6'])).
% 108.08/14.14 cnf('244', plain, (c0_1(a321) | $pr(hskp0) | $pr(hskp2)),
% 108.08/14.14 inference(resolution,[then_simplify],['163','243','95'])).
% 108.08/14.14 cnf('245', plain, ($pr(hskp0) | $pr(hskp2) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['244','47','99','93','95'])).
% 108.08/14.14 cnf('246', plain, (~$pr(hskp2) | c1_1(a297)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('247', plain, (c1_1(a297) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['245','246'])).
% 108.08/14.14 cnf('248', plain, (c2_1(a297) | c0_1(a297) | c3_1(a297) | $pr(hskp0) | $pr(hskp4) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 108.08/14.14 inference(resolution,[],['247','141'])).
% 108.08/14.14 cnf('249', plain, (c2_1(a297) | c0_1(a297) | c3_1(a297) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['248','91','93','95'])).
% 108.08/14.14 cnf('250', plain, (~c0_1(a297) | ~$pr(hskp2)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('251', plain, (c2_1(a297) | c3_1(a297) | $pr(hskp0) | $pr(hskp4) | ~$pr(hskp2)),
% 108.08/14.14 inference(resolution,[],['249','250'])).
% 108.08/14.14 cnf('252', plain, (~c3_1(a297) | ~$pr(hskp2)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('253', plain, (~$pr(hskp2) | c2_1(a297) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['251','252'])).
% 108.08/14.14 cnf('254', plain, (c3_1(a336)),
% 108.08/14.14 inference(resolution,[],['231','20'])).
% 108.08/14.14 cnf('255', plain, (c0_1(a336) | c1_1(a336) | $pr(hskp0) | $pr(hskp2)),
% 108.08/14.14 inference(resolution,[],['254','243'])).
% 108.08/14.14 cnf('256', plain, (c1_1(a336) | $pr(hskp0) | $pr(hskp2)),
% 108.08/14.14 inference(resolution,[then_simplify],['255','38','227'])).
% 108.08/14.14 cnf('257', plain, ($pr(hskp0) | $pr(hskp2)),
% 108.08/14.14 inference(resolution,[then_simplify],['256','25','227'])).
% 108.08/14.14 cnf('258', plain, (c2_1(a297) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['253','257'])).
% 108.08/14.14 cnf('259', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp13) | ~c0_1(X0) | ~c1_1(X1) | ~c1_1(X0) | ~c2_1(X1) | c0_1(X1) | c3_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('260', plain, ($pr(hskp13) | ~c0_1(X) | ~c1_1(Y) | ~c1_1(X) | ~c2_1(Y) | c0_1(Y) | c3_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['259','6','6'])).
% 108.08/14.14 cnf('261', plain, ($pr(hskp13) | c3_1(a333) | c2_1(a333) | ~c1_1(X) | ~c2_1(X) | c0_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['217','260','220'])).
% 108.08/14.14 cnf('262', plain, ($pr(hskp0) | $pr(hskp2)),
% 108.08/14.14 inference(resolution,[then_simplify],['256','25','227'])).
% 108.08/14.14 cnf('263', plain, (c1_1(a297) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['262','246'])).
% 108.08/14.14 cnf('264', plain, (~c2_1(a297) | $pr(hskp13) | c3_1(a333) | c0_1(a297) | c2_1(a333) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['261','263'])).
% 108.08/14.14 cnf('265', plain, ($pr(hskp13) | c3_1(a333) | c0_1(a297) | c2_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['258','264'])).
% 108.08/14.14 cnf('266', plain, ($pr(hskp13) | c3_1(a333) | c2_1(a333) | $pr(hskp0) | $pr(hskp4) | ~$pr(hskp2)),
% 108.08/14.14 inference(resolution,[],['265','250'])).
% 108.08/14.14 cnf('267', plain, ($pr(hskp13) | c3_1(a333) | c2_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['266','257'])).
% 108.08/14.14 cnf('268', plain, ($pr(hskp13) | c3_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['267','223','224'])).
% 108.08/14.14 cnf('269', plain, ($pr(hskp13) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['268','226','224'])).
% 108.08/14.14 cnf('270', plain, ($pr(hskp4) | c0_1(X) | c0_1(Y) | c1_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 108.08/14.14 inference(resolution,[then_simplify],['197','47','99','93','95'])).
% 108.08/14.14 cnf('271', plain, (~$pr(hskp0) | c2_1(a294) | c3_1(a294) | $pr(hskp4) | c0_1(X3) | c1_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['270','130'])).
% 108.08/14.14 cnf('272', plain, (~$pr(hskp0) | c3_1(a294) | $pr(hskp4) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['271','132'])).
% 108.08/14.14 cnf('273', plain, ($pr(hskp13) | c3_1(a294) | $pr(hskp4) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['269','272'])).
% 108.08/14.14 cnf('274', plain, ($pr(hskp13) | c3_1(a294) | $pr(hskp4) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['273','130'])).
% 108.08/14.14 cnf('275', plain, (~$pr(hskp0) | c1_1(a294) | $pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['274','187'])).
% 108.08/14.14 cnf('276', plain, (c1_1(a294) | $pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['275','269'])).
% 108.08/14.14 cnf('277', plain, (~$pr(ndr1_0) | $pr(hskp4) | $pr(hskp7) | ~c1_1(X0) | c0_1(X0) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('278', plain, ($pr(hskp4) | $pr(hskp7) | ~c1_1(X) | c0_1(X) | c2_1(X)),
% 108.08/14.14 inference(simplify,[],['277','6'])).
% 108.08/14.14 cnf('279', plain, (c2_1(a294) | $pr(hskp13) | c0_1(a294) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['276','278'])).
% 108.08/14.14 cnf('280', plain, (c2_1(a294) | $pr(hskp13) | $pr(hskp4) | $pr(hskp7) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['279','130'])).
% 108.08/14.14 cnf('281', plain, (~$pr(hskp0) | $pr(hskp13) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['280','132'])).
% 108.08/14.14 cnf('282', plain, ($pr(hskp13) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['281','269'])).
% 108.08/14.14 cnf('283', plain, (c0_1(a313) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['282','64'])).
% 108.08/14.14 cnf('284', plain, (~c2_1(a313) | ~c3_1(a313) | c1_1(a313) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['283','47'])).
% 108.08/14.14 cnf('285', plain, (c3_1(a313) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['282','67'])).
% 108.08/14.14 cnf('286', plain, (c0_1(a333) | c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['215','278'])).
% 108.08/14.14 cnf('287', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp7) | ~c0_1(X0) | ~c1_1(X0) | ~c3_1(X1) | c1_1(X1) | c2_1(X1) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('288', plain, ($pr(hskp7) | ~c0_1(X) | ~c1_1(X) | ~c3_1(Y) | c1_1(Y) | c2_1(Y) | c2_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['287','6','6'])).
% 108.08/14.14 cnf('289', plain, (c2_1(a333) | $pr(hskp4) | $pr(hskp7) | ~c3_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['286','288','220'])).
% 108.08/14.14 cnf('290', plain, (c1_1(a313) | c2_1(a313) | c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['285','289'])).
% 108.08/14.14 cnf('291', plain, (~c1_1(a313) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['282','70'])).
% 108.08/14.14 cnf('292', plain, (c2_1(a313) | c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['290','291'])).
% 108.08/14.14 cnf('293', plain, (~c3_1(a313) | c1_1(a313) | c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['284','292'])).
% 108.08/14.14 cnf('294', plain, (c1_1(a313) | c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['293','285'])).
% 108.08/14.14 cnf('295', plain, (c2_1(a333) | $pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['294','291'])).
% 108.08/14.14 cnf('296', plain, ($pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['295','223','224'])).
% 108.08/14.14 cnf('297', plain, (~$pr(hskp4) | c3_1(a300) | c0_1(a321) | c1_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['128','31'])).
% 108.08/14.14 cnf('298', plain, (~c1_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('299', plain, (~$pr(hskp4) | c3_1(a300) | c0_1(a321) | c2_1(a300)),
% 108.08/14.14 inference(simplify,[],['297','298'])).
% 108.08/14.14 cnf('300', plain, (c3_1(a300) | c0_1(a321) | $pr(hskp7) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['296','299'])).
% 108.08/14.14 cnf('301', plain, (~c2_1(a300) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['296','78'])).
% 108.08/14.14 cnf('302', plain, (c3_1(a300) | c0_1(a321) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['300','301'])).
% 108.08/14.14 cnf('303', plain, (c3_1(a300) | $pr(hskp7) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['302','98','99','93'])).
% 108.08/14.14 cnf('304', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp7) | ~c3_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['217','288','220'])).
% 108.08/14.14 cnf('305', plain, (c3_1(a333) | c1_1(a336) | c2_1(a333) | c2_1(a336) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['304','254'])).
% 108.08/14.14 cnf('306', plain, (c3_1(a333) | c2_1(a333) | c2_1(a336) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['305','25','227'])).
% 108.08/14.14 cnf('307', plain, (c3_1(a333) | c2_1(a336) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['306','223','224'])).
% 108.08/14.14 cnf('308', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp3) | ~c1_1(X0) | ~c2_1(X1) | ~c3_1(X1) | c0_1(X1) | c2_1(X0) | c3_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('309', plain, ($pr(hskp3) | ~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['308','6','6'])).
% 108.08/14.14 cnf('310', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp3) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 108.08/14.14 inference(resolution,[],['215','309'])).
% 108.08/14.14 cnf('311', plain, (c0_1(a336) | c3_1(a333) | c2_1(a333) | $pr(hskp3) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['307','310','232'])).
% 108.08/14.14 cnf('312', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp3) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['311','38','227'])).
% 108.08/14.14 cnf('313', plain, (c3_1(a333) | $pr(hskp3) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['312','223','224'])).
% 108.08/14.14 cnf('314', plain, ($pr(hskp3) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['313','226','224'])).
% 108.08/14.14 cnf('315', plain, (~$pr(hskp3) | c3_1(a299)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('316', plain, (c3_1(a299) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['314','315'])).
% 108.08/14.14 cnf('317', plain, (c1_1(a299) | c2_1(a299) | c3_1(a333) | c2_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['316','304'])).
% 108.08/14.14 cnf('318', plain, (~c3_1(a299) | c2_1(a299) | c3_1(a333) | c3_1(a300) | c2_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['303','317'])).
% 108.08/14.14 cnf('319', plain, (c3_1(a299) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[],['314','315'])).
% 108.08/14.14 cnf('320', plain, (c2_1(a299) | c3_1(a333) | c3_1(a300) | c2_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['318','319'])).
% 108.08/14.14 cnf('321', plain, (~c2_1(a299) | ~$pr(hskp3)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('322', plain, (c3_1(a333) | c3_1(a300) | c2_1(a333) | $pr(hskp7) | ~$pr(hskp3)),
% 108.08/14.14 inference(resolution,[],['320','321'])).
% 108.08/14.14 cnf('323', plain, ($pr(hskp3) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['313','226','224'])).
% 108.08/14.14 cnf('324', plain, (c3_1(a333) | c3_1(a300) | c2_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['322','323'])).
% 108.08/14.14 cnf('325', plain, (c3_1(a333) | c3_1(a300) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['324','223','224'])).
% 108.08/14.14 cnf('326', plain, (c3_1(a333) | c2_1(a333) | c1_1(a300) | $pr(hskp7) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['325','304'])).
% 108.08/14.14 cnf('327', plain, (c3_1(a333) | c2_1(a333) | c1_1(a300) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['326','301'])).
% 108.08/14.14 cnf('328', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp7) | ~$pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['327','83'])).
% 108.08/14.14 cnf('329', plain, ($pr(hskp4) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['295','223','224'])).
% 108.08/14.14 cnf('330', plain, (c3_1(a333) | c2_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(simplify,[],['328','329'])).
% 108.08/14.14 cnf('331', plain, (c3_1(a333) | $pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['330','223','224'])).
% 108.08/14.14 cnf('332', plain, ($pr(hskp7)),
% 108.08/14.14 inference(resolution,[then_simplify],['331','226','224'])).
% 108.08/14.14 cnf('333', plain, (c0_1(a303)),
% 108.08/14.14 inference(resolution,[],['332','105'])).
% 108.08/14.14 cnf('334', plain, (c1_1(a303)),
% 108.08/14.14 inference(resolution,[],['332','102'])).
% 108.08/14.14 cnf('335', plain, ($pr(hskp13) | c3_1(a303) | ~c1_1(X) | ~c2_1(X) | c0_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['333','260','334'])).
% 108.08/14.14 cnf('336', plain, (~c2_1(a315) | $pr(hskp13) | c3_1(a303) | c0_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['241','335'])).
% 108.08/14.14 cnf('337', plain, (~$pr(hskp14) | c2_1(a315)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('338', plain, (c2_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['239','337'])).
% 108.08/14.14 cnf('339', plain, ($pr(hskp13) | c3_1(a303) | c0_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['336','338'])).
% 108.08/14.14 cnf('340', plain, (~$pr(hskp14) | ~c0_1(a315)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('341', plain, (~c0_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['239','340'])).
% 108.08/14.14 cnf('342', plain, ($pr(hskp13) | c3_1(a303) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['339','341'])).
% 108.08/14.14 cnf('343', plain, (~c2_1(a303)),
% 108.08/14.14 inference(resolution,[],['332','108'])).
% 108.08/14.14 cnf('344', plain, (~c3_1(a303) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['333','193','334','343'])).
% 108.08/14.14 cnf('345', plain, ($pr(hskp13) | $pr(hskp4) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['342','344'])).
% 108.08/14.14 cnf('346', plain, (c2_1(a294) | $pr(hskp13) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['345','276'])).
% 108.08/14.14 cnf('347', plain, ($pr(hskp13) | c3_1(a294) | $pr(hskp4) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['346','208'])).
% 108.08/14.14 cnf('348', plain, (~$pr(hskp0) | $pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['347','187'])).
% 108.08/14.14 cnf('349', plain, ($pr(hskp13) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['348','269'])).
% 108.08/14.14 cnf('350', plain, (c0_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['349','64'])).
% 108.08/14.14 cnf('351', plain, (~c3_1(a313) | c1_1(a295) | $pr(hskp11) | $pr(hskp10) | c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['127','350'])).
% 108.08/14.14 cnf('352', plain, (c3_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['349','67'])).
% 108.08/14.14 cnf('353', plain, (c1_1(a295) | $pr(hskp11) | $pr(hskp10) | c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['351','352'])).
% 108.08/14.14 cnf('354', plain, ($pr(hskp11) | $pr(hskp10) | c1_1(a313) | $pr(hskp4) | ~$pr(hskp1)),
% 108.08/14.14 inference(resolution,[],['353','57'])).
% 108.08/14.14 cnf('355', plain, (~c1_1(a313) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['349','70'])).
% 108.08/14.14 cnf('356', plain, (~$pr(hskp1) | $pr(hskp11) | $pr(hskp10) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['354','355'])).
% 108.08/14.14 cnf('357', plain, ($pr(hskp1) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['96','47','99','93','95'])).
% 108.08/14.14 cnf('358', plain, ($pr(hskp11) | $pr(hskp10) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['356','357'])).
% 108.08/14.14 cnf('359', plain, (c0_1(a336) | $pr(hskp11) | $pr(hskp10) | c2_1(a336)),
% 108.08/14.14 inference(resolution,[],['254','115'])).
% 108.08/14.14 cnf('360', plain, ($pr(hskp11) | $pr(hskp10) | c2_1(a336)),
% 108.08/14.14 inference(resolution,[then_simplify],['359','38','227'])).
% 108.08/14.14 cnf('361', plain, (c0_1(a336) | $pr(hskp11) | $pr(hskp10) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['360','8','232'])).
% 108.08/14.14 cnf('362', plain, ($pr(hskp11) | $pr(hskp10) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['361','38','227'])).
% 108.08/14.14 cnf('363', plain, (~$pr(hskp4) | $pr(hskp11) | $pr(hskp10) | c3_1(a300) | c1_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['362','31'])).
% 108.08/14.14 cnf('364', plain, (~$pr(hskp4) | $pr(hskp11) | $pr(hskp10) | c3_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(simplify,[],['363','298'])).
% 108.08/14.14 cnf('365', plain, ($pr(hskp11) | $pr(hskp10) | c3_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['358','364'])).
% 108.08/14.14 cnf('366', plain, (~c2_1(a300) | $pr(hskp11) | $pr(hskp10)),
% 108.08/14.14 inference(resolution,[],['358','78'])).
% 108.08/14.14 cnf('367', plain, ($pr(hskp11) | $pr(hskp10) | c3_1(a300)),
% 108.08/14.14 inference(resolution,[],['365','366'])).
% 108.08/14.14 cnf('368', plain, ($pr(hskp11) | $pr(hskp10) | c0_1(a300) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['367','115'])).
% 108.08/14.14 cnf('369', plain, ($pr(hskp11) | $pr(hskp10) | c2_1(a300) | ~$pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['368','31'])).
% 108.08/14.14 cnf('370', plain, (~$pr(hskp4) | ~c2_1(a300)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('371', plain, (~$pr(hskp4) | $pr(hskp11) | $pr(hskp10)),
% 108.08/14.14 inference(simplify,[],['369','370'])).
% 108.08/14.14 cnf('372', plain, ($pr(hskp11) | $pr(hskp10)),
% 108.08/14.14 inference(resolution,[],['371','358'])).
% 108.08/14.14 cnf('373', plain, (~$pr(hskp10) | c1_1(a308)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('374', plain, ($pr(hskp11) | c1_1(a308)),
% 108.08/14.14 inference(resolution,[],['372','373'])).
% 108.08/14.14 cnf('375', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c1_1(X0) | ~c2_1(X0) | c0_1(X2) | c0_1(X1) | c0_1(X0) | c1_1(X2) | c2_1(X2) | c2_1(X1) | c3_1(X1)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('376', plain, (~c1_1(X) | ~c2_1(X) | c0_1(Y) | c0_1(Z) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(Z) | c3_1(Z)),
% 108.08/14.14 inference(simplify,[then_simplify],['375','6','6','6'])).
% 108.08/14.14 cnf('377', plain, (~c1_1(X) | ~c2_1(X) | c0_1(Y) | c0_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['376'])).
% 108.08/14.14 cnf('378', plain, (~c2_1(a308) | $pr(hskp11) | c0_1(a308) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['374','377'])).
% 108.08/14.14 cnf('379', plain, (~c1_1(X) | ~c1_1(Y) | ~c3_1(X) | c0_1(X) | c0_1(Y) | c2_1(Y) | c3_1(Y)),
% 108.08/14.14 inference(factorization,[],['181'])).
% 108.08/14.14 cnf('380', plain, (~c3_1(a308) | $pr(hskp11) | c0_1(a308) | ~c1_1(X3) | c0_1(X3) | c2_1(X3) | c3_1(X3)),
% 108.08/14.14 inference(resolution,[],['374','379'])).
% 108.08/14.14 cnf('381', plain, (~$pr(hskp10) | c3_1(a308)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('382', plain, ($pr(hskp11) | c3_1(a308)),
% 108.08/14.14 inference(resolution,[],['372','381'])).
% 108.08/14.14 cnf('383', plain, ($pr(hskp11) | c0_1(a308) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[],['380','382'])).
% 108.08/14.14 cnf('384', plain, ($pr(hskp14) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[then_simplify],['234','226','224'])).
% 108.08/14.14 cnf('385', plain, ($pr(hskp14) | c3_1(a294) | c0_1(a321) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['384','199'])).
% 108.08/14.14 cnf('386', plain, ($pr(hskp14) | c3_1(a294) | c0_1(a321) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['385','130'])).
% 108.08/14.14 cnf('387', plain, (~$pr(hskp0) | c1_1(a294) | $pr(hskp14) | c0_1(a321)),
% 108.08/14.14 inference(simplify,[],['386','187'])).
% 108.08/14.14 cnf('388', plain, (c1_1(a294) | $pr(hskp14) | c0_1(a321)),
% 108.08/14.14 inference(simplify,[],['387','235'])).
% 108.08/14.14 cnf('389', plain, (c1_1(a294) | $pr(hskp14) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['388','98','99','93'])).
% 108.08/14.14 cnf('390', plain, (~c3_1(a308) | c2_1(a308) | c1_1(a294) | $pr(hskp14) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['374','389'])).
% 108.08/14.14 cnf('391', plain, (c2_1(a308) | c1_1(a294) | $pr(hskp14) | $pr(hskp11)),
% 108.08/14.14 inference(simplify,[],['390','382'])).
% 108.08/14.14 cnf('392', plain, ($pr(hskp11) | c0_1(a308) | c0_1(a294) | c2_1(a294) | c3_1(a294) | c2_1(a308) | $pr(hskp14)),
% 108.08/14.14 inference(resolution,[],['383','391'])).
% 108.08/14.14 cnf('393', plain, (~$pr(hskp10) | ~c0_1(a308)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('394', plain, (~c0_1(a308) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['372','393'])).
% 108.08/14.14 cnf('395', plain, (c2_1(a308) | c2_1(a294) | $pr(hskp14) | $pr(hskp11) | c0_1(a294) | c3_1(a294)),
% 108.08/14.14 inference(simplify,[],['392','394'])).
% 108.08/14.14 cnf('396', plain, (c2_1(a308) | c2_1(a294) | $pr(hskp14) | $pr(hskp11) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['395','130'])).
% 108.08/14.14 cnf('397', plain, (~$pr(hskp0) | c2_1(a308) | $pr(hskp14) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.14 inference(simplify,[],['396','132'])).
% 108.08/14.14 cnf('398', plain, (c2_1(a308) | $pr(hskp14) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.14 inference(simplify,[],['397','235'])).
% 108.08/14.14 cnf('399', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp12) | ~c0_1(X0) | ~c1_1(X1) | ~c2_1(X1) | c0_1(X1) | c2_1(X0) | c3_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('400', plain, ($pr(hskp12) | ~c0_1(X) | ~c1_1(Y) | ~c2_1(Y) | c0_1(Y) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(simplify,[then_simplify],['399','6','6'])).
% 108.08/14.14 cnf('401', plain, ($pr(hskp12) | c3_1(a303) | ~c1_1(X) | ~c2_1(X) | c0_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['333','400','343'])).
% 108.08/14.14 cnf('402', plain, (~c2_1(a308) | $pr(hskp12) | $pr(hskp11) | c0_1(a308) | c3_1(a303)),
% 108.08/14.14 inference(resolution,[],['374','401'])).
% 108.08/14.14 cnf('403', plain, (~c2_1(a308) | $pr(hskp12) | $pr(hskp11) | c3_1(a303)),
% 108.08/14.14 inference(simplify,[],['402','394'])).
% 108.08/14.14 cnf('404', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11) | c3_1(a303) | c3_1(a294)),
% 108.08/14.14 inference(resolution,[],['398','403'])).
% 108.08/14.14 cnf('405', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11) | c3_1(a303) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['404','237'])).
% 108.08/14.14 cnf('406', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11) | c3_1(a303)),
% 108.08/14.14 inference(simplify,[],['405','235'])).
% 108.08/14.14 cnf('407', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['406','344'])).
% 108.08/14.14 cnf('408', plain, (~c2_1(a315) | $pr(hskp12) | c3_1(a303) | c0_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['241','401'])).
% 108.08/14.14 cnf('409', plain, ($pr(hskp12) | c3_1(a303) | c0_1(a315) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['408','338'])).
% 108.08/14.14 cnf('410', plain, ($pr(hskp12) | c3_1(a303) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['409','341'])).
% 108.08/14.14 cnf('411', plain, ($pr(hskp12) | $pr(hskp4) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['410','344'])).
% 108.08/14.14 cnf('412', plain, ($pr(hskp12) | c3_1(a333) | c2_1(a333) | ~c1_1(X) | ~c2_1(X) | c0_1(X)),
% 108.08/14.14 inference(resolution,[],['217','400'])).
% 108.08/14.14 cnf('413', plain, (~c2_1(a297) | $pr(hskp12) | c3_1(a333) | c0_1(a297) | c2_1(a333) | $pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['412','263'])).
% 108.08/14.14 cnf('414', plain, ($pr(hskp12) | c3_1(a333) | c0_1(a297) | c2_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['258','413'])).
% 108.08/14.14 cnf('415', plain, ($pr(hskp12) | c3_1(a333) | c2_1(a333) | $pr(hskp0) | $pr(hskp4) | ~$pr(hskp2)),
% 108.08/14.14 inference(resolution,[],['414','250'])).
% 108.08/14.14 cnf('416', plain, ($pr(hskp12) | c3_1(a333) | c2_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['415','257'])).
% 108.08/14.14 cnf('417', plain, ($pr(hskp12) | c3_1(a333) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['416','223','224'])).
% 108.08/14.14 cnf('418', plain, ($pr(hskp12) | $pr(hskp0) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[then_simplify],['417','226','224'])).
% 108.08/14.14 cnf('419', plain, ($pr(hskp12) | c3_1(a294) | $pr(hskp4) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['418','272'])).
% 108.08/14.14 cnf('420', plain, ($pr(hskp12) | c3_1(a294) | $pr(hskp4) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['419','130'])).
% 108.08/14.14 cnf('421', plain, (~$pr(hskp0) | c1_1(a294) | $pr(hskp12) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['420','187'])).
% 108.08/14.14 cnf('422', plain, (c1_1(a294) | $pr(hskp12) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['421','418'])).
% 108.08/14.14 cnf('423', plain, (c2_1(a294) | $pr(hskp12) | c3_1(a294) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['411','422'])).
% 108.08/14.14 cnf('424', plain, ($pr(hskp12) | c3_1(a294) | $pr(hskp4) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['423','208'])).
% 108.08/14.14 cnf('425', plain, (~$pr(hskp0) | $pr(hskp12) | $pr(hskp4)),
% 108.08/14.14 inference(simplify,[],['424','187'])).
% 108.08/14.14 cnf('426', plain, ($pr(hskp12) | $pr(hskp4)),
% 108.08/14.14 inference(resolution,[],['425','418'])).
% 108.08/14.14 cnf('427', plain, ($pr(hskp0) | c0_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['333','219','334','343'])).
% 108.08/14.14 cnf('428', plain, (~$pr(hskp4) | c1_1(a300) | $pr(hskp0) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['427','31'])).
% 108.08/14.14 cnf('429', plain, (~$pr(hskp4) | $pr(hskp0) | c2_1(a300)),
% 108.08/14.14 inference(simplify,[],['428','298'])).
% 108.08/14.14 cnf('430', plain, ($pr(hskp12) | $pr(hskp0) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['426','429'])).
% 108.08/14.14 cnf('431', plain, (~c2_1(a300) | $pr(hskp12)),
% 108.08/14.14 inference(resolution,[],['426','78'])).
% 108.08/14.14 cnf('432', plain, ($pr(hskp12) | $pr(hskp0)),
% 108.08/14.14 inference(simplify,[],['430','431'])).
% 108.08/14.14 cnf('433', plain, ($pr(hskp12) | c3_1(a294) | c0_1(a321) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['432','199'])).
% 108.08/14.14 cnf('434', plain, ($pr(hskp12) | c3_1(a294) | c0_1(a321) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['433','130'])).
% 108.08/14.14 cnf('435', plain, (~$pr(hskp0) | c1_1(a294) | $pr(hskp12) | c0_1(a321)),
% 108.08/14.14 inference(simplify,[],['434','187'])).
% 108.08/14.14 cnf('436', plain, (c1_1(a294) | $pr(hskp12) | c0_1(a321)),
% 108.08/14.14 inference(resolution,[],['435','432'])).
% 108.08/14.14 cnf('437', plain, (c1_1(a294) | $pr(hskp12) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['436','98','99','93'])).
% 108.08/14.14 cnf('438', plain, (c1_1(a303)),
% 108.08/14.14 inference(resolution,[],['332','102'])).
% 108.08/14.14 cnf('439', plain, (~c3_1(a303) | c1_1(a294) | $pr(hskp12)),
% 108.08/14.14 inference(resolution,[then_simplify],['437','438','343'])).
% 108.08/14.14 cnf('440', plain, (c1_1(a294) | $pr(hskp14) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['406','439'])).
% 108.08/14.14 cnf('441', plain, (c2_1(a294) | $pr(hskp14) | $pr(hskp12) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.14 inference(resolution,[],['407','440'])).
% 108.08/14.14 cnf('442', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['441','208'])).
% 108.08/14.14 cnf('443', plain, (~$pr(hskp0) | $pr(hskp14) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(simplify,[],['442','187'])).
% 108.08/14.14 cnf('444', plain, ($pr(hskp14) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(simplify,[],['443','235'])).
% 108.08/14.14 cnf('445', plain, ($pr(hskp12) | $pr(hskp11) | c1_1(a315)),
% 108.08/14.14 inference(resolution,[],['444','240'])).
% 108.08/14.14 cnf('446', plain, (~c2_1(a315) | $pr(hskp12) | $pr(hskp11) | c3_1(a303) | c0_1(a315)),
% 108.08/14.14 inference(resolution,[],['445','401'])).
% 108.08/14.14 cnf('447', plain, ($pr(hskp12) | $pr(hskp11) | c2_1(a315)),
% 108.08/14.14 inference(resolution,[],['444','337'])).
% 108.08/14.14 cnf('448', plain, ($pr(hskp12) | $pr(hskp11) | c3_1(a303) | c0_1(a315)),
% 108.08/14.14 inference(resolution,[],['446','447'])).
% 108.08/14.14 cnf('449', plain, (~c0_1(a315) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['444','340'])).
% 108.08/14.14 cnf('450', plain, ($pr(hskp12) | $pr(hskp11) | c3_1(a303)),
% 108.08/14.14 inference(resolution,[],['448','449'])).
% 108.08/14.14 cnf('451', plain, ($pr(hskp12) | $pr(hskp11) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[],['450','344'])).
% 108.08/14.14 cnf('452', plain, (c1_1(a294) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['450','439'])).
% 108.08/14.14 cnf('453', plain, (c2_1(a294) | $pr(hskp12) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.14 inference(resolution,[],['451','452'])).
% 108.08/14.14 cnf('454', plain, ($pr(hskp12) | $pr(hskp11) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.14 inference(resolution,[],['453','208'])).
% 108.08/14.14 cnf('455', plain, (~$pr(hskp0) | $pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(simplify,[],['454','187'])).
% 108.08/14.14 cnf('456', plain, ($pr(hskp12) | $pr(hskp11)),
% 108.08/14.14 inference(resolution,[],['455','432'])).
% 108.08/14.14 cnf('457', plain, ($pr(hskp12) | c1_1(a309)),
% 108.08/14.14 inference(resolution,[],['456','155'])).
% 108.08/14.14 cnf('458', plain, (~$pr(ndr1_0) | $pr(hskp15) | $pr(hskp6) | ~c3_1(X0) | c1_1(X0) | c2_1(X0)),
% 108.08/14.14 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.14 cnf('459', plain, ($pr(hskp15) | $pr(hskp6) | ~c3_1(X) | c1_1(X) | c2_1(X)),
% 108.08/14.14 inference(simplify,[],['458','6'])).
% 108.08/14.14 cnf('460', plain, ($pr(hskp15) | c1_1(a336) | c2_1(a336) | $pr(hskp6)),
% 108.08/14.14 inference(resolution,[],['254','459'])).
% 108.08/14.14 cnf('461', plain, ($pr(hskp15) | c2_1(a336) | $pr(hskp6)),
% 108.08/14.14 inference(resolution,[then_simplify],['460','25','227'])).
% 108.08/14.14 cnf('462', plain, (c0_1(a336) | $pr(hskp15) | $pr(hskp6) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['461','8','232'])).
% 108.08/14.14 cnf('463', plain, ($pr(hskp15) | $pr(hskp6) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.14 inference(resolution,[then_simplify],['462','38','227'])).
% 108.08/14.14 cnf('464', plain, (~$pr(hskp4) | $pr(hskp15) | c3_1(a300) | c1_1(a300) | $pr(hskp6) | c2_1(a300)),
% 108.08/14.14 inference(resolution,[],['463','31'])).
% 108.08/14.14 cnf('465', plain, (~$pr(hskp4) | $pr(hskp15) | c3_1(a300) | $pr(hskp6) | c2_1(a300)),
% 108.08/14.14 inference(simplify,[],['464','298'])).
% 108.08/14.14 cnf('466', plain, (c0_1(a336) | $pr(hskp15) | c1_1(a336) | $pr(hskp1) | $pr(hskp6)),
% 108.08/14.14 inference(resolution,[then_simplify],['461','35','232'])).
% 108.08/14.14 cnf('467', plain, ($pr(hskp15) | c1_1(a336) | $pr(hskp1) | $pr(hskp6)),
% 108.08/14.14 inference(resolution,[then_simplify],['466','38','227'])).
% 108.08/14.14 cnf('468', plain, ($pr(hskp15) | $pr(hskp1) | $pr(hskp6)),
% 108.08/14.14 inference(resolution,[then_simplify],['467','25','227'])).
% 108.08/14.14 cnf('469', plain, ($pr(hskp15) | c0_1(a295) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['468','43'])).
% 108.08/14.15 cnf('470', plain, (~c2_1(a295) | ~c3_1(a295) | c1_1(a295) | $pr(hskp15) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['469','47'])).
% 108.08/14.15 cnf('471', plain, (c2_1(a295) | $pr(hskp15) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['468','49'])).
% 108.08/14.15 cnf('472', plain, (~c3_1(a295) | c1_1(a295) | $pr(hskp15) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['470','471'])).
% 108.08/14.15 cnf('473', plain, (~c2_1(a295) | c1_1(a295) | $pr(hskp15) | $pr(hskp13) | c3_1(a295) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['469','54'])).
% 108.08/14.15 cnf('474', plain, (c1_1(a295) | $pr(hskp15) | $pr(hskp13) | c3_1(a295) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['473','471'])).
% 108.08/14.15 cnf('475', plain, (~$pr(hskp1) | $pr(hskp15) | $pr(hskp13) | c3_1(a295) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['474','57'])).
% 108.08/14.15 cnf('476', plain, ($pr(hskp15) | $pr(hskp13) | c3_1(a295) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['475','468'])).
% 108.08/14.15 cnf('477', plain, (c1_1(a295) | $pr(hskp15) | $pr(hskp13) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['472','476'])).
% 108.08/14.15 cnf('478', plain, ($pr(hskp15) | $pr(hskp13) | $pr(hskp4) | $pr(hskp6) | ~$pr(hskp1)),
% 108.08/14.15 inference(resolution,[],['477','57'])).
% 108.08/14.15 cnf('479', plain, ($pr(hskp15) | $pr(hskp13) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(simplify,[],['478','357'])).
% 108.08/14.15 cnf('480', plain, ($pr(hskp15) | c0_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['479','64'])).
% 108.08/14.15 cnf('481', plain, (~c2_1(a313) | ~c3_1(a313) | $pr(hskp15) | c1_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['480','47'])).
% 108.08/14.15 cnf('482', plain, ($pr(hskp15) | c3_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['479','67'])).
% 108.08/14.15 cnf('483', plain, ($pr(hskp15) | c1_1(a313) | c2_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['482','459'])).
% 108.08/14.15 cnf('484', plain, (~c1_1(a313) | $pr(hskp15) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['479','70'])).
% 108.08/14.15 cnf('485', plain, ($pr(hskp15) | c2_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['483','484'])).
% 108.08/14.15 cnf('486', plain, (~c3_1(a313) | $pr(hskp15) | c1_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['481','485'])).
% 108.08/14.15 cnf('487', plain, ($pr(hskp15) | c1_1(a313) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['486','482'])).
% 108.08/14.15 cnf('488', plain, ($pr(hskp15) | $pr(hskp4) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['487','484'])).
% 108.08/14.15 cnf('489', plain, ($pr(hskp15) | c3_1(a300) | $pr(hskp6) | c2_1(a300)),
% 108.08/14.15 inference(resolution,[],['465','488'])).
% 108.08/14.15 cnf('490', plain, (~c2_1(a300) | $pr(hskp15) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['488','78'])).
% 108.08/14.15 cnf('491', plain, ($pr(hskp15) | c3_1(a300) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['489','490'])).
% 108.08/14.15 cnf('492', plain, ($pr(hskp15) | c1_1(a300) | $pr(hskp6) | c2_1(a300)),
% 108.08/14.15 inference(resolution,[],['491','459'])).
% 108.08/14.15 cnf('493', plain, ($pr(hskp15) | $pr(hskp6) | c2_1(a300) | ~$pr(hskp4)),
% 108.08/14.15 inference(resolution,[],['492','83'])).
% 108.08/14.15 cnf('494', plain, (~$pr(hskp4) | $pr(hskp15) | $pr(hskp6)),
% 108.08/14.15 inference(simplify,[],['493','370'])).
% 108.08/14.15 cnf('495', plain, ($pr(hskp15) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['494','488'])).
% 108.08/14.15 cnf('496', plain, (~$pr(hskp6) | c0_1(a302)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('497', plain, ($pr(hskp15) | c0_1(a302)),
% 108.08/14.15 inference(resolution,[],['495','496'])).
% 108.08/14.15 cnf('498', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp14) | ~c0_1(X1) | ~c1_1(X0) | ~c3_1(X0) | c1_1(X1) | c2_1(X1) | c2_1(X0)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('499', plain, ($pr(hskp14) | ~c0_1(X) | ~c1_1(Y) | ~c3_1(Y) | c1_1(X) | c2_1(X) | c2_1(Y)),
% 108.08/14.15 inference(simplify,[then_simplify],['498','6','6'])).
% 108.08/14.15 cnf('500', plain, ($pr(hskp15) | $pr(hskp14) | c1_1(a302) | c2_1(a302) | ~c1_1(X3) | ~c3_1(X3) | c2_1(X3)),
% 108.08/14.15 inference(resolution,[],['497','499'])).
% 108.08/14.15 cnf('501', plain, (~$pr(hskp6) | ~c2_1(a302)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('502', plain, (~c2_1(a302) | $pr(hskp15)),
% 108.08/14.15 inference(resolution,[],['495','501'])).
% 108.08/14.15 cnf('503', plain, ($pr(hskp15) | $pr(hskp14) | c1_1(a302) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.15 inference(simplify,[],['500','502'])).
% 108.08/14.15 cnf('504', plain, (~c3_1(a309) | c2_1(a309) | $pr(hskp15) | $pr(hskp14) | $pr(hskp12) | c1_1(a302)),
% 108.08/14.15 inference(resolution,[],['457','503'])).
% 108.08/14.15 cnf('505', plain, ($pr(hskp12) | c3_1(a309)),
% 108.08/14.15 inference(resolution,[],['456','160'])).
% 108.08/14.15 cnf('506', plain, (c2_1(a309) | $pr(hskp15) | $pr(hskp14) | $pr(hskp12) | c1_1(a302)),
% 108.08/14.15 inference(simplify,[],['504','505'])).
% 108.08/14.15 cnf('507', plain, (~c1_1(a302) | ~$pr(hskp6)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('508', plain, (c2_1(a309) | $pr(hskp15) | $pr(hskp14) | $pr(hskp12) | ~$pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['506','507'])).
% 108.08/14.15 cnf('509', plain, ($pr(hskp15) | $pr(hskp6)),
% 108.08/14.15 inference(resolution,[],['494','488'])).
% 108.08/14.15 cnf('510', plain, (c2_1(a309) | $pr(hskp15) | $pr(hskp14) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['508','509'])).
% 108.08/14.15 cnf('511', plain, ($pr(hskp15) | $pr(hskp14) | $pr(hskp12) | ~$pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['510','168'])).
% 108.08/14.15 cnf('512', plain, ($pr(hskp12) | $pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['455','432'])).
% 108.08/14.15 cnf('513', plain, ($pr(hskp15) | $pr(hskp14) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['511','512'])).
% 108.08/14.15 cnf('514', plain, ($pr(hskp15) | $pr(hskp12) | c1_1(a315)),
% 108.08/14.15 inference(resolution,[],['513','240'])).
% 108.08/14.15 cnf('515', plain, (~c2_1(a315) | $pr(hskp15) | $pr(hskp12) | c3_1(a303) | c0_1(a315)),
% 108.08/14.15 inference(resolution,[],['514','401'])).
% 108.08/14.15 cnf('516', plain, ($pr(hskp15) | $pr(hskp12) | c2_1(a315)),
% 108.08/14.15 inference(resolution,[],['513','337'])).
% 108.08/14.15 cnf('517', plain, ($pr(hskp15) | $pr(hskp12) | c3_1(a303) | c0_1(a315)),
% 108.08/14.15 inference(resolution,[],['515','516'])).
% 108.08/14.15 cnf('518', plain, (~c0_1(a315) | $pr(hskp15) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['513','340'])).
% 108.08/14.15 cnf('519', plain, ($pr(hskp15) | $pr(hskp12) | c3_1(a303)),
% 108.08/14.15 inference(resolution,[],['517','518'])).
% 108.08/14.15 cnf('520', plain, ($pr(hskp15) | $pr(hskp12) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[],['519','344'])).
% 108.08/14.15 cnf('521', plain, (c1_1(a294) | $pr(hskp15) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['519','439'])).
% 108.08/14.15 cnf('522', plain, (c2_1(a294) | $pr(hskp15) | $pr(hskp12) | c3_1(a294)),
% 108.08/14.15 inference(resolution,[],['520','521'])).
% 108.08/14.15 cnf('523', plain, ($pr(hskp15) | $pr(hskp12) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['522','208'])).
% 108.08/14.15 cnf('524', plain, (~$pr(hskp0) | $pr(hskp15) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['523','187'])).
% 108.08/14.15 cnf('525', plain, ($pr(hskp15) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['524','432'])).
% 108.08/14.15 cnf('526', plain, (~$pr(hskp15) | c1_1(a320)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('527', plain, ($pr(hskp12) | c1_1(a320)),
% 108.08/14.15 inference(resolution,[],['525','526'])).
% 108.08/14.15 cnf('528', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp12) | ~c1_1(X1) | ~c1_1(X0) | ~c3_1(X0) | c0_1(X1) | c2_1(X0) | c3_1(X1)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('529', plain, ($pr(hskp12) | ~c1_1(X) | ~c1_1(Y) | ~c3_1(Y) | c0_1(X) | c2_1(Y) | c3_1(X)),
% 108.08/14.15 inference(simplify,[then_simplify],['528','6','6'])).
% 108.08/14.15 cnf('530', plain, (c3_1(a320) | $pr(hskp12) | c0_1(a320) | ~c1_1(X3) | ~c3_1(X3) | c2_1(X3)),
% 108.08/14.15 inference(resolution,[],['527','529'])).
% 108.08/14.15 cnf('531', plain, (~$pr(hskp15) | ~c0_1(a320)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('532', plain, (~c0_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['525','531'])).
% 108.08/14.15 cnf('533', plain, (c3_1(a320) | $pr(hskp12) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.15 inference(simplify,[],['530','532'])).
% 108.08/14.15 cnf('534', plain, (~c3_1(a309) | c2_1(a309) | c3_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['533','457'])).
% 108.08/14.15 cnf('535', plain, (c2_1(a309) | c3_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['534','505'])).
% 108.08/14.15 cnf('536', plain, (c3_1(a320) | $pr(hskp12) | ~$pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['535','168'])).
% 108.08/14.15 cnf('537', plain, (c3_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['536','512'])).
% 108.08/14.15 cnf('538', plain, (~c3_1(a320) | c1_1(a294) | $pr(hskp12) | c2_1(a320)),
% 108.08/14.15 inference(resolution,[],['527','437'])).
% 108.08/14.15 cnf('539', plain, (~$pr(hskp15) | ~c2_1(a320)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('540', plain, (~c2_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['525','539'])).
% 108.08/14.15 cnf('541', plain, (~c3_1(a320) | c1_1(a294) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['538','540'])).
% 108.08/14.15 cnf('542', plain, (c1_1(a294) | $pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['537','541'])).
% 108.08/14.15 cnf('543', plain, ($pr(hskp12) | c0_1(a294) | c3_1(a294) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.15 inference(resolution,[],['542','529'])).
% 108.08/14.15 cnf('544', plain, (~c3_1(a320) | $pr(hskp12) | c0_1(a294) | c2_1(a320) | c3_1(a294)),
% 108.08/14.15 inference(resolution,[],['543','527'])).
% 108.08/14.15 cnf('545', plain, (c3_1(a320) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['536','512'])).
% 108.08/14.15 cnf('546', plain, ($pr(hskp12) | c0_1(a294) | c2_1(a320) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['544','545'])).
% 108.08/14.15 cnf('547', plain, ($pr(hskp12) | c2_1(a320) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['546','130'])).
% 108.08/14.15 cnf('548', plain, (~$pr(hskp0) | $pr(hskp12) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['547','540'])).
% 108.08/14.15 cnf('549', plain, (~$pr(hskp0) | $pr(hskp12)),
% 108.08/14.15 inference(simplify,[],['548','187'])).
% 108.08/14.15 cnf('550', plain, ($pr(hskp12)),
% 108.08/14.15 inference(resolution,[],['549','432'])).
% 108.08/14.15 cnf('551', plain, (~$pr(hskp12) | ~c0_1(a310)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('552', plain, (~c0_1(a310)),
% 108.08/14.15 inference(resolution,[],['550','551'])).
% 108.08/14.15 cnf('553', plain, (~$pr(hskp12) | ~c2_1(a310)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('554', plain, (~c2_1(a310)),
% 108.08/14.15 inference(resolution,[],['550','553'])).
% 108.08/14.15 cnf('555', plain, (c1_1(a310) | $pr(hskp0)),
% 108.08/14.15 inference(resolution,[then_simplify],['552','427','554'])).
% 108.08/14.15 cnf('556', plain, (~$pr(hskp12) | c3_1(a310)),
% 108.08/14.15 inference(cnf_transformation,[],['co1_$sk'])).
% 108.08/14.15 cnf('557', plain, (c3_1(a310)),
% 108.08/14.15 inference(resolution,[],['550','556'])).
% 108.08/14.15 cnf('558', plain, (~c0_1(a310)),
% 108.08/14.15 inference(resolution,[],['550','551'])).
% 108.08/14.15 cnf('559', plain, ($pr(hskp0) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[then_simplify],['555','182','557','558','554'])).
% 108.08/14.15 cnf('560', plain, (c0_1(a297) | c3_1(a297) | $pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['559','263'])).
% 108.08/14.15 cnf('561', plain, (c3_1(a297) | $pr(hskp0) | ~$pr(hskp2)),
% 108.08/14.15 inference(resolution,[],['560','250'])).
% 108.08/14.15 cnf('562', plain, (~$pr(hskp2) | $pr(hskp0)),
% 108.08/14.15 inference(simplify,[],['561','252'])).
% 108.08/14.15 cnf('563', plain, ($pr(hskp0)),
% 108.08/14.15 inference(simplify,[],['562','257'])).
% 108.08/14.15 cnf('564', plain, (c3_1(a294) | c0_1(a321) | c0_1(X) | c1_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[],['563','199'])).
% 108.08/14.15 cnf('565', plain, (c3_1(a294) | c0_1(a321) | c1_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['564','130'])).
% 108.08/14.15 cnf('566', plain, (~$pr(hskp0) | c1_1(a294) | c0_1(a321)),
% 108.08/14.15 inference(simplify,[],['565','187'])).
% 108.08/14.15 cnf('567', plain, (c1_1(a294) | c0_1(a321)),
% 108.08/14.15 inference(resolution,[],['566','563'])).
% 108.08/14.15 cnf('568', plain, (c1_1(a294) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.15 inference(resolution,[then_simplify],['567','98','99','93'])).
% 108.08/14.15 cnf('569', plain, (~c3_1(a308) | c2_1(a308) | c1_1(a294) | $pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['568','374'])).
% 108.08/14.15 cnf('570', plain, (c2_1(a308) | c1_1(a294) | $pr(hskp11)),
% 108.08/14.15 inference(simplify,[],['569','382'])).
% 108.08/14.15 cnf('571', plain, (c2_1(a308) | $pr(hskp11) | c0_1(a308) | c0_1(a294) | c2_1(a294) | c3_1(a294)),
% 108.08/14.15 inference(resolution,[],['570','383'])).
% 108.08/14.15 cnf('572', plain, (c2_1(a308) | c2_1(a294) | $pr(hskp11) | c0_1(a294) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['571','394'])).
% 108.08/14.15 cnf('573', plain, (c2_1(a308) | c2_1(a294) | $pr(hskp11) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['572','130'])).
% 108.08/14.15 cnf('574', plain, (~$pr(hskp0) | c2_1(a308) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['573','132'])).
% 108.08/14.15 cnf('575', plain, (~$pr(hskp0) | c2_1(a308) | $pr(hskp11)),
% 108.08/14.15 inference(simplify,[],['574','187'])).
% 108.08/14.15 cnf('576', plain, (c2_1(a308) | $pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['575','563'])).
% 108.08/14.15 cnf('577', plain, ($pr(hskp11) | c0_1(a308) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.15 inference(simplify,[],['378','576'])).
% 108.08/14.15 cnf('578', plain, ($pr(hskp11) | c0_1(a308) | c1_1(a294) | c2_1(a294) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['577','130'])).
% 108.08/14.15 cnf('579', plain, (~$pr(hskp0) | c1_1(a294) | c2_1(a294) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['578','394'])).
% 108.08/14.15 cnf('580', plain, (c1_1(a294) | $pr(hskp0)),
% 108.08/14.15 inference(resolution,[then_simplify],['568','555','557','554'])).
% 108.08/14.15 cnf('581', plain, (c1_1(a294) | c2_1(a294) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['579','580'])).
% 108.08/14.15 cnf('582', plain, (c2_1(a294) | $pr(hskp11) | c3_1(a294) | c0_1(a308) | c0_1(a294)),
% 108.08/14.15 inference(resolution,[],['581','383'])).
% 108.08/14.15 cnf('583', plain, (c2_1(a294) | $pr(hskp11) | c0_1(a294) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['582','394'])).
% 108.08/14.15 cnf('584', plain, (c2_1(a294) | $pr(hskp11) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['583','130'])).
% 108.08/14.15 cnf('585', plain, (~$pr(hskp0) | $pr(hskp11) | c3_1(a294)),
% 108.08/14.15 inference(simplify,[],['584','132'])).
% 108.08/14.15 cnf('586', plain, (~$pr(hskp0) | $pr(hskp11)),
% 108.08/14.15 inference(simplify,[],['585','187'])).
% 108.08/14.15 cnf('587', plain, ($pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['586','563'])).
% 108.08/14.15 cnf('588', plain, (c1_1(a309)),
% 108.08/14.15 inference(resolution,[],['587','155'])).
% 108.08/14.15 cnf('589', plain, (c3_1(a309)),
% 108.08/14.15 inference(resolution,[],['587','160'])).
% 108.08/14.15 cnf('590', plain, (c2_1(a309) | c0_1(a309) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[then_simplify],['588','182','589'])).
% 108.08/14.15 cnf('591', plain, (c2_1(a309) | c1_1(a294)),
% 108.08/14.15 inference(resolution,[then_simplify],['588','568','589'])).
% 108.08/14.15 cnf('592', plain, (c2_1(a309) | c0_1(a309) | c0_1(a294) | c3_1(a294)),
% 108.08/14.15 inference(resolution,[],['590','591'])).
% 108.08/14.15 cnf('593', plain, (c2_1(a309) | c0_1(a309) | c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['592','130'])).
% 108.08/14.15 cnf('594', plain, (~$pr(hskp0) | c2_1(a309) | c0_1(a309)),
% 108.08/14.15 inference(simplify,[],['593','187'])).
% 108.08/14.15 cnf('595', plain, ($pr(hskp0) | $pr(hskp2) | ~c1_1(X) | ~c3_1(X) | c2_1(X)),
% 108.08/14.15 inference(resolution,[then_simplify],['244','98','99','93'])).
% 108.08/14.15 cnf('596', plain, ($pr(hskp0) | $pr(hskp2) | c2_1(a309)),
% 108.08/14.15 inference(resolution,[then_simplify],['588','595','589'])).
% 108.08/14.15 cnf('597', plain, (c2_1(a309) | $pr(hskp0)),
% 108.08/14.15 inference(simplify,[],['596','562'])).
% 108.08/14.15 cnf('598', plain, (c2_1(a309) | c0_1(a309)),
% 108.08/14.15 inference(simplify,[],['594','597'])).
% 108.08/14.15 cnf('599', plain, (c1_1(a309)),
% 108.08/14.15 inference(resolution,[],['587','155'])).
% 108.08/14.15 cnf('600', plain, (c2_1(a309) | ~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[then_simplify],['598','193','599','589'])).
% 108.08/14.15 cnf('601', plain, (c2_1(a309) | c3_1(a303)),
% 108.08/14.15 inference(resolution,[then_simplify],['600','438','343'])).
% 108.08/14.15 cnf('602', plain, ($pr(hskp11)),
% 108.08/14.15 inference(resolution,[],['586','563'])).
% 108.08/14.15 cnf('603', plain, (c3_1(a303)),
% 108.08/14.15 inference(resolution,[then_simplify],['601','168','602'])).
% 108.08/14.15 cnf('604', plain, (~c1_1(X) | c2_1(X) | c3_1(X)),
% 108.08/14.15 inference(resolution,[],['603','344'])).
% 108.08/14.15 cnf('605', plain, (~c3_1(a303) | c1_1(a294)),
% 108.08/14.15 inference(resolution,[then_simplify],['568','438','343'])).
% 108.08/14.15 cnf('606', plain, (c1_1(a294)),
% 108.08/14.15 inference(resolution,[],['603','605'])).
% 108.08/14.15 cnf('607', plain, (c2_1(a294) | c3_1(a294)),
% 108.08/14.15 inference(resolution,[],['604','606'])).
% 108.08/14.15 cnf('608', plain, (c3_1(a294) | ~$pr(hskp0)),
% 108.08/14.15 inference(resolution,[],['607','208'])).
% 108.08/14.15 cnf('609', plain, (~$pr(hskp0)),
% 108.08/14.15 inference(simplify,[],['608','187'])).
% 108.08/14.15 cnf('610', plain, ($false),
% 108.08/14.15 inference(resolution,[],['609','563'])).
% 108.08/14.15
% 108.08/14.15 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 108.08/14.15
% 108.08/14.15
% 108.08/14.15 fork 3: search terminated without proof.
% 108.08/14.15
% 108.08/14.15 run 107 fork 2 statistics:
% 108.08/14.15 ----------------------------------
% 108.08/14.15 this run seconds: 12.135775
% 108.08/14.15 total seconds: 13.379531
% 108.08/14.15 stat_given_used: 7203
% 108.08/14.15 stat_given_used_at_endgame: 0
% 108.08/14.15 stat_given_candidates: 116879
% 108.08/14.15 stat_given_candidates_at_endgame: 0
% 108.08/14.15 stat_given_candidates_h: 0
% 108.08/14.15 stat_binres_derived_cl: 1334574
% 108.08/14.15 stat_binres_derived_cl_h: 0
% 108.08/14.15 stat_factor_derived_cl: 2940
% 108.08/14.15 stat_para_derived_cl: 0
% 108.08/14.15 stat_tautologies_discarded: 213967
% 108.08/14.15 stat_forward_subsumed: 396537
% 108.08/14.15 stat_derived_cut: 104924
% 108.08/14.15 stat_derived_rewritten: 0
% 108.08/14.15 stat_weight_discarded_building: 0
% 108.08/14.15 stat_weight_discarded_cl: 0
% 108.08/14.15 stat_internlimit_discarded_cl: 0
% 108.08/14.15 stat_simplified: 75790 simplified 0 derived 0 given
% 108.08/14.15 stat_kept_cl: 727009
% 108.08/14.15 stat_built_cl: 817205
% 108.08/14.15 stat_hyperres_partial_cl: 0
% 108.08/14.15 stat_made_rewriters: 0
% 108.08/14.15 stat_backward_subsumed: 0
% 108.08/14.15 stat_propagated_subsumed: 0
% 108.08/14.15 stat_clsubs_attempted: 450422
% 108.08/14.15 stat_clsubs_fact_groundunit_found: 4
% 108.08/14.15 stat_clsubs_rule_groundunit_found: 2906
% 108.08/14.15 stat_clsubs_top_meta_attempted: 244230092
% 108.08/14.15 stat_clsubs_top_meta_failed: 243779670
% 108.08/14.15 stat_clsubs_top_meta_nonpref_attempted: 244230092
% 108.08/14.15 stat_clsubs_top_meta_nonpref_succeeded: 75506112
% 108.08/14.15 stat_clsubs_top_meta_pref_attempted: 75506112
% 108.08/14.15 stat_clsubs_top_meta_pref1_succeeded: 29639610
% 108.08/14.15 stat_clsubs_top_meta_pref2_succeeded: 450422
% 108.08/14.15 stat_clsubs_top_meta_pref3_succeeded: 450422
% 108.08/14.15 stat_clsubs_top_meta_pref_succeeded: 450422
% 108.08/14.15 stat_clsubs_meta_attempted: 1943010
% 108.08/14.15 stat_clsubs_meta_failed: 1378610
% 108.08/14.15 stat_clsubs_predsymbs_attempted: 0
% 108.08/14.15 stat_clsubs_unit_attempted: 0
% 108.08/14.15 stat_clsubs_full_attempted: 450422
% 108.08/14.15 stat_forwardsubs_attempted: 1123546
% 108.08/14.15 stat_lit_hash_added: 943
% 108.08/14.15 stat_lit_hash_computed: 17636408
% 108.08/14.15 stat_lit_hash_match_found: 478693
% 108.08/14.15 stat_lit_hash_match_miss: 22244321
% 108.08/14.15 stat_lit_hash_cut_ok: 136462
% 108.08/14.15 stat_lit_strong_cut_ok: 0
% 108.08/14.15 stat_lit_hash_subsume_ok: 396537
% 108.08/14.15 clqueue els 10000000 used 1
% 108.08/14.15 clactive els 10000000 used 7204
% 108.08/14.15 clactivesubsume els 10000000 used 42979
% 108.08/14.15 queue_termbuf els 200000000 used 70536963
% 108.08/14.15 hyper_termbuf els 100000000 used 1
% 108.08/14.15 active_termbuf els 100000000 used 355924
% 108.08/14.15 varstack els 5000 last used 1
% 108.08/14.15 given_termbuf els 10000000 last used 13
% 108.08/14.15 simplified_termbuf els 10000000 last used 1
% 108.08/14.15 derived_termbuf els 10000000 last used 3
% 108.08/14.15 wr_mallocs: 15607
% 108.08/14.15 wr_callocs: 19
% 108.08/14.15 wr_reallocs: 1208
% 108.08/14.15 wr_frees: 4
% 108.08/14.15 wr_malloc_bytes: 4163135796
% 108.08/14.15 wr_calloc_bytes: 96065504
% 108.08/14.15 wr_realloc_bytes: 17525080
% 108.08/14.15 wr_realloc_freebytes: 0
% 108.08/14.15 ----------------------------------
%------------------------------------------------------------------------------