%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : SYN478+1 : TPTP v8.1.2. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n020.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:02:03 EDT 2023
% Result : Theorem 190.75s 25.06s
% Output : CNFRefutation 190.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN478+1 : TPTP v8.1.2. Released v2.1.0.
% 0.00/0.13 % Command : gkc %s
% 0.14/0.34 % Computer : n020.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sat Aug 26 20:05:59 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.21/0.40
% 0.21/0.40 input clause set summed statistics:
% 0.21/0.40 ----------------------------------
% 0.21/0.40 in_clause_count: 200
% 0.21/0.40 in_rule_clause_count: 200
% 0.21/0.40 in_fact_clause_count: 0
% 0.21/0.40 in_answer_clause_count: 0
% 0.21/0.40 in_ground_clause_count: 139
% 0.21/0.40 in_unit_clause_count: 0
% 0.21/0.40 in_horn_clause_count: 127
% 0.21/0.40 in_pos_clause_count: 15
% 0.21/0.40 in_neg_clause_count: 47
% 0.21/0.40 in_poseq_clause_count: 0
% 0.21/0.40 in_negeq_clause_count: 0
% 0.21/0.40 in_unitposeq_clause_count: 0
% 0.21/0.40 in_chain_clause_count: 0
% 0.21/0.40 in_min_length: 2
% 0.21/0.40 in_max_length: 12
% 0.21/0.40 in_min_depth: 1
% 0.21/0.40 in_max_depth: 1
% 0.21/0.40 in_min_size: 4
% 0.21/0.40 in_max_size: 24
% 0.21/0.40 in_min_vars: 0
% 0.21/0.40 in_max_vars: 3
% 0.21/0.40 in_extaxiom_count: 0
% 0.21/0.40 in_axiom_count: 0
% 0.21/0.40 in_assumption_count: 0
% 0.21/0.40 in_goal_count: 200
% 0.21/0.40 in_neg_goal_count: 47
% 0.21/0.40 in_pos_goal_count: 15
% 0.21/0.40 in_posunit_goal_count: 0
% 0.21/0.40
% 0.21/0.40 auto guide:
% 0.21/0.40 -----------
% 0.21/0.40 {
% 0.21/0.40 "print":1,
% 0.21/0.40 "print_level": 15,
% 0.21/0.40 "max_size": 0,
% 0.21/0.40 "max_depth": 0,
% 0.21/0.40 "max_length": 0,
% 0.21/0.40 "max_dseconds": 0,
% 0.21/0.40 "equality":0,
% 0.21/0.40 "runs":[
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.21/0.40 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.21/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.21/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":1},
% 0.21/0.40 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.21/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.21/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.21/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.21/0.40 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.21/0.40
% 0.21/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.21/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.21/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.21/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":10},
% 0.21/0.40 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.21/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.21/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.21/0.40
% 0.21/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.21/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.21/0.40 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.21/0.40 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":50},
% 0.21/0.40 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.21/0.40 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.21/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.21/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.21/0.40
% 0.21/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.21/0.40 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.21/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.21/0.40
% 0.21/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.21/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0}
% 0.21/0.40
% 0.21/0.40 ]}
% 0.21/0.40
% 0.21/0.40
% 0.21/0.40 **** run 1 fork 0 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 2 fork 1 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 3 fork 2 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 4 fork 3 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"sine":5,"strategy":["unit"],"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 5 fork 4 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 6 fork 5 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.21/0.40
% 0.21/0.40 **** run 7 fork 6 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.21/0.40
% 0.21/0.40 **** run 8 fork 7 starts with strategy
% 0.21/0.40 {"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.21/0.46
% 0.21/0.46 fork 7: search finished without proof.
% 0.21/0.46
% 0.21/0.46 fork 3: search finished without proof.
% 0.21/0.48
% 0.21/0.48 **** run 16 fork 7 starts with strategy
% 0.21/0.48 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 0.21/0.48
% 0.21/0.48 **** run 12 fork 3 starts with strategy
% 0.21/0.48 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 0.21/0.53
% 0.21/0.53 fork 0: search finished without proof.
% 0.21/0.53
% 0.21/0.53 fork 2: search finished without proof.
% 0.21/0.53
% 0.21/0.53 fork 5: search finished without proof.
% 0.21/0.54
% 0.21/0.54 fork 4: search finished without proof.
% 0.21/0.54
% 0.21/0.54 fork 1: search finished without proof.
% 0.21/0.54
% 0.21/0.54
% 0.21/0.54 fork 6: search terminated without proof.
% 0.21/0.55
% 0.21/0.55 **** run 9 fork 0 starts with strategy
% 0.21/0.55 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 0.21/0.56
% 0.21/0.56 **** run 14 fork 5 starts with strategy
% 0.21/0.56
% 0.21/0.56 **** run 10 fork 1 starts with strategy
% 0.21/0.56 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.21/0.56 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 0.21/0.56
% 0.21/0.56 **** run 11 fork 2 starts with strategy
% 0.21/0.56 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 0.21/0.56
% 0.21/0.56 **** run 13 fork 4 starts with strategy
% 0.21/0.56 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 0.21/0.56
% 0.21/0.56 **** run 15 fork 6 starts with strategy
% 0.21/0.56 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 0.21/0.59
% 0.21/0.59 fork 7: search finished without proof.
% 0.21/0.59
% 0.21/0.59 fork 1: search finished without proof.
% 0.21/0.61
% 0.21/0.61 **** run 24 fork 7 starts with strategy
% 0.21/0.61 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":1}
% 0.21/0.61
% 0.21/0.61
% 0.21/0.61 fork 3: search terminated without proof.
% 0.21/0.62
% 0.21/0.62 **** run 18 fork 1 starts with strategy
% 0.21/0.63
% 0.21/0.63 **** run 20 fork 3 starts with strategy
% 0.21/0.63 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"reverse_clauselist":1}
% 0.21/0.64 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 0.21/0.68
% 0.21/0.68
% 0.21/0.68 fork 0: search terminated without proof.
% 0.21/0.68
% 0.21/0.68 fork 4: search finished without proof.
% 0.21/0.68
% 0.21/0.68
% 0.21/0.68 fork 2: search terminated without proof.
% 0.21/0.68
% 0.21/0.68 fork 5: search finished without proof.
% 0.21/0.69
% 0.21/0.69 fork 1: search finished without proof.
% 0.21/0.69
% 0.21/0.69 fork 3: search finished without proof.
% 0.21/0.69
% 0.21/0.69 **** run 17 fork 0 starts with strategy
% 0.21/0.69 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"depth_penalty":100}
% 0.21/0.70
% 0.21/0.70 fork 6: search finished without proof.
% 0.21/0.70
% 0.21/0.70 **** run 21 fork 4 starts with strategy
% 0.21/0.70 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 0.21/0.70
% 0.21/0.70 **** run 19 fork 2 starts with strategy
% 0.21/0.70 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":2}
% 0.21/0.70
% 0.21/0.70 **** run 28 fork 3 starts with strategy
% 0.21/0.70 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":2,"query_preference":1}
% 0.21/0.71
% 0.21/0.71 **** run 26 fork 1 starts with strategy
% 0.21/0.71 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":2,"sine":1}
% 0.21/0.71
% 0.21/0.71 **** run 22 fork 5 starts with strategy
% 0.21/0.71 {"max_dseconds":1,"strategy":["unit"],"query_preference":2}
% 0.21/0.73
% 0.21/0.73 **** run 23 fork 6 starts with strategy
% 0.21/0.73 {"max_dseconds":1,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 0.21/0.74
% 0.21/0.74 fork 7: search finished without proof.
% 2.37/0.75
% 2.37/0.75 fork 4: search finished without proof.
% 2.37/0.76
% 2.37/0.76 **** run 32 fork 7 starts with strategy
% 2.37/0.76 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":2}
% 2.37/0.76
% 2.37/0.76 fork 5: search finished without proof.
% 2.37/0.77
% 2.37/0.77 **** run 29 fork 4 starts with strategy
% 2.37/0.77 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1}
% 2.37/0.78
% 2.37/0.78 **** run 30 fork 5 starts with strategy
% 2.37/0.78 {"max_dseconds":1,"strategy":["query_focus","max_ground_weight"],"query_preference":1}
% 2.37/0.80
% 2.37/0.80 fork 7: search finished without proof.
% 2.37/0.81
% 2.37/0.81 fork 4: search finished without proof.
% 2.37/0.81
% 2.37/0.81 **** run 40 fork 7 starts with strategy
% 2.37/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.33/0.82
% 3.33/0.82 **** run 37 fork 4 starts with strategy
% 3.33/0.82 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 3.33/0.83
% 3.33/0.83 fork 1: search finished without proof.
% 3.33/0.83
% 3.33/0.83 fork 3: search finished without proof.
% 3.33/0.83
% 3.33/0.83
% 3.33/0.83 fork 0: search terminated without proof.
% 3.33/0.85
% 3.33/0.85 **** run 34 fork 1 starts with strategy
% 3.33/0.85 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 3.33/0.85
% 3.33/0.85 **** run 36 fork 3 starts with strategy
% 3.33/0.85 {"weight_select_ratio":20,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 3.33/0.85
% 3.33/0.85 fork 7: search finished without proof.
% 3.33/0.85
% 3.33/0.85
% 3.33/0.85 fork 2: search terminated without proof.
% 3.33/0.85
% 3.33/0.85 **** run 25 fork 0 starts with strategy
% 3.33/0.85 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":2}
% 3.33/0.87
% 3.33/0.87 **** run 48 fork 7 starts with strategy
% 3.33/0.87 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 3.33/0.87
% 3.33/0.87 fork 6: search finished without proof.
% 3.33/0.87
% 3.33/0.87 **** run 27 fork 2 starts with strategy
% 3.33/0.87 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":1,"query_preference":1}
% 3.33/0.89
% 3.33/0.89 **** run 31 fork 6 starts with strategy
% 3.33/0.89 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 4.05/0.91
% 4.05/0.91
% 4.05/0.91 fork 5: search terminated without proof.
% 4.05/0.92
% 4.05/0.92 **** run 38 fork 5 starts with strategy
% 4.05/0.92 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 4.05/0.94
% 4.05/0.94 fork 1: search finished without proof.
% 4.05/0.95
% 4.05/0.95
% 4.05/0.95 fork 4: search terminated without proof.
% 4.05/0.96
% 4.05/0.96 **** run 42 fork 1 starts with strategy
% 4.05/0.96 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":1}
% 4.05/0.97
% 4.05/0.97 **** run 45 fork 4 starts with strategy
% 4.05/0.97 {"max_dseconds":1,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 4.05/0.97
% 4.05/0.97
% 4.05/0.97 fork 3: search terminated without proof.
% 4.67/0.99
% 4.67/0.99 fork 0: search finished without proof.
% 4.67/0.99
% 4.67/0.99
% 4.67/0.99 fork 7: search terminated without proof.
% 4.67/1.00
% 4.67/1.00 **** run 44 fork 3 starts with strategy
% 4.67/1.00 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":2}
% 4.67/1.00
% 4.67/1.00 fork 2: search finished without proof.
% 4.67/1.01
% 4.67/1.01 **** run 33 fork 0 starts with strategy
% 4.67/1.01 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1,"sine":1}
% 4.67/1.01
% 4.67/1.01 fork 4: search finished without proof.
% 4.67/1.01
% 4.67/1.01 **** run 56 fork 7 starts with strategy
% 4.67/1.01 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 4.67/1.01
% 4.67/1.01
% 4.67/1.01 fork 6: search terminated without proof.
% 4.67/1.02
% 4.67/1.02 **** run 35 fork 2 starts with strategy
% 4.67/1.02 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 4.67/1.03
% 4.67/1.03 **** run 53 fork 4 starts with strategy
% 4.67/1.03 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 4.67/1.03
% 4.67/1.03 **** run 39 fork 6 starts with strategy
% 4.67/1.03 {"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.67/1.04
% 4.67/1.04 fork 0: search finished without proof.
% 4.67/1.04
% 4.67/1.04 fork 3: search finished without proof.
% 4.67/1.05
% 4.67/1.05
% 4.67/1.05 fork 5: search terminated without proof.
% 4.67/1.05
% 4.67/1.05 fork 2: search finished without proof.
% 4.67/1.06
% 4.67/1.06 **** run 41 fork 0 starts with strategy
% 4.67/1.06 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 4.67/1.06
% 4.67/1.06 **** run 52 fork 3 starts with strategy
% 4.67/1.06 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 4.67/1.06
% 4.67/1.06 **** run 46 fork 5 starts with strategy
% 4.67/1.06 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 4.67/1.07
% 4.67/1.07 **** run 43 fork 2 starts with strategy
% 4.67/1.07 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 5.42/1.08
% 5.42/1.08
% 5.42/1.08 fork 1: search terminated without proof.
% 5.50/1.09 No candidate clauses found.
% 5.50/1.09
% 5.50/1.09
% 5.50/1.09 fork 5: search terminated without proof.
% 5.50/1.10
% 5.50/1.10 **** run 50 fork 1 starts with strategy
% 5.50/1.10 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 5.63/1.11
% 5.63/1.11 **** run 54 fork 5 starts with strategy
% 5.63/1.11 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 5.74/1.13
% 5.74/1.13 fork 1: search finished without proof.
% 5.74/1.15
% 5.74/1.15 **** run 58 fork 1 starts with strategy
% 5.74/1.15 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 5.74/1.15
% 5.74/1.15 fork 6: search finished without proof.
% 5.74/1.17
% 5.74/1.17 **** run 47 fork 6 starts with strategy
% 5.74/1.17 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 5.74/1.18
% 5.74/1.18
% 5.74/1.18 fork 0: search terminated without proof.
% 5.74/1.20
% 5.74/1.20
% 5.74/1.20 fork 2: search terminated without proof.
% 5.74/1.20
% 5.74/1.20 **** run 49 fork 0 starts with strategy
% 5.74/1.20 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 6.45/1.21
% 6.45/1.21 **** run 51 fork 2 starts with strategy
% 6.45/1.21 {"weight_select_ratio":100,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 7.09/1.29
% 7.09/1.29
% 7.09/1.29 fork 6: search terminated without proof.
% 7.09/1.31
% 7.09/1.31 **** run 55 fork 6 starts with strategy
% 7.09/1.31 {"max_dseconds":10,"sine":5,"strategy":["unit"],"query_preference":0}
% 7.09/1.32
% 7.09/1.32
% 7.09/1.32 fork 0: search terminated without proof.
% 7.09/1.34
% 7.09/1.34
% 7.09/1.34 fork 2: search terminated without proof.
% 7.09/1.34
% 7.09/1.34 **** run 57 fork 0 starts with strategy
% 7.09/1.34 {"max_dseconds":10,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 7.09/1.35
% 7.09/1.35 fork 6: search finished without proof.
% 7.09/1.36
% 7.09/1.36 **** run 59 fork 2 starts with strategy
% 7.09/1.36 {"max_dseconds":10,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 7.09/1.36
% 7.09/1.36 **** run 63 fork 6 starts with strategy
% 7.09/1.36 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 7.82/1.39
% 7.82/1.39 fork 2: search finished without proof.
% 7.82/1.41
% 7.82/1.41 **** run 67 fork 2 starts with strategy
% 7.82/1.41 {"max_dseconds":10,"strategy":["unit"],"query_preference":0}
% 7.82/1.45
% 7.82/1.45 fork 2: search finished without proof.
% 7.82/1.46
% 7.82/1.46 **** run 75 fork 2 starts with strategy
% 7.82/1.46 {"max_dseconds":10,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 8.37/1.50
% 8.37/1.50 fork 2: search finished without proof.
% 8.37/1.52
% 8.37/1.52 **** run 83 fork 2 starts with strategy
% 8.37/1.52 {"max_dseconds":50,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 8.96/1.56
% 8.96/1.56 fork 2: search finished without proof.
% 8.96/1.57
% 8.96/1.57 **** run 91 fork 2 starts with strategy
% 8.96/1.57 {"max_dseconds":50,"strategy":["unit"],"query_preference":0}
% 8.96/1.60
% 8.96/1.60 fork 2: search finished without proof.
% 9.53/1.62
% 9.53/1.62 **** run 99 fork 2 starts with strategy
% 9.53/1.62 {"max_dseconds":50,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 9.53/1.65
% 9.53/1.65 fork 2: search finished without proof.
% 9.53/1.66
% 9.53/1.66 **** run 107 fork 2 starts with strategy
% 9.53/1.66 {"max_dseconds":250,"strategy":["negative_pref"],"query_preference":0}
% 12.41/2.05
% 12.41/2.05
% 12.41/2.05 fork 7: search terminated without proof.
% 12.41/2.05
% 12.41/2.05
% 12.41/2.05 fork 4: search terminated without proof.
% 12.41/2.07
% 12.41/2.07 **** run 64 fork 7 starts with strategy
% 12.41/2.07 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0}
% 12.41/2.07
% 12.41/2.07 **** run 61 fork 4 starts with strategy
% 12.41/2.07 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 12.41/2.11
% 12.41/2.11 fork 4: search finished without proof.
% 12.41/2.11
% 12.41/2.11 fork 3: search finished without proof.
% 12.41/2.12
% 12.41/2.12 fork 5: search finished without proof.
% 12.41/2.13
% 12.41/2.13 **** run 69 fork 4 starts with strategy
% 12.41/2.13 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 12.41/2.15
% 12.41/2.15 **** run 62 fork 5 starts with strategy
% 12.41/2.15 {"max_dseconds":10,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 12.41/2.15
% 12.41/2.15 **** run 60 fork 3 starts with strategy
% 12.41/2.15 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 13.58/2.19
% 13.58/2.19
% 13.58/2.19 fork 1: search terminated without proof.
% 14.13/2.21
% 14.13/2.21 **** run 66 fork 1 starts with strategy
% 14.13/2.21 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0}
% 14.46/2.24
% 14.46/2.24 fork 1: search finished without proof.
% 14.46/2.26
% 14.46/2.26 **** run 74 fork 1 starts with strategy
% 14.46/2.26 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"sine":2}
% 14.46/2.29
% 14.46/2.29 fork 1: search finished without proof.
% 14.46/2.31
% 14.46/2.31 **** run 82 fork 1 starts with strategy
% 14.46/2.31 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 15.72/2.40
% 15.72/2.40 fork 0: search finished without proof.
% 15.72/2.42
% 15.72/2.42
% 15.72/2.42 fork 6: search terminated without proof.
% 15.72/2.42
% 15.72/2.42 **** run 65 fork 0 starts with strategy
% 15.72/2.42 {"max_dseconds":10,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 15.72/2.44
% 15.72/2.44 **** run 71 fork 6 starts with strategy
% 15.72/2.44 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":10}
% 21.46/3.13
% 21.46/3.13
% 21.46/3.13 fork 7: search terminated without proof.
% 21.46/3.15
% 21.46/3.15 **** run 72 fork 7 starts with strategy
% 21.46/3.15 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 21.46/3.17
% 21.46/3.17
% 21.46/3.17 fork 4: search terminated without proof.
% 21.46/3.18
% 21.46/3.18 fork 3: search finished without proof.
% 21.46/3.18
% 21.46/3.18 **** run 77 fork 4 starts with strategy
% 21.46/3.18 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 21.96/3.19
% 21.96/3.19
% 21.96/3.19 fork 5: search terminated without proof.
% 21.96/3.20
% 21.96/3.20 **** run 68 fork 3 starts with strategy
% 21.96/3.20 {"max_dseconds":10,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 21.96/3.21
% 21.96/3.21 **** run 70 fork 5 starts with strategy
% 21.96/3.21 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 23.12/3.42
% 23.12/3.42 fork 0: search finished without proof.
% 23.84/3.43
% 23.84/3.43 **** run 73 fork 0 starts with strategy
% 23.84/3.43 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 23.84/3.48
% 23.84/3.48
% 23.84/3.48 fork 6: search terminated without proof.
% 23.84/3.50
% 23.84/3.50 **** run 79 fork 6 starts with strategy
% 23.84/3.50 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0}
% 29.11/4.19
% 29.11/4.19 fork 3: search finished without proof.
% 29.82/4.20
% 29.82/4.20 **** run 76 fork 3 starts with strategy
% 29.82/4.20 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":3}
% 29.82/4.21
% 29.82/4.21
% 29.82/4.21 fork 4: search terminated without proof.
% 29.82/4.23
% 29.82/4.23 **** run 85 fork 4 starts with strategy
% 29.82/4.23 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 29.82/4.23 No candidate clauses found.
% 29.82/4.23
% 29.82/4.23
% 29.82/4.23 fork 3: search terminated without proof.
% 29.82/4.23
% 29.82/4.23
% 29.82/4.23 fork 7: search terminated without proof.
% 29.82/4.23
% 29.82/4.23
% 29.82/4.23 fork 5: search terminated without proof.
% 29.82/4.25
% 29.82/4.25 **** run 84 fork 3 starts with strategy
% 29.82/4.25 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 29.82/4.25
% 29.82/4.25 **** run 80 fork 7 starts with strategy
% 29.82/4.25 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 29.82/4.25
% 29.82/4.25 **** run 78 fork 5 starts with strategy
% 29.82/4.25 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 29.82/4.26
% 29.82/4.26 fork 4: search finished without proof.
% 29.82/4.28
% 29.82/4.28 **** run 93 fork 4 starts with strategy
% 29.82/4.28 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 29.82/4.29
% 29.82/4.29 fork 5: search finished without proof.
% 29.82/4.30
% 29.82/4.30 **** run 86 fork 5 starts with strategy
% 29.82/4.30 {"max_dseconds":50,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 31.73/4.47
% 31.73/4.47
% 31.73/4.47 fork 0: search terminated without proof.
% 31.73/4.48
% 31.73/4.48 **** run 81 fork 0 starts with strategy
% 31.73/4.48 {"max_dseconds":50,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 54.44/7.38
% 54.44/7.38
% 54.44/7.38 fork 1: search terminated without proof.
% 54.44/7.40
% 54.44/7.40 **** run 90 fork 1 starts with strategy
% 54.44/7.40 {"max_dseconds":50,"strategy":["query_focus","unit"],"query_preference":0}
% 55.10/7.43
% 55.10/7.43 fork 1: search finished without proof.
% 55.10/7.45
% 55.10/7.45 **** run 98 fork 1 starts with strategy
% 55.10/7.45 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"sine":2}
% 55.48/7.48
% 55.48/7.48 fork 1: search finished without proof.
% 55.48/7.50
% 55.48/7.50 **** run 106 fork 1 starts with strategy
% 55.48/7.50 {"max_dseconds":250,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 63.92/8.62
% 63.92/8.62 fork 6: search finished without proof.
% 64.49/8.65
% 64.49/8.65 **** run 87 fork 6 starts with strategy
% 64.49/8.65 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 70.09/9.36
% 70.09/9.36 fork 3: search finished without proof.
% 70.09/9.37
% 70.09/9.37 **** run 92 fork 3 starts with strategy
% 70.09/9.37 {"max_dseconds":50,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 70.34/9.40
% 70.34/9.40
% 70.34/9.40 fork 4: search terminated without proof.
% 70.34/9.42
% 70.34/9.42 **** run 101 fork 4 starts with strategy
% 70.34/9.42 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 70.75/9.43
% 70.75/9.43 fork 7: search finished without proof.
% 70.86/9.45
% 70.86/9.45 **** run 88 fork 7 starts with strategy
% 70.86/9.45 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0}
% 70.86/9.52
% 70.86/9.52
% 70.86/9.52 fork 5: search terminated without proof.
% 70.86/9.55
% 70.86/9.55 **** run 94 fork 5 starts with strategy
% 70.86/9.55 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":50}
% 70.86/9.59
% 70.86/9.59
% 70.86/9.59 fork 0: search terminated without proof.
% 70.86/9.61
% 70.86/9.61 **** run 89 fork 0 starts with strategy
% 70.86/9.61 {"max_dseconds":50,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 106.06/13.99
% 106.06/13.99
% 106.06/13.99 fork 6: search terminated without proof.
% 106.06/14.01
% 106.06/14.01 **** run 95 fork 6 starts with strategy
% 106.06/14.01 {"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.20/14.38
% 108.20/14.38 fork 3: search finished without proof.
% 108.20/14.39
% 108.20/14.39 **** run 100 fork 3 starts with strategy
% 108.20/14.39 {"max_dseconds":50,"strategy":["query_focus"],"query_preference":3}
% 109.01/14.42 No candidate clauses found.
% 109.01/14.42
% 109.01/14.42
% 109.01/14.42 fork 3: search terminated without proof.
% 109.01/14.43
% 109.01/14.43 **** run 108 fork 3 starts with strategy
% 109.01/14.43 {"max_dseconds":250,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 110.40/14.53
% 110.40/14.53
% 110.40/14.53 fork 7: search terminated without proof.
% 110.40/14.55
% 110.40/14.55 **** run 96 fork 7 starts with strategy
% 110.40/14.55 {"max_dseconds":50,"strategy":["positive_pref"],"query_preference":0}
% 110.40/14.59
% 110.40/14.59
% 110.40/14.59 fork 4: search terminated without proof.
% 110.40/14.60
% 110.40/14.60 **** run 109 fork 4 starts with strategy
% 110.40/14.60 {"max_dseconds":250,"strategy":["query_focus","unit"],"query_preference":0}
% 111.09/14.64
% 111.09/14.64 fork 4: search finished without proof.
% 111.09/14.64
% 111.09/14.64 fork 0: search finished without proof.
% 111.09/14.65
% 111.09/14.65 **** run 117 fork 4 starts with strategy
% 111.09/14.65 {"max_dseconds":1250,"strategy":["query_focus","unit"],"query_preference":0}
% 111.09/14.65
% 111.09/14.65 **** run 97 fork 0 starts with strategy
% 111.09/14.65 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":50}
% 111.64/14.68
% 111.64/14.68 fork 4: search finished without proof.
% 111.64/14.69
% 111.64/14.69
% 111.64/14.69 fork 5: search terminated without proof.
% 111.64/14.70
% 111.64/14.70 **** run 125 fork 4 starts with strategy
% 111.64/14.71
% 111.64/14.71 **** run 102 fork 5 starts with strategy
% 111.64/14.71 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 111.64/14.74
% 111.64/14.74 fork 5: search finished without proof.
% 111.64/14.76
% 111.64/14.76 **** run 110 fork 5 starts with strategy
% 111.64/14.76 {"max_dseconds":250,"strategy":["unit"],"query_preference":0}
% 112.38/14.79
% 112.38/14.79 fork 5: search finished without proof.
% 112.38/14.81
% 112.38/14.81 **** run 118 fork 5 starts with strategy
% 112.38/14.81 {"max_dseconds":1250,"strategy":["unit"],"query_preference":0}
% 112.77/14.84
% 112.77/14.84 fork 5: search finished without proof.
% 112.77/14.85
% 112.77/14.85 **** run 126 fork 5 starts with strategy
% 146.07/19.26
% 146.07/19.26
% 146.07/19.26 fork 6: search terminated without proof.
% 146.07/19.29
% 146.07/19.29 **** run 103 fork 6 starts with strategy
% 146.07/19.29 {"max_dseconds":250,"strategy":["hardness_pref"],"query_preference":0}
% 150.86/19.73
% 150.86/19.73
% 150.86/19.73 fork 0: search terminated without proof.
% 150.86/19.74
% 150.86/19.74
% 150.86/19.74 fork 7: search terminated without proof.
% 150.86/19.75
% 150.86/19.75 **** run 105 fork 0 starts with strategy
% 150.86/19.75 {"max_dseconds":250,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 150.86/19.76
% 150.86/19.76 **** run 104 fork 7 starts with strategy
% 150.86/19.76 {"max_dseconds":250,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 150.86/19.80
% 150.86/19.80 fork 7: search finished without proof.
% 151.60/19.81
% 151.60/19.81 **** run 112 fork 7 starts with strategy
% 151.60/19.81 {"max_dseconds":1250,"strategy":["hardness_pref"],"query_preference":0}
% 190.75/25.06
% 190.75/25.06
% 190.75/25.06 result: proof found
% 190.75/25.06 for /export/starexec/sandbox/benchmark/theBenchmark.p
% 190.75/25.06 by run 108 fork 3 strategy {"max_dseconds":250,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 190.75/25.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 190.75/25.06
% 190.75/25.06 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 190.75/25.06 fof('co1_$sk', plain, ((hskp23 | (hskp0 | hskp6)) & ((hskp16 | (hskp5 | hskp18)) & ((hskp23 | (hskp1 | hskp2)) & ((hskp18 | hskp20) & ((hskp12 | hskp26) & ((hskp20 | (hskp29 | hskp26)) & ((hskp1 | (hskp4 | hskp14)) & ((hskp6 | (hskp20 | hskp25)) & ((hskp7 | (hskp21 | hskp3)) & ((hskp7 | (hskp4 | hskp3)) & ((hskp7 | (hskp1 | hskp28)) & ((hskp14 | (hskp25 | hskp28)) & ((hskp9 | (hskp14 | hskp19)) & ((hskp9 | (hskp2 | hskp30)) & ((hskp18 | (hskp14 | hskp27)) & ((hskp11 | (hskp22 | ((~c3_1(X1) | (~c2_1(X1) | ~c1_1(X1))) | ~ndr1_0))) & ((hskp29 | (((~c3_1(X2) | (~c2_1(X2) | ~c1_1(X2))) | ~ndr1_0) | ((~c3_1(X3) | (~c1_1(X3) | ~c0_1(X3))) | ~ndr1_0))) & ((hskp13 | ((~c2_1(X4) | (~c1_1(X4) | ~c0_1(X4))) | ~ndr1_0)) & ((hskp17 | (((~c3_1(X5) | (~c2_1(X5) | ~c1_1(X5))) | ~ndr1_0) | ((~c2_1(X6) | (~c1_1(X6) | ~c0_1(X6))) | ~ndr1_0))) & ((hskp5 | (((~c3_1(X7) | (~c1_1(X7) | ~c0_1(X7))) | ~ndr1_0) | ((~c2_1(X8) | (~c1_1(X8) | c3_1(X8))) | ~ndr1_0))) & ((hskp6 | (hskp9 | ((~c2_1(X9) | (~c0_1(X9) | c3_1(X9))) | ~ndr1_0))) & ((hskp12 | (hskp14 | ((~c2_1(X10) | (~c0_1(X10) | c3_1(X10))) | ~ndr1_0))) & ((hskp18 | (hskp30 | ((~c2_1(X11) | (~c0_1(X11) | c3_1(X11))) | ~ndr1_0))) & ((hskp11 | (((~c3_1(X12) | (~c1_1(X12) | ~c0_1(X12))) | ~ndr1_0) | ((~c2_1(X13) | (~c0_1(X13) | c3_1(X13))) | ~ndr1_0))) & ((hskp24 | (hskp20 | ((~c1_1(X14) | (~c0_1(X14) | c3_1(X14))) | ~ndr1_0))) & ((hskp8 | (hskp14 | ((~c1_1(X15) | (~c0_1(X15) | c3_1(X15))) | ~ndr1_0))) & ((hskp13 | (hskp14 | ((~c1_1(X16) | (c3_1(X16) | c2_1(X16))) | ~ndr1_0))) & ((hskp16 | (hskp14 | ((~c1_1(X17) | (c3_1(X17) | c2_1(X17))) | ~ndr1_0))) & ((hskp17 | (hskp4 | ((~c0_1(X18) | (c3_1(X18) | c2_1(X18))) | ~ndr1_0))) & ((hskp27 | (((~c1_1(X19) | (~c0_1(X19) | c3_1(X19))) | ~ndr1_0) | ((~c0_1(X20) | (c3_1(X20) | c2_1(X20))) | ~ndr1_0))) & ((hskp23 | (hskp22 | ((~c3_1(X21) | (~c2_1(X21) | c1_1(X21))) | ~ndr1_0))) & ((hskp2 | (hskp22 | ((~c3_1(X22) | (~c2_1(X22) | c1_1(X22))) | ~ndr1_0))) & ((hskp27 | (((~c3_1(X23) | (~c0_1(X23) | c2_1(X23))) | ~ndr1_0) | ((~c3_1(X24) | (~c2_1(X24) | c1_1(X24))) | ~ndr1_0))) & ((hskp20 | (((~c1_1(X25) | (c3_1(X25) | c2_1(X25))) | ~ndr1_0) | ((~c3_1(X26) | (~c0_1(X26) | c1_1(X26))) | ~ndr1_0))) & ((hskp0 | (hskp21 | ((~c2_1(X27) | (~c0_1(X27) | c1_1(X27))) | ~ndr1_0))) & ((hskp0 | (hskp12 | ((~c2_1(X28) | (~c0_1(X28) | c1_1(X28))) | ~ndr1_0))) & ((hskp2 | (hskp20 | ((~c2_1(X29) | (~c0_1(X29) | c1_1(X29))) | ~ndr1_0))) & ((hskp1 | (hskp10 | ((~c2_1(X30) | (c3_1(X30) | c1_1(X30))) | ~ndr1_0))) & ((hskp15 | (hskp19 | ((~c0_1(X31) | (c3_1(X31) | c1_1(X31))) | ~ndr1_0))) & ((hskp1 | (hskp2 | ((~c3_1(X32) | (c2_1(X32) | c1_1(X32))) | ~ndr1_0))) & ((((~c2_1(X33) | (~c1_1(X33) | c3_1(X33))) | ~ndr1_0) | (((~c1_1(X34) | (~c0_1(X34) | c3_1(X34))) | ~ndr1_0) | ((~c3_1(X35) | (c2_1(X35) | c1_1(X35))) | ~ndr1_0))) & ((((~c0_1(X36) | (c3_1(X36) | c2_1(X36))) | ~ndr1_0) | (((~c2_1(X37) | (~c0_1(X37) | c1_1(X37))) | ~ndr1_0) | ((~c3_1(X38) | (c2_1(X38) | c1_1(X38))) | ~ndr1_0))) & ((hskp7 | (hskp8 | ((~c0_1(X39) | (c2_1(X39) | c1_1(X39))) | ~ndr1_0))) & ((hskp18 | (hskp29 | ((~c0_1(X40) | (c2_1(X40) | c1_1(X40))) | ~ndr1_0))) & ((hskp14 | (((~c2_1(X41) | (~c0_1(X41) | c3_1(X41))) | ~ndr1_0) | ((~c0_1(X42) | (c2_1(X42) | c1_1(X42))) | ~ndr1_0))) & ((hskp15 | (((~c0_1(X43) | (c3_1(X43) | c1_1(X43))) | ~ndr1_0) | ((~c0_1(X44) | (c2_1(X44) | c1_1(X44))) | ~ndr1_0))) & ((hskp0 | (((~c1_1(X45) | (~c0_1(X45) | c2_1(X45))) | ~ndr1_0) | ((~c3_1(X46) | (~c2_1(X46) | c0_1(X46))) | ~ndr1_0))) & ((hskp17 | (hskp16 | ((~c2_1(X47) | (~c1_1(X47) | c0_1(X47))) | ~ndr1_0))) & ((hskp28 | (((~c3_1(X48) | (~c0_1(X48) | c2_1(X48))) | ~ndr1_0) | ((~c2_1(X49) | (~c1_1(X49) | c0_1(X49))) | ~ndr1_0))) & ((hskp15 | (hskp14 | ((~c2_1(X50) | (c3_1(X50) | c0_1(X50))) | ~ndr1_0))) & ((((~c3_1(X51) | (~c1_1(X51) | ~c0_1(X51))) | ~ndr1_0) | (((~c3_1(X52) | (~c2_1(X52) | c0_1(X52))) | ~ndr1_0) | ((~c2_1(X53) | (c3_1(X53) | c0_1(X53))) | ~ndr1_0))) & ((((~c2_1(X54) | (~c0_1(X54) | c1_1(X54))) | ~ndr1_0) | (((~c3_1(X55) | (~c2_1(X55) | c0_1(X55))) | ~ndr1_0) | ((~c2_1(X56) | (c3_1(X56) | c0_1(X56))) | ~ndr1_0))) & ((hskp4 | (((~c3_1(X57) | (~c1_1(X57) | c0_1(X57))) | ~ndr1_0) | ((~c2_1(X58) | (c3_1(X58) | c0_1(X58))) | ~ndr1_0))) & ((hskp28 | ((~c1_1(X59) | (c3_1(X59) | c0_1(X59))) | ~ndr1_0)) & ((hskp12 | (((~c2_1(X60) | (~c1_1(X60) | ~c0_1(X60))) | ~ndr1_0) | ((~c1_1(X61) | (c3_1(X61) | c0_1(X61))) | ~ndr1_0))) & ((((~c1_1(X62) | (~c0_1(X62) | c3_1(X62))) | ~ndr1_0) | (((c3_1(X63) | (c2_1(X63) | c1_1(X63))) | ~ndr1_0) | ((~c1_1(X64) | (c3_1(X64) | c0_1(X64))) | ~ndr1_0))) & ((hskp13 | (((~c0_1(X65) | (c3_1(X65) | c1_1(X65))) | ~ndr1_0) | ((~c3_1(X66) | (c2_1(X66) | c0_1(X66))) | ~ndr1_0))) & ((((~c3_1(X67) | (~c0_1(X67) | c1_1(X67))) | ~ndr1_0) | (((~c3_1(X68) | (~c1_1(X68) | c0_1(X68))) | ~ndr1_0) | ((~c3_1(X69) | (c2_1(X69) | c0_1(X69))) | ~ndr1_0))) & ((hskp12 | (((~c3_1(X70) | (~c2_1(X70) | ~c1_1(X70))) | ~ndr1_0) | ((~c1_1(X71) | (c2_1(X71) | c0_1(X71))) | ~ndr1_0))) & ((hskp11 | (((c3_1(X72) | (c2_1(X72) | c1_1(X72))) | ~ndr1_0) | ((~c1_1(X73) | (c2_1(X73) | c0_1(X73))) | ~ndr1_0))) & ((hskp9 | (((~c1_1(X74) | (c3_1(X74) | c0_1(X74))) | ~ndr1_0) | ((~c1_1(X75) | (c2_1(X75) | c0_1(X75))) | ~ndr1_0))) & ((((~c1_1(X76) | (c3_1(X76) | c2_1(X76))) | ~ndr1_0) | (((~c3_1(X77) | (c2_1(X77) | c0_1(X77))) | ~ndr1_0) | ((~c1_1(X78) | (c2_1(X78) | c0_1(X78))) | ~ndr1_0))) & ((hskp6 | (hskp10 | ((c3_1(X79) | (c2_1(X79) | c0_1(X79))) | ~ndr1_0))) & ((hskp9 | (((~c0_1(X80) | (c3_1(X80) | c2_1(X80))) | ~ndr1_0) | ((c3_1(X81) | (c2_1(X81) | c0_1(X81))) | ~ndr1_0))) & ((hskp8 | (((~c3_1(X82) | (~c2_1(X82) | c0_1(X82))) | ~ndr1_0) | ((c3_1(X83) | (c2_1(X83) | c0_1(X83))) | ~ndr1_0))) & ((hskp6 | (((~c2_1(X84) | (~c1_1(X84) | c0_1(X84))) | ~ndr1_0) | ((c3_1(X85) | (c2_1(X85) | c0_1(X85))) | ~ndr1_0))) & ((hskp6 | (((~c2_1(X86) | (c3_1(X86) | c0_1(X86))) | ~ndr1_0) | ((c3_1(X87) | (c2_1(X87) | c0_1(X87))) | ~ndr1_0))) & ((hskp7 | (((~c3_1(X88) | (~c1_1(X88) | c2_1(X88))) | ~ndr1_0) | ((~c3_1(X89) | (c1_1(X89) | c0_1(X89))) | ~ndr1_0))) & ((hskp6 | (hskp5 | ((~c2_1(X90) | (c1_1(X90) | c0_1(X90))) | ~ndr1_0))) & ((hskp2 | (hskp4 | ((~c2_1(X91) | (c1_1(X91) | c0_1(X91))) | ~ndr1_0))) & ((hskp3 | (((~c3_1(X92) | (~c0_1(X92) | c2_1(X92))) | ~ndr1_0) | ((c3_1(X93) | (c1_1(X93) | c0_1(X93))) | ~ndr1_0))) & ((((~c2_1(X94) | (c3_1(X94) | c1_1(X94))) | ~ndr1_0) | (((~c2_1(X95) | (c1_1(X95) | c0_1(X95))) | ~ndr1_0) | ((c3_1(X96) | (c1_1(X96) | c0_1(X96))) | ~ndr1_0))) & ((hskp1 | (hskp2 | ((c2_1(X97) | (c1_1(X97) | c0_1(X97))) | ~ndr1_0))) & ((hskp1 | (hskp27 | ((c2_1(X98) | (c1_1(X98) | c0_1(X98))) | ~ndr1_0))) & ((((~c1_1(X99) | (~c0_1(X99) | c3_1(X99))) | ~ndr1_0) | (((~c3_1(X100) | (~c1_1(X100) | c2_1(X100))) | ~ndr1_0) | ((c2_1(X101) | (c1_1(X101) | c0_1(X101))) | ~ndr1_0))) & ((hskp0 | (((~c2_1(X102) | (c3_1(X102) | c1_1(X102))) | ~ndr1_0) | ((c2_1(X103) | (c1_1(X103) | c0_1(X103))) | ~ndr1_0))) & (((c3_1(a1372) & (c1_1(a1372) & (c0_1(a1372) & ndr1_0))) | ~hskp30) & (((c3_1(a1338) & (c2_1(a1338) & (c1_1(a1338) & ndr1_0))) | ~hskp29) & (((c3_1(a1328) & (c2_1(a1328) & (c0_1(a1328) & ndr1_0))) | ~hskp28) & (((c2_1(a1307) & (c1_1(a1307) & (c0_1(a1307) & ndr1_0))) | ~hskp27) & (((~c3_1(a1411) & (~c2_1(a1411) & (c0_1(a1411) & ndr1_0))) | ~hskp26) & (((~c3_1(a1394) & (c2_1(a1394) & (c0_1(a1394) & ndr1_0))) | ~hskp25) & (((~c3_1(a1370) & (~c1_1(a1370) & (c2_1(a1370) & ndr1_0))) | ~hskp24) & (((~c3_1(a1359) & (~c1_1(a1359) & (~c0_1(a1359) & ndr1_0))) | ~hskp23) & (((~c3_1(a1356) & (c1_1(a1356) & (c0_1(a1356) & ndr1_0))) | ~hskp22) & (((~c2_1(a1352) & (~c0_1(a1352) & (c3_1(a1352) & ndr1_0))) | ~hskp21) & (((~c0_1(a1348) & (c2_1(a1348) & (c1_1(a1348) & ndr1_0))) | ~hskp20) & (((~c2_1(a1344) & (c1_1(a1344) & (c0_1(a1344) & ndr1_0))) | ~hskp19) & (((~c2_1(a1339) & (~c0_1(a1339) & (c1_1(a1339) & ndr1_0))) | ~hskp18) & (((~c0_1(a1334) & (c3_1(a1334) & (c2_1(a1334) & ndr1_0))) | ~hskp17) & (((~c3_1(a1333) & (~c2_1(a1333) & (c1_1(a1333) & ndr1_0))) | ~hskp16) & (((~c3_1(a1331) & (c2_1(a1331) & (c1_1(a1331) & ndr1_0))) | ~hskp15) & (((~c2_1(a1330) & (~c1_1(a1330) & (c0_1(a1330) & ndr1_0))) | ~hskp14) & (((~c3_1(a1326) & (~c2_1(a1326) & (~c1_1(a1326) & ndr1_0))) | ~hskp13) & (((~c0_1(a1325) & (c3_1(a1325) & (c1_1(a1325) & ndr1_0))) | ~hskp12) & (((~c1_1(a1324) & (c3_1(a1324) & (c0_1(a1324) & ndr1_0))) | ~hskp11) & (((~c2_1(a1321) & (c3_1(a1321) & (c0_1(a1321) & ndr1_0))) | ~hskp10) & (((~c1_1(a1320) & (~c0_1(a1320) & (c2_1(a1320) & ndr1_0))) | ~hskp9) & (((~c3_1(a1319) & (~c0_1(a1319) & (c2_1(a1319) & ndr1_0))) | ~hskp8) & (((~c3_1(a1316) & (~c2_1(a1316) & (~c0_1(a1316) & ndr1_0))) | ~hskp7) & (((~c1_1(a1315) & (~c0_1(a1315) & (c3_1(a1315) & ndr1_0))) | ~hskp6) & (((~c3_1(a1314) & (~c0_1(a1314) & (c1_1(a1314) & ndr1_0))) | ~hskp5) & (((~c3_1(a1312) & (~c1_1(a1312) & (c0_1(a1312) & ndr1_0))) | ~hskp4) & (((~c1_1(a1311) & (c2_1(a1311) & (c0_1(a1311) & ndr1_0))) | ~hskp3) & (((~c2_1(a1309) & (c3_1(a1309) & (c1_1(a1309) & ndr1_0))) | ~hskp2) & (((~c2_1(a1308) & (~c1_1(a1308) & (c3_1(a1308) & ndr1_0))) | ~hskp1) & ((~c2_1(a1306) & (~c1_1(a1306) & (~c0_1(a1306) & ndr1_0))) | ~hskp0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 190.75/25.06 inference(negpush_and_skolemize,[],['co1'])).
% 190.75/25.06 fof('co1', conjecture, ~(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0 | (((ndr1_0 & ~c0_1(a1306)) & ~c1_1(a1306)) & ~c2_1(a1306))) & (~hskp1 | (((ndr1_0 & c3_1(a1308)) & ~c1_1(a1308)) & ~c2_1(a1308)))) & (~hskp2 | (((ndr1_0 & c1_1(a1309)) & c3_1(a1309)) & ~c2_1(a1309)))) & (~hskp3 | (((ndr1_0 & c0_1(a1311)) & c2_1(a1311)) & ~c1_1(a1311)))) & (~hskp4 | (((ndr1_0 & c0_1(a1312)) & ~c1_1(a1312)) & ~c3_1(a1312)))) & (~hskp5 | (((ndr1_0 & c1_1(a1314)) & ~c0_1(a1314)) & ~c3_1(a1314)))) & (~hskp6 | (((ndr1_0 & c3_1(a1315)) & ~c0_1(a1315)) & ~c1_1(a1315)))) & (~hskp7 | (((ndr1_0 & ~c0_1(a1316)) & ~c2_1(a1316)) & ~c3_1(a1316)))) & (~hskp8 | (((ndr1_0 & c2_1(a1319)) & ~c0_1(a1319)) & ~c3_1(a1319)))) & (~hskp9 | (((ndr1_0 & c2_1(a1320)) & ~c0_1(a1320)) & ~c1_1(a1320)))) & (~hskp10 | (((ndr1_0 & c0_1(a1321)) & c3_1(a1321)) & ~c2_1(a1321)))) & (~hskp11 | (((ndr1_0 & c0_1(a1324)) & c3_1(a1324)) & ~c1_1(a1324)))) & (~hskp12 | (((ndr1_0 & c1_1(a1325)) & c3_1(a1325)) & ~c0_1(a1325)))) & (~hskp13 | (((ndr1_0 & ~c1_1(a1326)) & ~c2_1(a1326)) & ~c3_1(a1326)))) & (~hskp14 | (((ndr1_0 & c0_1(a1330)) & ~c1_1(a1330)) & ~c2_1(a1330)))) & (~hskp15 | (((ndr1_0 & c1_1(a1331)) & c2_1(a1331)) & ~c3_1(a1331)))) & (~hskp16 | (((ndr1_0 & c1_1(a1333)) & ~c2_1(a1333)) & ~c3_1(a1333)))) & (~hskp17 | (((ndr1_0 & c2_1(a1334)) & c3_1(a1334)) & ~c0_1(a1334)))) & (~hskp18 | (((ndr1_0 & c1_1(a1339)) & ~c0_1(a1339)) & ~c2_1(a1339)))) & (~hskp19 | (((ndr1_0 & c0_1(a1344)) & c1_1(a1344)) & ~c2_1(a1344)))) & (~hskp20 | (((ndr1_0 & c1_1(a1348)) & c2_1(a1348)) & ~c0_1(a1348)))) & (~hskp21 | (((ndr1_0 & c3_1(a1352)) & ~c0_1(a1352)) & ~c2_1(a1352)))) & (~hskp22 | (((ndr1_0 & c0_1(a1356)) & c1_1(a1356)) & ~c3_1(a1356)))) & (~hskp23 | (((ndr1_0 & ~c0_1(a1359)) & ~c1_1(a1359)) & ~c3_1(a1359)))) & (~hskp24 | (((ndr1_0 & c2_1(a1370)) & ~c1_1(a1370)) & ~c3_1(a1370)))) & (~hskp25 | (((ndr1_0 & c0_1(a1394)) & c2_1(a1394)) & ~c3_1(a1394)))) & (~hskp26 | (((ndr1_0 & c0_1(a1411)) & ~c2_1(a1411)) & ~c3_1(a1411)))) & (~hskp27 | (((ndr1_0 & c0_1(a1307)) & c1_1(a1307)) & c2_1(a1307)))) & (~hskp28 | (((ndr1_0 & c0_1(a1328)) & c2_1(a1328)) & c3_1(a1328)))) & (~hskp29 | (((ndr1_0 & c1_1(a1338)) & c2_1(a1338)) & c3_1(a1338)))) & (~hskp30 | (((ndr1_0 & c0_1(a1372)) & c1_1(a1372)) & c3_1(a1372)))) & (((! [U] : (ndr1_0 => ((c0_1(U) | c1_1(U)) | c2_1(U)))) | (! [V] : (ndr1_0 => ((c1_1(V) | c3_1(V)) | ~c2_1(V))))) | hskp0)) & (((! [W] : (ndr1_0 => ((c0_1(W) | c1_1(W)) | c2_1(W)))) | (! [X] : (ndr1_0 => ((c2_1(X) | ~c1_1(X)) | ~c3_1(X))))) | (! [Y] : (ndr1_0 => ((c3_1(Y) | ~c0_1(Y)) | ~c1_1(Y)))))) & (((! [Z] : (ndr1_0 => ((c0_1(Z) | c1_1(Z)) | c2_1(Z)))) | hskp27) | hskp1)) & (((! [X1] : (ndr1_0 => ((c0_1(X1) | c1_1(X1)) | c2_1(X1)))) | hskp2) | hskp1)) & (((! [X2] : (ndr1_0 => ((c0_1(X2) | c1_1(X2)) | c3_1(X2)))) | (! [X3] : (ndr1_0 => ((c0_1(X3) | c1_1(X3)) | ~c2_1(X3))))) | (! [X4] : (ndr1_0 => ((c1_1(X4) | c3_1(X4)) | ~c2_1(X4)))))) & (((! [X5] : (ndr1_0 => ((c0_1(X5) | c1_1(X5)) | c3_1(X5)))) | (! [X6] : (ndr1_0 => ((c2_1(X6) | ~c0_1(X6)) | ~c3_1(X6))))) | hskp3)) & (((! [X7] : (ndr1_0 => ((c0_1(X7) | c1_1(X7)) | ~c2_1(X7)))) | hskp4) | hskp2)) & (((! [X8] : (ndr1_0 => ((c0_1(X8) | c1_1(X8)) | ~c2_1(X8)))) | hskp5) | hskp6)) & (((! [X9] : (ndr1_0 => ((c0_1(X9) | c1_1(X9)) | ~c3_1(X9)))) | (! [X10] : (ndr1_0 => ((c2_1(X10) | ~c1_1(X10)) | ~c3_1(X10))))) | hskp7)) & (((! [X11] : (ndr1_0 => ((c0_1(X11) | c2_1(X11)) | c3_1(X11)))) | (! [X12] : (ndr1_0 => ((c0_1(X12) | c3_1(X12)) | ~c2_1(X12))))) | hskp6)) & (((! [X13] : (ndr1_0 => ((c0_1(X13) | c2_1(X13)) | c3_1(X13)))) | (! [X14] : (ndr1_0 => ((c0_1(X14) | ~c1_1(X14)) | ~c2_1(X14))))) | hskp6)) & (((! [X15] : (ndr1_0 => ((c0_1(X15) | c2_1(X15)) | c3_1(X15)))) | (! [X16] : (ndr1_0 => ((c0_1(X16) | ~c2_1(X16)) | ~c3_1(X16))))) | hskp8)) & (((! [X17] : (ndr1_0 => ((c0_1(X17) | c2_1(X17)) | c3_1(X17)))) | (! [X18] : (ndr1_0 => ((c2_1(X18) | c3_1(X18)) | ~c0_1(X18))))) | hskp9)) & (((! [X19] : (ndr1_0 => ((c0_1(X19) | c2_1(X19)) | c3_1(X19)))) | hskp10) | hskp6)) & (((! [X20] : (ndr1_0 => ((c0_1(X20) | c2_1(X20)) | ~c1_1(X20)))) | (! [X21] : (ndr1_0 => ((c0_1(X21) | c2_1(X21)) | ~c3_1(X21))))) | (! [X22] : (ndr1_0 => ((c2_1(X22) | c3_1(X22)) | ~c1_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))))) | hskp9)) & (((! [X25] : (ndr1_0 => ((c0_1(X25) | c2_1(X25)) | ~c1_1(X25)))) | (! [X26] : (ndr1_0 => ((c1_1(X26) | c2_1(X26)) | c3_1(X26))))) | hskp11)) & (((! [X27] : (ndr1_0 => ((c0_1(X27) | c2_1(X27)) | ~c1_1(X27)))) | (! [X28] : (ndr1_0 => ((~c1_1(X28) | ~c2_1(X28)) | ~c3_1(X28))))) | hskp12)) & (((! [X29] : (ndr1_0 => ((c0_1(X29) | c2_1(X29)) | ~c3_1(X29)))) | (! [X30] : (ndr1_0 => ((c0_1(X30) | ~c1_1(X30)) | ~c3_1(X30))))) | (! [X31] : (ndr1_0 => ((c1_1(X31) | ~c0_1(X31)) | ~c3_1(X31)))))) & (((! [X32] : (ndr1_0 => ((c0_1(X32) | c2_1(X32)) | ~c3_1(X32)))) | (! [X33] : (ndr1_0 => ((c1_1(X33) | c3_1(X33)) | ~c0_1(X33))))) | hskp13)) & (((! [X34] : (ndr1_0 => ((c0_1(X34) | c3_1(X34)) | ~c1_1(X34)))) | (! [X35] : (ndr1_0 => ((c1_1(X35) | c2_1(X35)) | c3_1(X35))))) | (! [X36] : (ndr1_0 => ((c3_1(X36) | ~c0_1(X36)) | ~c1_1(X36)))))) & (((! [X37] : (ndr1_0 => ((c0_1(X37) | c3_1(X37)) | ~c1_1(X37)))) | (! [X38] : (ndr1_0 => ((~c0_1(X38) | ~c1_1(X38)) | ~c2_1(X38))))) | hskp12)) & ((! [X39] : (ndr1_0 => ((c0_1(X39) | c3_1(X39)) | ~c1_1(X39)))) | hskp28)) & (((! [X40] : (ndr1_0 => ((c0_1(X40) | c3_1(X40)) | ~c2_1(X40)))) | (! [X41] : (ndr1_0 => ((c0_1(X41) | ~c1_1(X41)) | ~c3_1(X41))))) | hskp4)) & (((! [X42] : (ndr1_0 => ((c0_1(X42) | c3_1(X42)) | ~c2_1(X42)))) | (! [X43] : (ndr1_0 => ((c0_1(X43) | ~c2_1(X43)) | ~c3_1(X43))))) | (! [X44] : (ndr1_0 => ((c1_1(X44) | ~c0_1(X44)) | ~c2_1(X44)))))) & (((! [X45] : (ndr1_0 => ((c0_1(X45) | c3_1(X45)) | ~c2_1(X45)))) | (! [X46] : (ndr1_0 => ((c0_1(X46) | ~c2_1(X46)) | ~c3_1(X46))))) | (! [X47] : (ndr1_0 => ((~c0_1(X47) | ~c1_1(X47)) | ~c3_1(X47)))))) & (((! [X48] : (ndr1_0 => ((c0_1(X48) | c3_1(X48)) | ~c2_1(X48)))) | hskp14) | hskp15)) & (((! [X49] : (ndr1_0 => ((c0_1(X49) | ~c1_1(X49)) | ~c2_1(X49)))) | (! [X50] : (ndr1_0 => ((c2_1(X50) | ~c0_1(X50)) | ~c3_1(X50))))) | hskp28)) & (((! [X51] : (ndr1_0 => ((c0_1(X51) | ~c1_1(X51)) | ~c2_1(X51)))) | hskp16) | hskp17)) & (((! [X52] : (ndr1_0 => ((c0_1(X52) | ~c2_1(X52)) | ~c3_1(X52)))) | (! [X53] : (ndr1_0 => ((c2_1(X53) | ~c0_1(X53)) | ~c1_1(X53))))) | hskp0)) & (((! [X54] : (ndr1_0 => ((c1_1(X54) | c2_1(X54)) | ~c0_1(X54)))) | (! [X55] : (ndr1_0 => ((c1_1(X55) | c3_1(X55)) | ~c0_1(X55))))) | hskp15)) & (((! [X56] : (ndr1_0 => ((c1_1(X56) | c2_1(X56)) | ~c0_1(X56)))) | (! [X57] : (ndr1_0 => ((c3_1(X57) | ~c0_1(X57)) | ~c2_1(X57))))) | hskp14)) & (((! [X58] : (ndr1_0 => ((c1_1(X58) | c2_1(X58)) | ~c0_1(X58)))) | hskp29) | hskp18)) & (((! [X59] : (ndr1_0 => ((c1_1(X59) | c2_1(X59)) | ~c0_1(X59)))) | hskp8) | hskp7)) & (((! [X60] : (ndr1_0 => ((c1_1(X60) | c2_1(X60)) | ~c3_1(X60)))) | (! [X61] : (ndr1_0 => ((c1_1(X61) | ~c0_1(X61)) | ~c2_1(X61))))) | (! [X62] : (ndr1_0 => ((c2_1(X62) | c3_1(X62)) | ~c0_1(X62)))))) & (((! [X63] : (ndr1_0 => ((c1_1(X63) | c2_1(X63)) | ~c3_1(X63)))) | (! [X64] : (ndr1_0 => ((c3_1(X64) | ~c0_1(X64)) | ~c1_1(X64))))) | (! [X65] : (ndr1_0 => ((c3_1(X65) | ~c1_1(X65)) | ~c2_1(X65)))))) & (((! [X66] : (ndr1_0 => ((c1_1(X66) | c2_1(X66)) | ~c3_1(X66)))) | hskp2) | hskp1)) & (((! [X67] : (ndr1_0 => ((c1_1(X67) | c3_1(X67)) | ~c0_1(X67)))) | hskp19) | hskp15)) & (((! [X68] : (ndr1_0 => ((c1_1(X68) | c3_1(X68)) | ~c2_1(X68)))) | hskp10) | hskp1)) & (((! [X69] : (ndr1_0 => ((c1_1(X69) | ~c0_1(X69)) | ~c2_1(X69)))) | hskp20) | hskp2)) & (((! [X70] : (ndr1_0 => ((c1_1(X70) | ~c0_1(X70)) | ~c2_1(X70)))) | hskp12) | hskp0)) & (((! [X71] : (ndr1_0 => ((c1_1(X71) | ~c0_1(X71)) | ~c2_1(X71)))) | hskp21) | hskp0)) & (((! [X72] : (ndr1_0 => ((c1_1(X72) | ~c0_1(X72)) | ~c3_1(X72)))) | (! [X73] : (ndr1_0 => ((c2_1(X73) | c3_1(X73)) | ~c1_1(X73))))) | hskp20)) & (((! [X74] : (ndr1_0 => ((c1_1(X74) | ~c2_1(X74)) | ~c3_1(X74)))) | (! [X75] : (ndr1_0 => ((c2_1(X75) | ~c0_1(X75)) | ~c3_1(X75))))) | hskp27)) & (((! [X76] : (ndr1_0 => ((c1_1(X76) | ~c2_1(X76)) | ~c3_1(X76)))) | hskp22) | hskp2)) & (((! [X77] : (ndr1_0 => ((c1_1(X77) | ~c2_1(X77)) | ~c3_1(X77)))) | hskp22) | hskp23)) & (((! [X78] : (ndr1_0 => ((c2_1(X78) | c3_1(X78)) | ~c0_1(X78)))) | (! [X79] : (ndr1_0 => ((c3_1(X79) | ~c0_1(X79)) | ~c1_1(X79))))) | hskp27)) & (((! [X80] : (ndr1_0 => ((c2_1(X80) | c3_1(X80)) | ~c0_1(X80)))) | hskp4) | hskp17)) & (((! [X81] : (ndr1_0 => ((c2_1(X81) | c3_1(X81)) | ~c1_1(X81)))) | hskp14) | hskp16)) & (((! [X82] : (ndr1_0 => ((c2_1(X82) | c3_1(X82)) | ~c1_1(X82)))) | hskp14) | hskp13)) & (((! [X83] : (ndr1_0 => ((c3_1(X83) | ~c0_1(X83)) | ~c1_1(X83)))) | hskp14) | hskp8)) & (((! [X84] : (ndr1_0 => ((c3_1(X84) | ~c0_1(X84)) | ~c1_1(X84)))) | hskp20) | hskp24)) & (((! [X85] : (ndr1_0 => ((c3_1(X85) | ~c0_1(X85)) | ~c2_1(X85)))) | (! [X86] : (ndr1_0 => ((~c0_1(X86) | ~c1_1(X86)) | ~c3_1(X86))))) | hskp11)) & (((! [X87] : (ndr1_0 => ((c3_1(X87) | ~c0_1(X87)) | ~c2_1(X87)))) | hskp30) | hskp18)) & (((! [X88] : (ndr1_0 => ((c3_1(X88) | ~c0_1(X88)) | ~c2_1(X88)))) | hskp14) | hskp12)) & (((! [X89] : (ndr1_0 => ((c3_1(X89) | ~c0_1(X89)) | ~c2_1(X89)))) | hskp9) | hskp6)) & (((! [X90] : (ndr1_0 => ((c3_1(X90) | ~c1_1(X90)) | ~c2_1(X90)))) | (! [X91] : (ndr1_0 => ((~c0_1(X91) | ~c1_1(X91)) | ~c3_1(X91))))) | hskp5)) & (((! [X92] : (ndr1_0 => ((~c0_1(X92) | ~c1_1(X92)) | ~c2_1(X92)))) | (! [X93] : (ndr1_0 => ((~c1_1(X93) | ~c2_1(X93)) | ~c3_1(X93))))) | hskp17)) & ((! [X94] : (ndr1_0 => ((~c0_1(X94) | ~c1_1(X94)) | ~c2_1(X94)))) | hskp13)) & (((! [X95] : (ndr1_0 => ((~c0_1(X95) | ~c1_1(X95)) | ~c3_1(X95)))) | (! [X96] : (ndr1_0 => ((~c1_1(X96) | ~c2_1(X96)) | ~c3_1(X96))))) | hskp29)) & (((! [X97] : (ndr1_0 => ((~c1_1(X97) | ~c2_1(X97)) | ~c3_1(X97)))) | hskp22) | hskp11)) & ((hskp27 | hskp14) | hskp18)) & ((hskp30 | hskp2) | hskp9)) & ((hskp19 | hskp14) | hskp9)) & ((hskp28 | hskp25) | hskp14)) & ((hskp28 | hskp1) | hskp7)) & ((hskp3 | hskp4) | hskp7)) & ((hskp3 | hskp21) | hskp7)) & ((hskp25 | hskp20) | hskp6)) & ((hskp14 | hskp4) | hskp1)) & ((hskp26 | hskp29) | hskp20)) & (hskp26 | hskp12)) & (hskp20 | hskp18)) & ((hskp2 | hskp1) | hskp23)) & ((hskp18 | hskp5) | hskp16)) & ((hskp6 | hskp0) | hskp23)),
% 190.75/25.06 input).
% 190.75/25.06 cnf('1', plain, (~$pr(ndr1_0) | $pr(hskp28) | ~c1_1(X0) | c0_1(X0) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('2', plain, ($pr(hskp18) | $pr(hskp20)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('3', plain, (~$pr(hskp18) | $pr(ndr1_0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('4', plain, ($pr(hskp20) | $pr(ndr1_0)),
% 190.75/25.06 inference(resolution,[],['2','3'])).
% 190.75/25.06 cnf('5', plain, (~$pr(hskp20) | $pr(ndr1_0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('6', plain, ($pr(ndr1_0)),
% 190.75/25.06 inference(simplify,[],['4','5'])).
% 190.75/25.06 cnf('7', plain, ($pr(hskp28) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['1','6'])).
% 190.75/25.06 cnf('8', plain, (~$pr(hskp28) | c0_1(a1328)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('9', plain, (c0_1(a1328) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['7','8'])).
% 190.75/25.06 cnf('10', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c0_1(X0) | ~c2_1(X2) | ~c2_1(X1) | ~c2_1(X0) | ~c3_1(X1) | c0_1(X2) | c0_1(X1) | c1_1(X0) | c3_1(X2)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('11', plain, (~c0_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c2_1(X) | ~c3_1(Z) | c0_1(Y) | c0_1(Z) | c1_1(X) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['10','6','6','6'])).
% 190.75/25.06 cnf('12', plain, (~c2_1(a1328) | c1_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c3_1(Y) | c0_1(Y) | c0_1(Z) | c0_1(X) | c3_1(Z) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['9','11'])).
% 190.75/25.06 cnf('13', plain, (~c2_1(a1328) | c1_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(X) | ~c3_1(Y) | c0_1(Y) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['12'])).
% 190.75/25.06 cnf('14', plain, (~$pr(hskp28) | c2_1(a1328)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('15', plain, (c2_1(a1328) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['7','14'])).
% 190.75/25.06 cnf('16', plain, (c1_1(a1328) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(Z) | ~c2_1(Y) | ~c3_1(Z) | c0_1(X) | c0_1(Z) | c0_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['13','15'])).
% 190.75/25.06 cnf('17', plain, (c1_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(X) | ~c3_1(Y) | c0_1(Y) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['16'])).
% 190.75/25.06 cnf('18', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c0_1(X0) | ~c1_1(X0) | ~c2_1(X2) | ~c2_1(X1) | ~c3_1(X1) | ~c3_1(X0) | c0_1(X2) | c0_1(X1) | c3_1(X2)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('19', plain, (~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c3_1(Z) | ~c3_1(X) | c0_1(Y) | c0_1(Z) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['18','6','6','6'])).
% 190.75/25.06 cnf('20', plain, (~c1_1(a1328) | ~c3_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c3_1(Y) | c0_1(Y) | c0_1(Z) | c0_1(X) | c3_1(Z) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['9','19'])).
% 190.75/25.06 cnf('21', plain, (~c1_1(a1328) | ~c3_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(X) | ~c3_1(Y) | c0_1(Y) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['20'])).
% 190.75/25.06 cnf('22', plain, (~c3_1(a1328) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(Z) | ~c2_1(X) | ~c2_1(U) | ~c2_1(Y) | ~c3_1(Z) | ~c3_1(U) | c0_1(Z) | c0_1(X) | c0_1(U) | c0_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['17','21'])).
% 190.75/25.06 cnf('23', plain, (~c3_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c2_1(X) | ~c3_1(Y) | ~c3_1(Z) | c0_1(Y) | c0_1(Z) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['22'])).
% 190.75/25.06 cnf('24', plain, (~c3_1(a1328) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(X) | ~c3_1(Y) | c0_1(Y) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['23'])).
% 190.75/25.06 cnf('25', plain, (~$pr(hskp28) | c3_1(a1328)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('26', plain, (c3_1(a1328) | ~c1_1(X) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['7','25'])).
% 190.75/25.06 cnf('27', plain, (~c1_1(X) | ~c1_1(Y) | ~c2_1(Z) | ~c2_1(Y) | ~c3_1(Z) | c0_1(X) | c0_1(Z) | c0_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['24','26'])).
% 190.75/25.06 cnf('28', plain, (~c1_1(X) | ~c2_1(Y) | ~c2_1(X) | ~c3_1(Y) | c0_1(Y) | c0_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['27'])).
% 190.75/25.06 cnf('29', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp8) | ~c2_1(X0) | ~c3_1(X0) | c0_1(X1) | c0_1(X0) | c2_1(X1) | c3_1(X1)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('30', plain, ($pr(hskp8) | ~c2_1(X) | ~c3_1(X) | c0_1(Y) | c0_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['29','6','6'])).
% 190.75/25.06 cnf('31', plain, (~$pr(hskp8) | c2_1(a1319)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('32', plain, (c2_1(a1319) | ~c2_1(X) | ~c3_1(X) | c0_1(Y) | c0_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['30','31'])).
% 190.75/25.06 cnf('33', plain, (c2_1(a1319) | c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 190.75/25.06 inference(factorization,[],['32'])).
% 190.75/25.06 cnf('34', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c2_1(X1) | ~c2_1(X0) | c0_1(X2) | c0_1(X1) | c1_1(X2) | c1_1(X1) | c1_1(X0) | c3_1(X2) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('35', plain, (~c2_1(X) | ~c2_1(Y) | c0_1(Z) | c0_1(X) | c1_1(Z) | c1_1(X) | c1_1(Y) | c3_1(Z) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['34','6','6','6'])).
% 190.75/25.06 cnf('36', plain, (~c2_1(X) | c0_1(Y) | c0_1(X) | c1_1(Y) | c1_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['35'])).
% 190.75/25.06 cnf('37', plain, (~c2_1(X) | c0_1(X) | c1_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['36'])).
% 190.75/25.06 cnf('38', plain, (c1_1(a1319) | c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 190.75/25.06 inference(resolution,[],['33','37'])).
% 190.75/25.06 cnf('39', plain, (~c2_1(a1319) | c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y)),
% 190.75/25.06 inference(resolution,[],['28','38'])).
% 190.75/25.06 cnf('40', plain, (~c2_1(a1319) | c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 190.75/25.06 inference(factorization,[],['39'])).
% 190.75/25.06 cnf('41', plain, (c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y)),
% 190.75/25.06 inference(resolution,[],['40','33'])).
% 190.75/25.06 cnf('42', plain, (c0_1(a1319) | c3_1(a1319) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 190.75/25.06 inference(factorization,[],['41'])).
% 190.75/25.06 cnf('43', plain, (~c0_1(a1319) | ~$pr(hskp8)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('44', plain, (c3_1(a1319) | ~c2_1(X3) | ~c3_1(X3) | c0_1(X3) | ~$pr(hskp8)),
% 190.75/25.06 inference(resolution,[],['42','43'])).
% 190.75/25.06 cnf('45', plain, (~c3_1(a1319) | ~$pr(hskp8)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('46', plain, (~$pr(hskp8) | ~c2_1(X) | ~c3_1(X) | c0_1(X)),
% 190.75/25.06 inference(simplify,[],['44','45'])).
% 190.75/25.06 cnf('47', plain, (~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(Z) | c0_1(X) | c0_1(Y) | c2_1(Z) | c3_1(Z)),
% 190.75/25.06 inference(resolution,[],['46','30'])).
% 190.75/25.06 cnf('48', plain, (~c2_1(X) | ~c3_1(X) | c0_1(Y) | c0_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['47'])).
% 190.75/25.06 cnf('49', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp9) | ~c0_1(X0) | c0_1(X1) | c2_1(X1) | c2_1(X0) | c3_1(X1) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('50', plain, ($pr(hskp9) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(simplify,[then_simplify],['49','6','6'])).
% 190.75/25.06 cnf('51', plain, (~$pr(hskp9) | c2_1(a1320)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('52', plain, (c2_1(a1320) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['50','51'])).
% 190.75/25.06 cnf('53', plain, (~c3_1(a1320) | c0_1(a1320) | ~c0_1(X) | c0_1(Y) | c0_1(Z) | c2_1(Y) | c2_1(X) | c2_1(Z) | c3_1(Y) | c3_1(X) | c3_1(Z)),
% 190.75/25.06 inference(resolution,[],['48','52'])).
% 190.75/25.06 cnf('54', plain, (~c3_1(a1320) | c0_1(a1320) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['53'])).
% 190.75/25.06 cnf('55', plain, (c2_1(a1320) | c0_1(a1320) | c3_1(a1320) | ~c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['52'])).
% 190.75/25.06 cnf('56', plain, (c0_1(a1320) | c3_1(a1320) | c1_1(a1320) | ~c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['55','37'])).
% 190.75/25.06 cnf('57', plain, (~c0_1(a1320) | ~$pr(hskp9)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('58', plain, (c3_1(a1320) | c1_1(a1320) | ~c0_1(X3) | c2_1(X3) | c3_1(X3) | ~$pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['56','57'])).
% 190.75/25.06 cnf('59', plain, (~c1_1(a1320) | ~$pr(hskp9)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('60', plain, (~$pr(hskp9) | c3_1(a1320) | ~c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['58','59'])).
% 190.75/25.06 cnf('61', plain, (c3_1(a1320) | ~c0_1(X) | ~c0_1(Y) | c0_1(Z) | c2_1(Z) | c2_1(X) | c2_1(Y) | c3_1(Z) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['60','50'])).
% 190.75/25.06 cnf('62', plain, (c3_1(a1320) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['61'])).
% 190.75/25.06 cnf('63', plain, (c0_1(a1320) | ~c0_1(X) | ~c0_1(Y) | c0_1(Z) | c0_1(U) | c2_1(Z) | c2_1(X) | c2_1(U) | c2_1(Y) | c3_1(Z) | c3_1(X) | c3_1(U) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['54','62'])).
% 190.75/25.06 cnf('64', plain, (c0_1(a1320) | ~c0_1(X) | c0_1(Y) | c0_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Y) | c3_1(Z) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['63'])).
% 190.75/25.06 cnf('65', plain, (c0_1(a1320) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['64'])).
% 190.75/25.06 cnf('66', plain, (~$pr(hskp9) | ~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['65','57'])).
% 190.75/25.06 cnf('67', plain, (~c0_1(X) | ~c0_1(Y) | c0_1(Z) | c0_1(U) | c2_1(Z) | c2_1(X) | c2_1(U) | c2_1(Y) | c3_1(Z) | c3_1(X) | c3_1(U) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['66','50'])).
% 190.75/25.06 cnf('68', plain, (~c0_1(X) | c0_1(Y) | c0_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Y) | c3_1(Z) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['67'])).
% 190.75/25.06 cnf('69', plain, (~c0_1(X) | c0_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['68'])).
% 190.75/25.06 cnf('70', plain, (~$pr(hskp12) | c1_1(a1325)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('71', plain, ($pr(hskp12) | $pr(hskp26)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('72', plain, ($pr(hskp26) | c1_1(a1325)),
% 190.75/25.06 inference(resolution,[],['70','71'])).
% 190.75/25.06 cnf('73', plain, (~$pr(hskp26) | c0_1(a1411)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('74', plain, (c0_1(a1411) | c1_1(a1325)),
% 190.75/25.06 inference(resolution,[],['72','73'])).
% 190.75/25.06 cnf('75', plain, (c2_1(a1411) | c3_1(a1411) | c1_1(a1325) | c0_1(X3) | c2_1(X3) | c3_1(X3)),
% 190.75/25.06 inference(resolution,[],['69','74'])).
% 190.75/25.06 cnf('76', plain, (~$pr(hskp26) | ~c3_1(a1411)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('77', plain, (~c3_1(a1411) | c1_1(a1325)),
% 190.75/25.06 inference(resolution,[],['72','76'])).
% 190.75/25.06 cnf('78', plain, (c2_1(a1411) | c1_1(a1325) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['75','77'])).
% 190.75/25.06 cnf('79', plain, (~c2_1(a1411) | ~$pr(hskp26)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('80', plain, (c1_1(a1325) | c0_1(X3) | c2_1(X3) | c3_1(X3) | ~$pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['78','79'])).
% 190.75/25.06 cnf('81', plain, ($pr(hskp26) | c1_1(a1325)),
% 190.75/25.06 inference(resolution,[],['70','71'])).
% 190.75/25.06 cnf('82', plain, (c1_1(a1325) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['80','81'])).
% 190.75/25.06 cnf('83', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp11) | ~c1_1(X1) | c0_1(X1) | c1_1(X0) | c2_1(X1) | c2_1(X0) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('84', plain, ($pr(hskp11) | ~c1_1(X) | c0_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['83','6','6'])).
% 190.75/25.06 cnf('85', plain, (~$pr(hskp11) | c0_1(a1324)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('86', plain, (c0_1(a1324) | ~c1_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['84','85'])).
% 190.75/25.06 cnf('87', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | ~$pr(ndr1_0) | ~c0_1(X0) | ~c1_1(X1) | ~c3_1(X2) | ~c3_1(X1) | ~c3_1(X0) | c0_1(X2) | c0_1(X1) | c1_1(X0) | c2_1(X2)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('88', plain, (~c0_1(X) | ~c1_1(Y) | ~c3_1(Z) | ~c3_1(Y) | ~c3_1(X) | c0_1(Z) | c0_1(Y) | c1_1(X) | c2_1(Z)),
% 190.75/25.06 inference(simplify,[then_simplify],['87','6','6','6'])).
% 190.75/25.06 cnf('89', plain, (~c0_1(X) | ~c1_1(Y) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(X) | c2_1(Y)),
% 190.75/25.06 inference(factorization,[],['88'])).
% 190.75/25.06 cnf('90', plain, (~c3_1(a1324) | c1_1(a1324) | ~c1_1(X) | ~c1_1(Y) | ~c3_1(X) | c0_1(X) | c0_1(Y) | c1_1(Z) | c2_1(X) | c2_1(Z) | c2_1(Y) | c3_1(Z)),
% 190.75/25.06 inference(resolution,[],['86','89'])).
% 190.75/25.06 cnf('91', plain, (~c3_1(a1324) | c1_1(a1324) | ~c1_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['90'])).
% 190.75/25.06 cnf('92', plain, (~$pr(hskp11) | c3_1(a1324)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('93', plain, (c3_1(a1324) | ~c1_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['84','92'])).
% 190.75/25.06 cnf('94', plain, (c1_1(a1324) | ~c1_1(X) | ~c1_1(Y) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(Z) | c1_1(U) | c2_1(Z) | c2_1(X) | c2_1(U) | c2_1(Y) | c3_1(Z) | c3_1(U)),
% 190.75/25.06 inference(resolution,[],['91','93'])).
% 190.75/25.06 cnf('95', plain, (c1_1(a1324) | ~c1_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c1_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Y) | c3_1(Z)),
% 190.75/25.06 inference(factorization,[],['94'])).
% 190.75/25.06 cnf('96', plain, (c1_1(a1324) | ~c1_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['95'])).
% 190.75/25.06 cnf('97', plain, (~$pr(hskp11) | ~c1_1(a1324)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('98', plain, (~c1_1(a1324) | ~c1_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['84','97'])).
% 190.75/25.06 cnf('99', plain, (~c1_1(X) | ~c1_1(Y) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(Z) | c1_1(U) | c2_1(Z) | c2_1(X) | c2_1(U) | c2_1(Y) | c3_1(Z) | c3_1(U)),
% 190.75/25.06 inference(resolution,[],['96','98'])).
% 190.75/25.06 cnf('100', plain, (~c1_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c1_1(Z) | c2_1(Y) | c2_1(Z) | c2_1(X) | c3_1(Y) | c3_1(Z)),
% 190.75/25.06 inference(factorization,[],['99'])).
% 190.75/25.06 cnf('101', plain, (~c1_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['100'])).
% 190.75/25.06 cnf('102', plain, (~c3_1(a1325) | c2_1(a1325) | c0_1(a1325) | c0_1(X) | c1_1(Y) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['82','101'])).
% 190.75/25.06 cnf('103', plain, (~c3_1(a1325) | c2_1(a1325) | c0_1(a1325) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['102'])).
% 190.75/25.06 cnf('104', plain, (~$pr(hskp12) | c3_1(a1325)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('105', plain, (c3_1(a1325) | $pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['104','71'])).
% 190.75/25.06 cnf('106', plain, (c2_1(a1325) | c0_1(a1325) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3) | $pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['103','105'])).
% 190.75/25.06 cnf('107', plain, (~$pr(hskp12) | ~c0_1(a1325)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('108', plain, (~c0_1(a1325) | $pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['107','71'])).
% 190.75/25.06 cnf('109', plain, (c2_1(a1325) | $pr(hskp26) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['106','108'])).
% 190.75/25.06 cnf('110', plain, (~c3_1(a1325) | c0_1(a1325) | $pr(hskp26) | c0_1(Y3) | c0_1(X3) | c1_1(X3) | c2_1(Y3) | c2_1(X3) | c3_1(Y3) | c3_1(X3)),
% 190.75/25.06 inference(resolution,[],['109','48'])).
% 190.75/25.06 cnf('111', plain, (c3_1(a1325) | $pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['104','71'])).
% 190.75/25.06 cnf('112', plain, (c0_1(a1325) | $pr(hskp26) | c0_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[],['110','111'])).
% 190.75/25.06 cnf('113', plain, (c0_1(a1325) | $pr(hskp26) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3)),
% 190.75/25.06 inference(factorization,[],['112'])).
% 190.75/25.06 cnf('114', plain, ($pr(hskp26) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['113','108'])).
% 190.75/25.06 cnf('115', plain, (c0_1(a1411) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['114','73'])).
% 190.75/25.06 cnf('116', plain, (c2_1(a1411) | c3_1(a1411) | c0_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['115','69'])).
% 190.75/25.06 cnf('117', plain, (c2_1(a1411) | c3_1(a1411) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['116'])).
% 190.75/25.06 cnf('118', plain, (c3_1(a1411) | c0_1(X3) | c1_1(X3) | c2_1(X3) | c3_1(X3) | ~$pr(hskp26)),
% 190.75/25.06 inference(resolution,[],['117','79'])).
% 190.75/25.06 cnf('119', plain, (~$pr(hskp26) | ~c3_1(a1411)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('120', plain, (~$pr(hskp26) | c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['118','119'])).
% 190.75/25.06 cnf('121', plain, (c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['120','114'])).
% 190.75/25.06 cnf('122', plain, (c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['121'])).
% 190.75/25.06 cnf('123', plain, (~c0_1(a1316) | ~$pr(hskp7)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('124', plain, (~$pr(hskp7) | c1_1(a1316) | c2_1(a1316) | c3_1(a1316)),
% 190.75/25.06 inference(resolution,[],['122','123'])).
% 190.75/25.06 cnf('125', plain, (~c2_1(a1316) | ~$pr(hskp7)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('126', plain, (~$pr(hskp7) | c1_1(a1316) | c3_1(a1316)),
% 190.75/25.06 inference(simplify,[],['124','125'])).
% 190.75/25.06 cnf('127', plain, (~$pr(ndr1_0) | $pr(hskp7) | $pr(hskp8) | ~c0_1(X0) | c1_1(X0) | c2_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('128', plain, ($pr(hskp7) | $pr(hskp8) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(simplify,[],['127','6'])).
% 190.75/25.06 cnf('129', plain, (c1_1(a1316) | c3_1(a1316) | $pr(hskp8) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['126','128'])).
% 190.75/25.06 cnf('130', plain, (~c0_1(a1316) | c1_1(a1316) | c2_1(a1316) | c3_1(a1316) | $pr(hskp8)),
% 190.75/25.06 inference(factorization,[],['129'])).
% 190.75/25.06 cnf('131', plain, (c1_1(a1316) | c2_1(a1316) | c3_1(a1316) | $pr(hskp8)),
% 190.75/25.06 inference(resolution,[],['130','122'])).
% 190.75/25.06 cnf('132', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp9) | ~c1_1(X1) | ~c1_1(X0) | c0_1(X1) | c0_1(X0) | c2_1(X1) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('133', plain, ($pr(hskp9) | ~c1_1(X) | ~c1_1(Y) | c0_1(X) | c0_1(Y) | c2_1(X) | c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['132','6','6'])).
% 190.75/25.06 cnf('134', plain, ($pr(hskp9) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['133'])).
% 190.75/25.06 cnf('135', plain, (c2_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['134','51'])).
% 190.75/25.06 cnf('136', plain, (~c3_1(a1320) | c0_1(a1320) | ~c1_1(X) | c0_1(X) | c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['48','135'])).
% 190.75/25.06 cnf('137', plain, (~c3_1(a1320) | c0_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['136'])).
% 190.75/25.06 cnf('138', plain, (c0_1(a1320) | c3_1(a1320) | c1_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['135','37'])).
% 190.75/25.06 cnf('139', plain, (c3_1(a1320) | c1_1(a1320) | ~c1_1(X3) | c0_1(X3) | c2_1(X3) | c3_1(X3) | ~$pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['138','57'])).
% 190.75/25.06 cnf('140', plain, (~$pr(hskp9) | c3_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['139','59'])).
% 190.75/25.06 cnf('141', plain, (c3_1(a1320) | ~c1_1(X) | ~c1_1(Y) | c0_1(X) | c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['140','134'])).
% 190.75/25.06 cnf('142', plain, (c3_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['141'])).
% 190.75/25.06 cnf('143', plain, (c0_1(a1320) | ~c1_1(X) | ~c1_1(Y) | c0_1(X) | c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['137','142'])).
% 190.75/25.06 cnf('144', plain, (c0_1(a1320) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['143'])).
% 190.75/25.06 cnf('145', plain, (~$pr(hskp9) | ~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['144','57'])).
% 190.75/25.06 cnf('146', plain, (~c1_1(X) | ~c1_1(Y) | c0_1(X) | c0_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['145','134'])).
% 190.75/25.06 cnf('147', plain, (~c1_1(X) | c0_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['146'])).
% 190.75/25.06 cnf('148', plain, (c2_1(a1316) | c0_1(a1316) | c3_1(a1316) | $pr(hskp8)),
% 190.75/25.06 inference(resolution,[],['131','147'])).
% 190.75/25.06 cnf('149', plain, (~c2_1(a1316) | ~$pr(hskp7)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('150', plain, (c0_1(a1316) | c3_1(a1316) | $pr(hskp8) | ~$pr(hskp7)),
% 190.75/25.06 inference(resolution,[],['148','149'])).
% 190.75/25.06 cnf('151', plain, (~c0_1(a1316) | ~$pr(hskp7)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('152', plain, (~$pr(hskp7) | c3_1(a1316) | $pr(hskp8)),
% 190.75/25.06 inference(simplify,[],['150','151'])).
% 190.75/25.06 cnf('153', plain, (~c3_1(a1316) | ~$pr(hskp7)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('154', plain, (~$pr(hskp7) | $pr(hskp8)),
% 190.75/25.06 inference(simplify,[],['152','153'])).
% 190.75/25.06 cnf('155', plain, ($pr(hskp8) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['154','128'])).
% 190.75/25.06 cnf('156', plain, (~c0_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['155','46'])).
% 190.75/25.06 cnf('157', plain, (~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['156','122'])).
% 190.75/25.06 cnf('158', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp17) | ~c0_1(X1) | ~c1_1(X1) | ~c1_1(X0) | ~c2_1(X1) | ~c2_1(X0) | ~c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('159', plain, ($pr(hskp17) | ~c0_1(X) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(Y)),
% 190.75/25.06 inference(simplify,[then_simplify],['158','6','6'])).
% 190.75/25.06 cnf('160', plain, ($pr(hskp17) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X)),
% 190.75/25.06 inference(factorization,[],['159'])).
% 190.75/25.06 cnf('161', plain, (~$pr(hskp17) | c2_1(a1334)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('162', plain, (c2_1(a1334) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X)),
% 190.75/25.06 inference(resolution,[],['160','161'])).
% 190.75/25.06 cnf('163', plain, (~c3_1(a1334) | c0_1(a1334) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['157','162'])).
% 190.75/25.06 cnf('164', plain, (~$pr(hskp17) | c3_1(a1334)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('165', plain, (c3_1(a1334) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X)),
% 190.75/25.06 inference(resolution,[],['160','164'])).
% 190.75/25.06 cnf('166', plain, (c0_1(a1334) | ~c0_1(X) | ~c0_1(Y) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c1_1(Z) | c2_1(Z) | c3_1(Z)),
% 190.75/25.06 inference(resolution,[],['163','165'])).
% 190.75/25.06 cnf('167', plain, (c0_1(a1334) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['166'])).
% 190.75/25.06 cnf('168', plain, (~$pr(hskp17) | ~c0_1(a1334)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('169', plain, (~c0_1(a1334) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X)),
% 190.75/25.06 inference(resolution,[],['160','168'])).
% 190.75/25.06 cnf('170', plain, (~c0_1(X) | ~c0_1(Y) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c1_1(Z) | c2_1(Z) | c3_1(Z)),
% 190.75/25.06 inference(resolution,[],['167','169'])).
% 190.75/25.06 cnf('171', plain, (~c0_1(X) | ~c1_1(X) | ~c2_1(X) | ~c3_1(X) | c1_1(Y) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(factorization,[],['170'])).
% 190.75/25.06 cnf('172', plain, (~$pr(ndr1_0) | $pr(hskp18) | $pr(hskp29) | ~c0_1(X0) | c1_1(X0) | c2_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('173', plain, ($pr(hskp18) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(simplify,[],['172','6'])).
% 190.75/25.06 cnf('174', plain, (~$pr(hskp18) | c1_1(a1339)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('175', plain, (c1_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['173','174'])).
% 190.75/25.06 cnf('176', plain, (c2_1(a1339) | c0_1(a1339) | $pr(hskp29) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['147','175'])).
% 190.75/25.06 cnf('177', plain, (~$pr(hskp18) | ~c2_1(a1339)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('178', plain, (~c2_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['173','177'])).
% 190.75/25.06 cnf('179', plain, (c0_1(a1339) | $pr(hskp29) | c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y)),
% 190.75/25.06 inference(resolution,[],['176','178'])).
% 190.75/25.06 cnf('180', plain, (c0_1(a1339) | $pr(hskp29) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(factorization,[],['179'])).
% 190.75/25.06 cnf('181', plain, (~$pr(hskp18) | ~c0_1(a1339)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('182', plain, (~c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['173','181'])).
% 190.75/25.06 cnf('183', plain, ($pr(hskp29) | c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y)),
% 190.75/25.06 inference(resolution,[],['180','182'])).
% 190.75/25.06 cnf('184', plain, ($pr(hskp29) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(factorization,[],['183'])).
% 190.75/25.06 cnf('185', plain, (~$pr(hskp29) | c2_1(a1338)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('186', plain, (c2_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['184','185'])).
% 190.75/25.06 cnf('187', plain, (~c3_1(a1338) | c0_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['157','186'])).
% 190.75/25.06 cnf('188', plain, (~c3_1(a1338) | c0_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['187'])).
% 190.75/25.06 cnf('189', plain, (~$pr(hskp29) | c3_1(a1338)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('190', plain, (c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['184','189'])).
% 190.75/25.06 cnf('191', plain, (c0_1(a1338) | c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['188','190'])).
% 190.75/25.06 cnf('192', plain, (c0_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['191'])).
% 190.75/25.06 cnf('193', plain, (~c1_1(a1338) | ~c2_1(a1338) | ~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['171','192'])).
% 190.75/25.06 cnf('194', plain, (~c1_1(a1338) | ~c2_1(a1338) | ~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['193'])).
% 190.75/25.06 cnf('195', plain, (~$pr(hskp29) | c1_1(a1338)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('196', plain, (c1_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['184','195'])).
% 190.75/25.06 cnf('197', plain, (~c2_1(a1338) | ~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['194','196'])).
% 190.75/25.06 cnf('198', plain, (~c2_1(a1338) | ~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['197'])).
% 190.75/25.06 cnf('199', plain, (~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['198','186'])).
% 190.75/25.06 cnf('200', plain, (~c3_1(a1338) | c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['199'])).
% 190.75/25.06 cnf('201', plain, (c3_1(a1339) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['200','190'])).
% 190.75/25.06 cnf('202', plain, (c3_1(a1339) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['201'])).
% 190.75/25.06 cnf('203', plain, (~c3_1(a1339) | c2_1(a1339) | c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['101','175'])).
% 190.75/25.06 cnf('204', plain, (~c3_1(a1339) | c2_1(a1339) | c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['203'])).
% 190.75/25.06 cnf('205', plain, (c2_1(a1339) | c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['202','204'])).
% 190.75/25.06 cnf('206', plain, (c2_1(a1339) | c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['205'])).
% 190.75/25.06 cnf('207', plain, (c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['206','178'])).
% 190.75/25.06 cnf('208', plain, (c0_1(a1339) | $pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['207'])).
% 190.75/25.06 cnf('209', plain, ($pr(hskp29) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['208','182'])).
% 190.75/25.06 cnf('210', plain, ($pr(hskp29) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['209'])).
% 190.75/25.06 cnf('211', plain, (c2_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['210','185'])).
% 190.75/25.06 cnf('212', plain, (~c3_1(a1338) | c0_1(a1338) | ~c0_1(X) | c1_1(Y) | c1_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['211','157'])).
% 190.75/25.06 cnf('213', plain, (~c3_1(a1338) | c0_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['212'])).
% 190.75/25.06 cnf('214', plain, (c3_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['210','189'])).
% 190.75/25.06 cnf('215', plain, (c0_1(a1338) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['213','214'])).
% 190.75/25.06 cnf('216', plain, (c0_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['215'])).
% 190.75/25.06 cnf('217', plain, (~c1_1(a1338) | ~c2_1(a1338) | ~c3_1(a1338) | ~c0_1(X) | c1_1(Y) | c1_1(X) | c2_1(Y) | c2_1(X) | c3_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['216','171'])).
% 190.75/25.06 cnf('218', plain, (~c1_1(a1338) | ~c2_1(a1338) | ~c3_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['217'])).
% 190.75/25.06 cnf('219', plain, (c1_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['210','195'])).
% 190.75/25.06 cnf('220', plain, (~c2_1(a1338) | ~c3_1(a1338) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['218','219'])).
% 190.75/25.06 cnf('221', plain, (~c2_1(a1338) | ~c3_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['220'])).
% 190.75/25.06 cnf('222', plain, (~c3_1(a1338) | ~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['221','211'])).
% 190.75/25.06 cnf('223', plain, (~c3_1(a1338) | ~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['222'])).
% 190.75/25.06 cnf('224', plain, (~c0_1(X) | ~c0_1(Y) | c1_1(X) | c1_1(Y) | c2_1(X) | c2_1(Y) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['223','214'])).
% 190.75/25.06 cnf('225', plain, (~c0_1(X) | c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['224'])).
% 190.75/25.06 cnf('226', plain, (c1_1(X) | c2_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['225','122'])).
% 190.75/25.06 cnf('227', plain, (~$pr(ndr1_0) | $pr(hskp13) | ~c0_1(X0) | ~c1_1(X0) | ~c2_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('228', plain, ($pr(hskp13) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X)),
% 190.75/25.06 inference(simplify,[],['227','6'])).
% 190.75/25.06 cnf('229', plain, (~$pr(hskp13) | ~c1_1(a1326)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('230', plain, (~c1_1(a1326) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X)),
% 190.75/25.06 inference(resolution,[],['228','229'])).
% 190.75/25.06 cnf('231', plain, (c2_1(a1326) | c3_1(a1326) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X)),
% 190.75/25.06 inference(resolution,[],['226','230'])).
% 190.75/25.06 cnf('232', plain, (~c2_1(a1326) | ~$pr(hskp13)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('233', plain, (c3_1(a1326) | ~c0_1(X3) | ~c1_1(X3) | ~c2_1(X3) | ~$pr(hskp13)),
% 190.75/25.06 inference(resolution,[],['231','232'])).
% 190.75/25.06 cnf('234', plain, (~$pr(hskp13) | ~c3_1(a1326)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('235', plain, (~$pr(hskp13) | ~c0_1(X) | ~c1_1(X) | ~c2_1(X)),
% 190.75/25.06 inference(simplify,[],['233','234'])).
% 190.75/25.06 cnf('236', plain, (~c0_1(X) | ~c0_1(Y) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(X) | ~c2_1(Y)),
% 190.75/25.06 inference(resolution,[],['235','228'])).
% 190.75/25.06 cnf('237', plain, (~c0_1(X) | ~c1_1(X) | ~c2_1(X)),
% 190.75/25.06 inference(factorization,[],['236'])).
% 190.75/25.06 cnf('238', plain, ($pr(hskp30) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('239', plain, (~$pr(hskp30) | c0_1(a1372)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('240', plain, (c0_1(a1372) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['238','239'])).
% 190.75/25.06 cnf('241', plain, (~c1_1(a1372) | ~c2_1(a1372) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['237','240'])).
% 190.75/25.06 cnf('242', plain, (~$pr(hskp30) | c1_1(a1372)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('243', plain, (c1_1(a1372) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['238','242'])).
% 190.75/25.06 cnf('244', plain, (~c2_1(a1372) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['241','243'])).
% 190.75/25.06 cnf('245', plain, (~$pr(ndr1_0) | ~$pr(ndr1_0) | $pr(hskp7) | ~c1_1(X0) | ~c3_1(X1) | ~c3_1(X0) | c0_1(X1) | c1_1(X1) | c2_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('246', plain, ($pr(hskp7) | ~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 190.75/25.06 inference(simplify,[then_simplify],['245','6','6'])).
% 190.75/25.06 cnf('247', plain, (c1_1(a1316) | c3_1(a1316) | ~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['126','246'])).
% 190.75/25.06 cnf('248', plain, (c2_1(a1316) | c0_1(a1316) | c3_1(a1316) | ~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 190.75/25.06 inference(resolution,[],['247','147'])).
% 190.75/25.06 cnf('249', plain, (c0_1(a1316) | c3_1(a1316) | ~c1_1(X3) | ~c3_1(Y3) | ~c3_1(X3) | c0_1(Y3) | c1_1(Y3) | c2_1(X3) | ~$pr(hskp7)),
% 190.75/25.06 inference(resolution,[],['248','149'])).
% 190.75/25.06 cnf('250', plain, (~$pr(hskp7) | c3_1(a1316) | ~c1_1(Z3) | ~c3_1(U3) | ~c3_1(Z3) | c0_1(U3) | c1_1(U3) | c2_1(Z3)),
% 190.75/25.06 inference(simplify,[],['249','151'])).
% 190.75/25.06 cnf('251', plain, (~$pr(hskp7) | ~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 190.75/25.06 inference(simplify,[],['250','153'])).
% 190.75/25.06 cnf('252', plain, (~c1_1(X) | ~c1_1(Y) | ~c3_1(Z) | ~c3_1(X) | ~c3_1(U) | ~c3_1(Y) | c0_1(Z) | c0_1(U) | c1_1(Z) | c1_1(U) | c2_1(X) | c2_1(Y)),
% 190.75/25.06 inference(resolution,[],['251','246'])).
% 190.75/25.06 cnf('253', plain, (~c1_1(X) | ~c3_1(Y) | ~c3_1(Z) | ~c3_1(X) | c0_1(Y) | c0_1(Z) | c1_1(Y) | c1_1(Z) | c2_1(X)),
% 190.75/25.06 inference(factorization,[],['252'])).
% 190.75/25.06 cnf('254', plain, (~c1_1(X) | ~c3_1(Y) | ~c3_1(X) | c0_1(Y) | c1_1(Y) | c2_1(X)),
% 190.75/25.06 inference(factorization,[],['253'])).
% 190.75/25.06 cnf('255', plain, (~c3_1(a1372) | c2_1(a1372) | $pr(hskp2) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['254','243'])).
% 190.75/25.06 cnf('256', plain, (~$pr(hskp30) | c3_1(a1372)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('257', plain, (c3_1(a1372) | $pr(hskp2) | $pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['238','256'])).
% 190.75/25.06 cnf('258', plain, (c2_1(a1372) | $pr(hskp2) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['255','257'])).
% 190.75/25.06 cnf('259', plain, ($pr(hskp2) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['244','258'])).
% 190.75/25.06 cnf('260', plain, (~$pr(hskp2) | c1_1(a1309)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('261', plain, (c1_1(a1309) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['259','260'])).
% 190.75/25.06 cnf('262', plain, (~c3_1(a1309) | c2_1(a1309) | $pr(hskp9) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['261','254'])).
% 190.75/25.06 cnf('263', plain, (~c3_1(a1309) | c2_1(a1309) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['262'])).
% 190.75/25.06 cnf('264', plain, (~$pr(hskp2) | c3_1(a1309)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('265', plain, (c3_1(a1309) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['259','264'])).
% 190.75/25.06 cnf('266', plain, (c2_1(a1309) | $pr(hskp9) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['263','265'])).
% 190.75/25.06 cnf('267', plain, (c2_1(a1309) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['266'])).
% 190.75/25.06 cnf('268', plain, (~c2_1(a1309) | ~$pr(hskp2)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('269', plain, (~$pr(hskp2) | $pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['267','268'])).
% 190.75/25.06 cnf('270', plain, ($pr(hskp9) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['269','259'])).
% 190.75/25.06 cnf('271', plain, ($pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['270'])).
% 190.75/25.06 cnf('272', plain, (c2_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['271','51'])).
% 190.75/25.06 cnf('273', plain, (c0_1(a1320) | c3_1(a1320) | c1_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['272','37'])).
% 190.75/25.06 cnf('274', plain, (c3_1(a1320) | c1_1(a1320) | ~c3_1(X3) | c0_1(X3) | c1_1(X3) | ~$pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['273','57'])).
% 190.75/25.06 cnf('275', plain, (~$pr(hskp9) | c3_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(simplify,[],['274','59'])).
% 190.75/25.06 cnf('276', plain, (c3_1(a1320) | ~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['275','271'])).
% 190.75/25.06 cnf('277', plain, (c3_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['276'])).
% 190.75/25.06 cnf('278', plain, (~$pr(ndr1_0) | $pr(hskp14) | $pr(hskp8) | ~c0_1(X0) | ~c1_1(X0) | c3_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('279', plain, ($pr(hskp14) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | c3_1(X)),
% 190.75/25.06 inference(simplify,[],['278','6'])).
% 190.75/25.06 cnf('280', plain, (~$pr(hskp14) | c0_1(a1330)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('281', plain, (c0_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['279','280'])).
% 190.75/25.06 cnf('282', plain, (c1_1(a1330) | c2_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['156','281'])).
% 190.75/25.06 cnf('283', plain, (~$pr(hskp14) | ~c1_1(a1330)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('284', plain, (~c1_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['279','283'])).
% 190.75/25.06 cnf('285', plain, (c2_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c0_1(Y) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(Z) | ~c3_1(Z) | c0_1(Z) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['282','284'])).
% 190.75/25.06 cnf('286', plain, (c2_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['285'])).
% 190.75/25.06 cnf('287', plain, (~$pr(hskp14) | ~c2_1(a1330)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('288', plain, (~c2_1(a1330) | $pr(hskp8) | ~c0_1(X) | ~c1_1(X) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['279','287'])).
% 190.75/25.06 cnf('289', plain, ($pr(hskp8) | ~c0_1(X) | ~c0_1(Y) | ~c1_1(X) | ~c1_1(Y) | ~c2_1(Z) | ~c3_1(Z) | c0_1(Z) | c3_1(X) | c3_1(Y)),
% 190.75/25.06 inference(resolution,[],['286','288'])).
% 190.75/25.06 cnf('290', plain, ($pr(hskp8) | ~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['289'])).
% 190.75/25.06 cnf('291', plain, (~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c2_1(Z) | ~c3_1(Y) | ~c3_1(Z) | c0_1(Y) | c0_1(Z) | c3_1(X)),
% 190.75/25.06 inference(resolution,[],['290','46'])).
% 190.75/25.06 cnf('292', plain, (~c0_1(X) | ~c1_1(X) | ~c2_1(Y) | ~c3_1(Y) | c0_1(Y) | c3_1(X)),
% 190.75/25.06 inference(factorization,[],['291'])).
% 190.75/25.06 cnf('293', plain, (~c0_1(a1359) | ~$pr(hskp23)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('294', plain, (~$pr(hskp23) | c3_1(a1359) | c1_1(a1359) | c2_1(a1359)),
% 190.75/25.06 inference(resolution,[],['122','293'])).
% 190.75/25.06 cnf('295', plain, (~c3_1(a1359) | ~$pr(hskp23)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('296', plain, (~$pr(hskp23) | c1_1(a1359) | c2_1(a1359)),
% 190.75/25.06 inference(simplify,[],['294','295'])).
% 190.75/25.06 cnf('297', plain, (~$pr(ndr1_0) | $pr(hskp23) | $pr(hskp22) | ~c2_1(X0) | ~c3_1(X0) | c1_1(X0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('298', plain, ($pr(hskp23) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(simplify,[],['297','6'])).
% 190.75/25.06 cnf('299', plain, (c1_1(a1359) | c2_1(a1359) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['296','298'])).
% 190.75/25.06 cnf('300', plain, (~c1_1(a1359) | ~$pr(hskp23)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('301', plain, (~$pr(hskp23) | c2_1(a1359) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['299','300'])).
% 190.75/25.06 cnf('302', plain, (c2_1(a1359) | $pr(hskp22) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['301','298'])).
% 190.75/25.06 cnf('303', plain, (c2_1(a1359) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['302'])).
% 190.75/25.06 cnf('304', plain, (c0_1(a1359) | c3_1(a1359) | c1_1(a1359) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['303','37'])).
% 190.75/25.06 cnf('305', plain, (c3_1(a1359) | c1_1(a1359) | $pr(hskp22) | ~c2_1(X3) | ~c3_1(X3) | c1_1(X3) | ~$pr(hskp23)),
% 190.75/25.06 inference(resolution,[],['304','293'])).
% 190.75/25.06 cnf('306', plain, (~$pr(hskp23) | c1_1(a1359) | $pr(hskp22) | ~c2_1(Y3) | ~c3_1(Y3) | c1_1(Y3)),
% 190.75/25.06 inference(simplify,[],['305','295'])).
% 190.75/25.06 cnf('307', plain, (~c1_1(a1359) | ~$pr(hskp23)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('308', plain, (~$pr(hskp23) | $pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(simplify,[],['306','307'])).
% 190.75/25.06 cnf('309', plain, ($pr(hskp22) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['308','298'])).
% 190.75/25.06 cnf('310', plain, ($pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['309'])).
% 190.75/25.06 cnf('311', plain, (~$pr(hskp22) | c0_1(a1356)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('312', plain, (c0_1(a1356) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['310','311'])).
% 190.75/25.06 cnf('313', plain, (~c1_1(a1356) | c3_1(a1356) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(Y) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['292','312'])).
% 190.75/25.06 cnf('314', plain, (~c1_1(a1356) | c3_1(a1356) | ~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['313'])).
% 190.75/25.06 cnf('315', plain, (~$pr(hskp22) | c1_1(a1356)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('316', plain, (c1_1(a1356) | ~c2_1(X) | ~c3_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['310','315'])).
% 190.75/25.06 cnf('317', plain, (c3_1(a1356) | ~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['314','316'])).
% 190.75/25.06 cnf('318', plain, (c3_1(a1356) | ~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['317'])).
% 190.75/25.06 cnf('319', plain, (~c3_1(a1356) | ~$pr(hskp22)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('320', plain, (~$pr(hskp22) | ~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['318','319'])).
% 190.75/25.06 cnf('321', plain, (~c2_1(X) | ~c2_1(Y) | ~c3_1(X) | ~c3_1(Y) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['320','310'])).
% 190.75/25.06 cnf('322', plain, (~c2_1(X) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['321'])).
% 190.75/25.06 cnf('323', plain, (~c3_1(a1320) | c0_1(a1320) | c1_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['272','322'])).
% 190.75/25.06 cnf('324', plain, (~c3_1(a1320) | c0_1(a1320) | c1_1(a1320)),
% 190.75/25.06 inference(factorization,[],['323'])).
% 190.75/25.06 cnf('325', plain, (c0_1(a1320) | c1_1(a1320) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(resolution,[],['277','324'])).
% 190.75/25.06 cnf('326', plain, (c1_1(a1320) | ~c3_1(X3) | c0_1(X3) | c1_1(X3) | ~$pr(hskp9)),
% 190.75/25.06 inference(resolution,[],['325','57'])).
% 190.75/25.06 cnf('327', plain, (~$pr(hskp9) | ~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(simplify,[],['326','59'])).
% 190.75/25.06 cnf('328', plain, (~c3_1(X) | ~c3_1(Y) | c0_1(X) | c0_1(Y) | c1_1(X) | c1_1(Y)),
% 190.75/25.06 inference(resolution,[],['327','271'])).
% 190.75/25.06 cnf('329', plain, (~c3_1(X) | c0_1(X) | c1_1(X)),
% 190.75/25.06 inference(factorization,[],['328'])).
% 190.75/25.06 cnf('330', plain, ($pr(hskp23) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('331', plain, (c1_1(a1359) | c2_1(a1359) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['296','330'])).
% 190.75/25.06 cnf('332', plain, (~$pr(hskp23) | c2_1(a1359) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['331','300'])).
% 190.75/25.06 cnf('333', plain, (c2_1(a1359) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['332','330'])).
% 190.75/25.06 cnf('334', plain, (c0_1(a1359) | c3_1(a1359) | c1_1(a1359) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['333','37'])).
% 190.75/25.06 cnf('335', plain, (c3_1(a1359) | c1_1(a1359) | $pr(hskp0) | $pr(hskp6) | ~$pr(hskp23)),
% 190.75/25.06 inference(resolution,[],['334','293'])).
% 190.75/25.06 cnf('336', plain, (~$pr(hskp23) | c1_1(a1359) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['335','295'])).
% 190.75/25.06 cnf('337', plain, (~$pr(hskp23) | $pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['336','307'])).
% 190.75/25.06 cnf('338', plain, ($pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['337','330'])).
% 190.75/25.06 cnf('339', plain, (~c0_1(a1306) | ~$pr(hskp0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('340', plain, (~$pr(hskp0) | c1_1(a1306) | c2_1(a1306) | c3_1(a1306)),
% 190.75/25.06 inference(resolution,[],['122','339'])).
% 190.75/25.06 cnf('341', plain, (~c1_1(a1306) | ~$pr(hskp0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('342', plain, (~$pr(hskp0) | c2_1(a1306) | c3_1(a1306)),
% 190.75/25.06 inference(simplify,[],['340','341'])).
% 190.75/25.06 cnf('343', plain, (c2_1(a1306) | c3_1(a1306) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['338','342'])).
% 190.75/25.06 cnf('344', plain, (~c2_1(a1306) | ~$pr(hskp0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('345', plain, (c3_1(a1306) | $pr(hskp6) | ~$pr(hskp0)),
% 190.75/25.06 inference(resolution,[],['343','344'])).
% 190.75/25.06 cnf('346', plain, ($pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['337','330'])).
% 190.75/25.06 cnf('347', plain, (c3_1(a1306) | $pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['345','346'])).
% 190.75/25.06 cnf('348', plain, (c1_1(a1306) | c0_1(a1306) | $pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['329','347'])).
% 190.75/25.06 cnf('349', plain, (~c1_1(a1306) | ~$pr(hskp0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('350', plain, (c0_1(a1306) | $pr(hskp6) | ~$pr(hskp0)),
% 190.75/25.06 inference(resolution,[],['348','349'])).
% 190.75/25.06 cnf('351', plain, (~c0_1(a1306) | ~$pr(hskp0)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('352', plain, (~$pr(hskp0) | $pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['350','351'])).
% 190.75/25.06 cnf('353', plain, ($pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['352','346'])).
% 190.75/25.06 cnf('354', plain, (~$pr(hskp6) | c3_1(a1315)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('355', plain, (c3_1(a1315)),
% 190.75/25.06 inference(resolution,[],['353','354'])).
% 190.75/25.06 cnf('356', plain, (c1_1(a1315) | c0_1(a1315)),
% 190.75/25.06 inference(resolution,[],['355','329'])).
% 190.75/25.06 cnf('357', plain, (~c1_1(a1315) | ~$pr(hskp6)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('358', plain, (c0_1(a1315) | ~$pr(hskp6)),
% 190.75/25.06 inference(resolution,[],['356','357'])).
% 190.75/25.06 cnf('359', plain, (~c0_1(a1315) | ~$pr(hskp6)),
% 190.75/25.06 inference(cnf_transformation,[],['co1_$sk'])).
% 190.75/25.06 cnf('360', plain, (~$pr(hskp6)),
% 190.75/25.06 inference(simplify,[],['358','359'])).
% 190.75/25.06 cnf('361', plain, ($false),
% 190.75/25.06 inference(resolution,[],['360','353'])).
% 190.75/25.06
% 190.75/25.06 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 190.75/25.06
% 190.75/25.06 run 108 fork 3 statistics:
% 190.75/25.06 ----------------------------------
% 190.75/25.06 this run seconds: 9.670826
% 190.75/25.06 total seconds: 23.328953
% 190.75/25.06 stat_given_used: 10153
% 190.75/25.06 stat_given_used_at_endgame: 0
% 190.75/25.06 stat_given_candidates: 104315
% 190.75/25.06 stat_given_candidates_at_endgame: 0
% 190.75/25.06 stat_given_candidates_h: 0
% 190.75/25.06 stat_binres_derived_cl: 576690
% 190.75/25.06 stat_binres_derived_cl_h: 0
% 190.75/25.06 stat_factor_derived_cl: 26146
% 190.75/25.06 stat_para_derived_cl: 0
% 190.75/25.06 stat_tautologies_discarded: 100685
% 190.75/25.06 stat_forward_subsumed: 261
% 190.75/25.06 stat_derived_cut: 32646
% 190.75/25.06 stat_derived_rewritten: 0
% 190.75/25.06 stat_weight_discarded_building: 0
% 190.75/25.06 stat_weight_discarded_cl: 0
% 190.75/25.06 stat_internlimit_discarded_cl: 0
% 190.75/25.06 stat_simplified: 32632 simplified 0 derived 0 given
% 190.75/25.06 stat_kept_cl: 501889
% 190.75/25.06 stat_built_cl: 554827
% 190.75/25.06 stat_hyperres_partial_cl: 0
% 190.75/25.06 stat_made_rewriters: 0
% 190.75/25.06 stat_backward_subsumed: 0
% 190.75/25.06 stat_propagated_subsumed: 0
% 190.75/25.06 stat_clsubs_attempted: 1353318
% 190.75/25.06 stat_clsubs_fact_groundunit_found: 1
% 190.75/25.06 stat_clsubs_rule_groundunit_found: 0
% 190.75/25.06 stat_clsubs_top_meta_attempted: 365847089
% 190.75/25.06 stat_clsubs_top_meta_failed: 364493771
% 190.75/25.06 stat_clsubs_top_meta_nonpref_attempted: 365847089
% 190.75/25.06 stat_clsubs_top_meta_nonpref_succeeded: 80449616
% 190.75/25.06 stat_clsubs_top_meta_pref_attempted: 80449616
% 190.75/25.06 stat_clsubs_top_meta_pref1_succeeded: 20904243
% 190.75/25.06 stat_clsubs_top_meta_pref2_succeeded: 1353318
% 190.75/25.06 stat_clsubs_top_meta_pref3_succeeded: 1353318
% 190.75/25.06 stat_clsubs_top_meta_pref_succeeded: 1353318
% 190.75/25.06 stat_clsubs_meta_attempted: 19800575
% 190.75/25.06 stat_clsubs_meta_failed: 9647205
% 190.75/25.06 stat_clsubs_predsymbs_attempted: 0
% 190.75/25.06 stat_clsubs_unit_attempted: 0
% 190.75/25.06 stat_clsubs_full_attempted: 1353318
% 190.75/25.06 stat_forwardsubs_attempted: 502150
% 190.75/25.06 stat_lit_hash_added: 327
% 190.75/25.06 stat_lit_hash_computed: 17006974
% 190.75/25.06 stat_lit_hash_match_found: 532
% 190.75/25.06 stat_lit_hash_match_miss: 23481912
% 190.75/25.06 stat_lit_hash_cut_ok: 32730
% 190.75/25.06 stat_lit_strong_cut_ok: 0
% 190.75/25.06 stat_lit_hash_subsume_ok: 261
% 190.75/25.06 clqueue els 10000000 used 1
% 190.75/25.06 clactive els 10000000 used 10154
% 190.75/25.06 clactivesubsume els 10000000 used 60895
% 190.75/25.06 queue_termbuf els 200000000 used 69878703
% 190.75/25.06 hyper_termbuf els 100000000 used 1
% 190.75/25.06 active_termbuf els 100000000 used 749486
% 190.75/25.06 varstack els 5000 last used 1
% 190.75/25.06 given_termbuf els 10000000 last used 13
% 190.75/25.06 simplified_termbuf els 10000000 last used 1
% 190.75/25.06 derived_termbuf els 10000000 last used 3
% 190.75/25.06 wr_mallocs: 20756
% 190.75/25.06 wr_callocs: 19
% 190.75/25.06 wr_reallocs: 400
% 190.75/25.06 wr_frees: 4
% 190.75/25.06 wr_malloc_bytes: 4163261156
% 190.75/25.06 wr_calloc_bytes: 96065504
% 190.75/25.06 wr_realloc_bytes: 10743992
% 190.75/25.06 wr_realloc_freebytes: 0
% 190.75/25.06 ----------------------------------
%------------------------------------------------------------------------------