%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : SWV569-1.030 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Aug 31 22:28:39 EDT 2023
% Result : Unsatisfiable 24.10s 3.55s
% Output : CNFRefutation 24.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV569-1.030 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.13 % Command : gkc %s
% 0.13/0.34 % Computer : n031.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Aug 29 10:06:41 EDT 2023
% 0.13/0.34 % CPUTime :
% 0.19/0.39
% 0.19/0.39 input clause set summed statistics:
% 0.19/0.39 ----------------------------------
% 0.19/0.39 in_clause_count: 302
% 0.19/0.39 in_rule_clause_count: 271
% 0.19/0.39 in_fact_clause_count: 31
% 0.19/0.39 in_answer_clause_count: 0
% 0.19/0.39 in_ground_clause_count: 250
% 0.19/0.39 in_unit_clause_count: 301
% 0.19/0.39 in_horn_clause_count: 301
% 0.19/0.39 in_pos_clause_count: 248
% 0.19/0.39 in_neg_clause_count: 54
% 0.19/0.39 in_poseq_clause_count: 248
% 0.19/0.39 in_negeq_clause_count: 54
% 0.19/0.39 in_unitposeq_clause_count: 247
% 0.19/0.39 in_chain_clause_count: 0
% 0.19/0.39 in_min_length: 1
% 0.19/0.39 in_max_length: 2
% 0.19/0.39 in_min_depth: 1
% 0.19/0.39 in_max_depth: 51
% 0.19/0.39 in_min_size: 3
% 0.19/0.39 in_max_size: 53
% 0.19/0.39 in_min_vars: 0
% 0.19/0.39 in_max_vars: 4
% 0.19/0.39 in_extaxiom_count: 0
% 0.19/0.39 in_axiom_count: 55
% 0.19/0.39 in_assumption_count: 246
% 0.19/0.39 in_goal_count: 1
% 0.19/0.39 in_neg_goal_count: 1
% 0.19/0.39 in_pos_goal_count: 0
% 0.19/0.39 in_posunit_goal_count: 0
% 0.19/0.39
% 0.19/0.39 auto guide:
% 0.19/0.39 -----------
% 0.19/0.39 {
% 0.19/0.39 "print":1,
% 0.19/0.39 "print_level": 15,
% 0.19/0.39 "max_size": 0,
% 0.19/0.39 "max_depth": 0,
% 0.19/0.39 "max_length": 0,
% 0.19/0.39 "max_dseconds": 0,
% 0.19/0.39 "runs":[
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":30, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref", "posunitpara"], "query_preference":1, "max_depth":2, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":1, "max_size":15},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":1, "strategy":["negative_pref"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "rewrite":0, "length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["hardness_pref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.19/0.39 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":1},
% 0.19/0.39 {"depth_penalty":50, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"depth_penalty":50, "sine":3, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "hornpref"], "max_dseconds":1},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["unit"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "weight_select_ratio":30, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"length_penalty":100, "query_preference":1, "strategy":["positive_pref", "posunitpara"], "max_dseconds":1},
% 0.19/0.39 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":1},
% 0.19/0.39 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref", "posunitpara"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit", "prohibit_nested_para"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"sine":1, "rewrite":0, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["hardness_pref", "posunitpara"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "equality":0},
% 0.19/0.39 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "length_penalty":100, "query_preference":1, "strategy":["query_focus", "prohibit_nested_para"], "max_dseconds":1},
% 0.19/0.39 {"query_preference":1, "strategy":["unit", "max_weight"], "max_dseconds":1},
% 0.19/0.39 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"sine":2, "weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.19/0.39
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":30, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref", "posunitpara"], "query_preference":1, "max_depth":2, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":10, "max_size":15},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":1, "strategy":["negative_pref"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "rewrite":0, "length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["hardness_pref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.19/0.39 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":10},
% 0.19/0.39 {"depth_penalty":50, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"depth_penalty":50, "sine":3, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "hornpref"], "max_dseconds":10},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["unit"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "weight_select_ratio":30, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"length_penalty":100, "query_preference":1, "strategy":["positive_pref", "posunitpara"], "max_dseconds":10},
% 0.19/0.39 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":10},
% 0.19/0.39 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref", "posunitpara"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit", "prohibit_nested_para"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "double"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"sine":1, "rewrite":0, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":10},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["hardness_pref", "posunitpara"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "equality":0},
% 0.19/0.39 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":10, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "length_penalty":100, "query_preference":1, "strategy":["query_focus", "prohibit_nested_para"], "max_dseconds":10},
% 0.19/0.39 {"query_preference":1, "strategy":["unit", "max_weight"], "max_dseconds":10},
% 0.19/0.39 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"sine":2, "weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus"], "max_dseconds":10},
% 0.19/0.39
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":30, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref", "posunitpara"], "query_preference":1, "max_depth":2, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":50, "max_size":15},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":1, "strategy":["negative_pref"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "rewrite":0, "length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["hardness_pref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.19/0.39 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "max_depth":2},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":50},
% 0.19/0.39 {"depth_penalty":50, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"depth_penalty":50, "sine":3, "query_preference":1, "strategy":["hardness_pref", "hornpref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "hornpref"], "max_dseconds":50},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["unit"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "weight_select_ratio":30, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"length_penalty":100, "query_preference":1, "strategy":["positive_pref", "posunitpara"], "max_dseconds":50},
% 0.19/0.39 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":50},
% 0.19/0.39 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref", "posunitpara"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "rewrite":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":50, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit", "prohibit_nested_para"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "double"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.19/0.39 {"sine":1, "var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":1, "strategy":["query_focus", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"sine":1, "rewrite":0, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":50},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["positive_pref", "unit"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["hardness_pref", "posunitpara"], "query_preference":1, "sine":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "equality":0},
% 0.19/0.39 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.19/0.39 {"max_dseconds":50, "strategy":["query_focus", "posunitpara"], "query_preference":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"var_weight":70, "repeat_var_weight":70, "length_penalty":100, "depth_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.19/0.39 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "length_penalty":100, "query_preference":1, "strategy":["query_focus", "prohibit_nested_para"], "max_dseconds":50},
% 0.19/0.39 {"query_preference":1, "strategy":["unit", "max_weight"], "max_dseconds":50},
% 0.19/0.39 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.19/0.39 {"sine":2, "weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":1, "strategy":["query_focus"], "max_dseconds":50},
% 0.19/0.39
% 0.19/0.39 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":3},
% 0.19/0.39 {"max_dseconds":250, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.19/0.39 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":30, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref", "posunitpara"], "query_preference":1, "max_depth":2, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.19/0.39 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":250, "strategy":["unit"], "query_preference":1, "max_depth":2},
% 0.19/0.39
% 0.19/0.39 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":3},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":30, "depth_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref", "posunitpara"], "query_preference":1, "max_depth":2, "depth_penalty":50, "length_penalty":100},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.19/0.39 {"max_dseconds":1250, "strategy":["unit"], "query_preference":1, "max_depth":2}
% 0.19/0.39
% 0.19/0.39 ]}
% 0.19/0.39
% 0.19/0.39
% 0.19/0.39 **** run 1 fork 0 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.19/0.39
% 0.19/0.39 **** run 2 fork 1 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"sine":3,"strategy":["hardness_pref"],"query_preference":0}
% 0.19/0.39
% 0.19/0.39 **** run 3 fork 2 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.19/0.39
% 0.19/0.39 **** run 4 fork 3 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.19/0.39
% 0.19/0.39 **** run 5 fork 4 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"strategy":["negative_pref","prohibit_unordered_para"],"query_preference":0}
% 0.19/0.39
% 0.19/0.39 **** run 7 fork 6 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para"],"query_preference":1}
% 0.19/0.39
% 0.19/0.39 **** run 6 fork 5 starts with strategy
% 0.19/0.39 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para"],"query_preference":0}
% 0.19/0.40
% 0.19/0.40 **** run 8 fork 7 starts with strategy
% 0.19/0.40 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 0.19/0.45
% 0.19/0.45 fork 1: search finished without proof.
% 0.19/0.49
% 0.19/0.49 **** run 10 fork 1 starts with strategy
% 0.19/0.49 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"],"query_preference":1}
% 0.19/0.52
% 0.19/0.52 fork 3: search finished without proof.
% 0.19/0.52
% 0.19/0.52 fork 2: search finished without proof.
% 0.19/0.52
% 0.19/0.52
% 0.19/0.52 fork 6: search terminated without proof.
% 0.19/0.52
% 0.19/0.52
% 0.19/0.52 fork 0: search terminated without proof.
% 0.19/0.52
% 0.19/0.52
% 0.19/0.52 fork 4: search terminated without proof.
% 0.19/0.53
% 0.19/0.53
% 0.19/0.53 fork 5: search terminated without proof.
% 0.19/0.54
% 0.19/0.54 **** run 11 fork 2 starts with strategy
% 0.19/0.54 {"max_dseconds":1,"strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"],"query_preference":0}
% 0.19/0.54
% 0.19/0.54 **** run 12 fork 3 starts with strategy
% 0.19/0.54 {"max_dseconds":1,"strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 0.19/0.55
% 0.19/0.55 **** run 15 fork 6 starts with strategy
% 0.19/0.55 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 0.19/0.55
% 0.19/0.55 **** run 9 fork 0 starts with strategy
% 0.19/0.55 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 0.19/0.55
% 0.19/0.55 **** run 13 fork 4 starts with strategy
% 0.19/0.55 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 0.19/0.55
% 0.19/0.55 **** run 14 fork 5 starts with strategy
% 0.19/0.55 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 0.19/0.57
% 0.19/0.57
% 0.19/0.57 fork 7: search terminated without proof.
% 0.19/0.59
% 0.19/0.59 **** run 16 fork 7 starts with strategy
% 0.19/0.59 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"depth_penalty":100}
% 0.19/0.62
% 0.19/0.62
% 0.19/0.62 fork 1: search terminated without proof.
% 0.19/0.63
% 0.19/0.63 **** run 18 fork 1 starts with strategy
% 0.19/0.64 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 0.19/0.66
% 0.19/0.66 fork 3: search finished without proof.
% 0.19/0.67
% 0.19/0.67
% 0.19/0.67 fork 2: search terminated without proof.
% 0.19/0.68
% 0.19/0.68
% 0.19/0.68 fork 0: search terminated without proof.
% 0.19/0.68
% 0.19/0.68 **** run 20 fork 3 starts with strategy
% 0.19/0.68 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 0.19/0.68
% 0.19/0.68 **** run 19 fork 2 starts with strategy
% 0.19/0.68 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"reverse_clauselist":1}
% 0.19/0.69
% 0.19/0.69
% 0.19/0.69 fork 5: search terminated without proof.
% 0.19/0.69
% 0.19/0.69
% 0.19/0.69 fork 4: search terminated without proof.
% 0.19/0.69
% 0.19/0.69
% 0.19/0.69 fork 6: search terminated without proof.
% 0.19/0.69
% 0.19/0.69 **** run 17 fork 0 starts with strategy
% 0.19/0.69 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 0.19/0.72
% 0.19/0.72 **** run 23 fork 6 starts with strategy
% 0.19/0.72 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"sine":1}
% 0.19/0.72
% 0.19/0.72 **** run 22 fork 5 starts with strategy
% 0.19/0.72 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 2.34/0.73
% 2.34/0.73 **** run 21 fork 4 starts with strategy
% 2.34/0.73 {"max_dseconds":1,"sine":3,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 2.34/0.75
% 2.34/0.75
% 2.34/0.75 fork 7: search terminated without proof.
% 2.34/0.75
% 2.34/0.75 fork 4: search finished without proof.
% 2.85/0.77
% 2.85/0.77 **** run 29 fork 4 starts with strategy
% 2.85/0.77 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 2.85/0.77
% 2.85/0.77 **** run 24 fork 7 starts with strategy
% 2.85/0.77 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 2.85/0.78
% 2.85/0.78
% 2.85/0.78 fork 1: search terminated without proof.
% 2.85/0.80
% 2.85/0.80 **** run 26 fork 1 starts with strategy
% 2.85/0.80 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"sine":2}
% 3.39/0.82
% 3.39/0.82
% 3.39/0.82 fork 2: search terminated without proof.
% 3.39/0.82
% 3.39/0.82
% 3.39/0.82 fork 3: search terminated without proof.
% 3.39/0.83
% 3.39/0.83 fork 1: search finished without proof.
% 3.39/0.83
% 3.39/0.83
% 3.39/0.83 fork 0: search terminated without proof.
% 3.39/0.84
% 3.39/0.84 **** run 28 fork 3 starts with strategy
% 3.39/0.84 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"depth_penalty":100}
% 3.39/0.84
% 3.39/0.84
% 3.39/0.84 fork 5: search terminated without proof.
% 3.39/0.84
% 3.39/0.84 **** run 27 fork 2 starts with strategy
% 3.39/0.84 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":1}
% 3.39/0.84
% 3.39/0.84
% 3.39/0.84 fork 6: search terminated without proof.
% 3.39/0.84
% 3.39/0.84 **** run 34 fork 1 starts with strategy
% 3.39/0.84 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":3}
% 3.39/0.85
% 3.39/0.85 **** run 25 fork 0 starts with strategy
% 3.39/0.85 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 3.70/0.86
% 3.70/0.86 **** run 31 fork 6 starts with strategy
% 3.70/0.86 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_deep_para"],"query_preference":0,"rewrite":0}
% 3.70/0.87
% 3.70/0.87 **** run 30 fork 5 starts with strategy
% 3.70/0.87 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"rewrite":0}
% 3.70/0.89
% 3.70/0.89
% 3.70/0.89 fork 4: search terminated without proof.
% 3.70/0.90
% 3.70/0.90
% 3.70/0.90 fork 7: search terminated without proof.
% 3.70/0.91
% 3.70/0.91 **** run 37 fork 4 starts with strategy
% 3.70/0.91 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":1}
% 3.70/0.93
% 3.70/0.93 **** run 32 fork 7 starts with strategy
% 3.70/0.93 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 4.38/0.97
% 4.38/0.97 fork 4: search finished without proof.
% 4.38/0.97
% 4.38/0.97
% 4.38/0.97 fork 3: search terminated without proof.
% 4.38/0.97
% 4.38/0.97
% 4.38/0.97 fork 2: search terminated without proof.
% 4.38/0.98
% 4.38/0.98
% 4.38/0.98 fork 1: search terminated without proof.
% 4.66/0.98
% 4.66/0.98
% 4.66/0.98 fork 0: search terminated without proof.
% 4.66/0.98
% 4.66/0.98 **** run 45 fork 4 starts with strategy
% 4.66/0.98 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":1}
% 4.66/0.99
% 4.66/0.99 **** run 36 fork 3 starts with strategy
% 4.66/0.99 {"max_dseconds":1,"strategy":["negative_pref","posunitpara"],"query_preference":1,"max_depth":2,"depth_penalty":50,"length_penalty":100}
% 4.66/0.99
% 4.66/0.99 **** run 35 fork 2 starts with strategy
% 4.66/0.99 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":30,"depth_penalty":100}
% 4.66/1.00
% 4.66/1.00 **** run 42 fork 1 starts with strategy
% 4.66/1.00 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"max_depth":6,"var_weight":1}
% 4.66/1.00
% 4.66/1.00 fork 6: search finished without proof.
% 4.66/1.00
% 4.66/1.00
% 4.66/1.00 fork 5: search terminated without proof.
% 4.66/1.00
% 4.66/1.00 **** run 33 fork 0 starts with strategy
% 4.66/1.00 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"length_penalty":100}
% 4.66/1.02
% 4.66/1.02 **** run 39 fork 6 starts with strategy
% 4.66/1.02 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"query_preference":1,"strategy":["query_focus","max_weight"],"max_dseconds":1,"max_size":15}
% 4.66/1.03
% 4.66/1.03 **** run 38 fork 5 starts with strategy
% 4.66/1.03 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":2}
% 5.24/1.06
% 5.24/1.06 fork 5: search finished without proof.
% 5.24/1.07
% 5.24/1.07
% 5.24/1.07 fork 7: search terminated without proof.
% 5.24/1.08
% 5.24/1.08 **** run 46 fork 5 starts with strategy
% 5.24/1.08 {"var_weight":70,"repeat_var_weight":70,"rewrite":0,"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["hardness_pref","max_weight"],"max_dseconds":1}
% 5.24/1.08
% 5.24/1.08 **** run 40 fork 7 starts with strategy
% 5.24/1.08 {"weight_select_ratio":100,"query_preference":1,"strategy":["negative_pref"],"max_dseconds":1}
% 5.24/1.09
% 5.24/1.09 fork 3: search finished without proof.
% 5.24/1.11
% 5.24/1.11 **** run 44 fork 3 starts with strategy
% 5.24/1.11 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"sine":3,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 5.75/1.12
% 5.75/1.12
% 5.75/1.12 fork 4: search terminated without proof.
% 5.75/1.13
% 5.75/1.13
% 5.75/1.13 fork 1: search terminated without proof.
% 5.75/1.13
% 5.75/1.13
% 5.75/1.13 fork 2: search terminated without proof.
% 5.75/1.13
% 5.75/1.13
% 5.75/1.13 fork 0: search terminated without proof.
% 5.75/1.14
% 5.75/1.14 **** run 53 fork 4 starts with strategy
% 5.75/1.14 {"max_dseconds":1,"strategy":["negative_pref","max_ground_weight"],"query_preference":1}
% 5.75/1.14
% 5.75/1.14 fork 3: search finished without proof.
% 5.75/1.15
% 5.75/1.15 **** run 50 fork 1 starts with strategy
% 5.75/1.15 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"max_depth":2}
% 5.75/1.15
% 5.75/1.15 **** run 43 fork 2 starts with strategy
% 5.75/1.15 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 5.75/1.15
% 5.75/1.15
% 5.75/1.15 fork 6: search terminated without proof.
% 5.75/1.15
% 5.75/1.15 **** run 41 fork 0 starts with strategy
% 5.75/1.15 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"max_depth":2}
% 6.11/1.16
% 6.11/1.16 **** run 52 fork 3 starts with strategy
% 6.11/1.16 {"max_dseconds":1,"sine":4,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 6.11/1.17
% 6.11/1.17 **** run 47 fork 6 starts with strategy
% 6.11/1.17 {"max_depth":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 6.11/1.21
% 6.11/1.21
% 6.11/1.21 fork 5: search terminated without proof.
% 6.11/1.21
% 6.11/1.21
% 6.11/1.21 fork 7: search terminated without proof.
% 6.11/1.22
% 6.11/1.22 **** run 54 fork 5 starts with strategy
% 6.11/1.22 {"weight_select_ratio":20,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 6.11/1.23
% 6.11/1.23 **** run 48 fork 7 starts with strategy
% 6.11/1.23 {"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 6.75/1.26
% 6.75/1.26 fork 1: search finished without proof.
% 6.75/1.27
% 6.75/1.27
% 6.75/1.27 fork 4: search terminated without proof.
% 6.75/1.28
% 6.75/1.28
% 6.75/1.28 fork 2: search terminated without proof.
% 6.75/1.28
% 6.75/1.28 **** run 58 fork 1 starts with strategy
% 6.75/1.28 {"depth_penalty":50,"sine":3,"query_preference":1,"strategy":["hardness_pref","hornpref","max_weight"],"max_dseconds":1}
% 6.75/1.28
% 6.75/1.28 **** run 61 fork 4 starts with strategy
% 6.75/1.28 {"sine":1,"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":1,"strategy":["unit"],"max_dseconds":1}
% 6.75/1.28
% 6.75/1.28
% 6.75/1.28 fork 0: search terminated without proof.
% 6.75/1.29
% 6.75/1.29 fork 3: search finished without proof.
% 6.75/1.30
% 6.75/1.30
% 6.75/1.30 fork 6: search terminated without proof.
% 6.75/1.30
% 6.75/1.30 **** run 51 fork 2 starts with strategy
% 6.75/1.30 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 6.75/1.31
% 6.75/1.31 **** run 60 fork 3 starts with strategy
% 6.75/1.31 {"sine":1,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 6.75/1.31
% 6.75/1.31 **** run 49 fork 0 starts with strategy
% 6.75/1.31 {"max_dseconds":1,"strategy":["hardness_pref","posunitpara"],"query_preference":0,"depth_penalty":50,"length_penalty":100}
% 6.75/1.31
% 6.75/1.31 fork 1: search finished without proof.
% 6.75/1.32
% 6.75/1.32 **** run 55 fork 6 starts with strategy
% 6.75/1.32 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_dseconds":1}
% 6.75/1.33
% 6.75/1.33 **** run 66 fork 1 starts with strategy
% 6.75/1.33 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1}
% 7.44/1.37
% 7.44/1.37
% 7.44/1.37 fork 5: search terminated without proof.
% 7.44/1.39
% 7.44/1.39
% 7.44/1.39 fork 7: search terminated without proof.
% 7.44/1.39
% 7.44/1.39 **** run 62 fork 5 starts with strategy
% 7.44/1.39 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"weight_select_ratio":30,"depth_penalty":100,"length_penalty":100}
% 7.44/1.41
% 7.44/1.41 **** run 56 fork 7 starts with strategy
% 7.44/1.41 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_depth":2,"max_dseconds":1}
% 8.13/1.42
% 8.13/1.42
% 8.13/1.42 fork 4: search terminated without proof.
% 8.13/1.44
% 8.13/1.44
% 8.13/1.44 fork 2: search terminated without proof.
% 8.13/1.44
% 8.13/1.44
% 8.13/1.44 fork 0: search terminated without proof.
% 8.29/1.44
% 8.29/1.44 **** run 69 fork 4 starts with strategy
% 8.29/1.44 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":1}
% 8.29/1.45
% 8.29/1.45
% 8.29/1.45 fork 3: search terminated without proof.
% 8.29/1.45
% 8.29/1.45
% 8.29/1.45 fork 6: search terminated without proof.
% 8.29/1.46
% 8.29/1.46 **** run 57 fork 0 starts with strategy
% 8.29/1.46 {"depth_penalty":50,"query_preference":1,"strategy":["hardness_pref","hornpref","max_weight"],"max_dseconds":1}
% 8.29/1.46
% 8.29/1.46 **** run 59 fork 2 starts with strategy
% 8.29/1.46 {"rewrite":0,"depth_penalty":50,"query_preference":1,"strategy":["query_focus","hornpref"],"max_dseconds":1}
% 8.29/1.47
% 8.29/1.47 **** run 68 fork 3 starts with strategy
% 8.29/1.47 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 8.29/1.48
% 8.29/1.48 **** run 63 fork 6 starts with strategy
% 8.29/1.48 {"length_penalty":100,"query_preference":1,"strategy":["positive_pref","posunitpara"],"max_dseconds":1}
% 8.29/1.48
% 8.29/1.48
% 8.29/1.48 fork 1: search terminated without proof.
% 8.29/1.50
% 8.29/1.50 **** run 74 fork 1 starts with strategy
% 8.29/1.50 {"max_dseconds":1,"strategy":["query_focus","posunitpara"],"query_preference":1,"depth_penalty":50,"length_penalty":100,"sine":1}
% 8.87/1.52
% 8.87/1.52
% 8.87/1.52 fork 5: search terminated without proof.
% 8.87/1.53
% 8.87/1.53
% 8.87/1.53 fork 7: search terminated without proof.
% 8.87/1.54
% 8.87/1.54 **** run 70 fork 5 starts with strategy
% 8.87/1.54 {"max_dseconds":1,"strategy":["unit","pure_unit"],"max_size":30,"max_depth":10,"max_weight":300,"weight_select_ratio":1,"rewrite":0}
% 8.87/1.55
% 8.87/1.55 **** run 64 fork 7 starts with strategy
% 8.87/1.55 {"sine":2,"query_preference":0,"strategy":["unit"],"max_dseconds":1}
% 9.29/1.58
% 9.29/1.58
% 9.29/1.58 fork 4: search terminated without proof.
% 9.29/1.58
% 9.29/1.58 fork 7: search finished without proof.
% 9.29/1.59
% 9.29/1.59
% 9.29/1.59 fork 0: search terminated without proof.
% 9.29/1.60
% 9.29/1.60 **** run 77 fork 4 starts with strategy
% 9.29/1.60 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 9.29/1.60
% 9.29/1.60 **** run 72 fork 7 starts with strategy
% 9.29/1.60 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 9.29/1.60
% 9.29/1.60
% 9.29/1.60 fork 2: search terminated without proof.
% 9.29/1.60
% 9.29/1.60
% 9.29/1.60 fork 3: search terminated without proof.
% 9.29/1.61
% 9.29/1.61 **** run 65 fork 0 starts with strategy
% 9.29/1.61 {"weight_select_ratio":100,"rewrite":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 9.29/1.61
% 9.29/1.61
% 9.29/1.61 fork 6: search terminated without proof.
% 9.29/1.61
% 9.29/1.61 fork 5: search finished without proof.
% 9.29/1.62
% 9.29/1.62 **** run 67 fork 2 starts with strategy
% 9.29/1.62 {"max_dseconds":1,"strategy":["hardness_pref","posunitpara"],"query_preference":1}
% 9.29/1.62
% 9.29/1.62 **** run 76 fork 3 starts with strategy
% 9.29/1.62 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"rewrite":0}
% 9.29/1.63
% 9.29/1.63 **** run 71 fork 6 starts with strategy
% 9.29/1.63 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 9.29/1.63
% 9.29/1.63
% 9.29/1.63 fork 1: search terminated without proof.
% 9.29/1.63
% 9.29/1.63 **** run 78 fork 5 starts with strategy
% 9.29/1.63 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 9.95/1.65
% 9.95/1.65 **** run 82 fork 1 starts with strategy
% 9.95/1.65 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 10.53/1.73
% 10.53/1.73
% 10.53/1.73 fork 7: search terminated without proof.
% 10.53/1.73
% 10.53/1.73
% 10.53/1.73 fork 4: search terminated without proof.
% 10.53/1.74
% 10.53/1.74
% 10.53/1.74 fork 0: search terminated without proof.
% 10.68/1.75
% 10.68/1.75 **** run 80 fork 7 starts with strategy
% 10.68/1.75 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 10.68/1.75
% 10.68/1.75
% 10.68/1.75 fork 2: search terminated without proof.
% 10.68/1.75
% 10.68/1.75 **** run 85 fork 4 starts with strategy
% 10.68/1.75 {"max_dseconds":1,"strategy":["unit","pure_unit"],"query_preference":0}
% 10.68/1.76
% 10.68/1.76 **** run 73 fork 0 starts with strategy
% 10.68/1.76 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":1}
% 10.68/1.76
% 10.68/1.76
% 10.68/1.76 fork 6: search terminated without proof.
% 10.68/1.76
% 10.68/1.76
% 10.68/1.76 fork 3: search terminated without proof.
% 10.68/1.76
% 10.68/1.76
% 10.68/1.76 fork 5: search terminated without proof.
% 10.68/1.77
% 10.68/1.77 **** run 75 fork 2 starts with strategy
% 10.68/1.77 {"max_dseconds":1,"strategy":["query_focus","max_ground_weight"],"query_preference":1}
% 10.68/1.78
% 10.68/1.78 **** run 84 fork 3 starts with strategy
% 10.68/1.78 {"max_dseconds":1,"strategy":["negative_pref","prohibit_nested_para"],"query_preference":0}
% 10.68/1.78
% 10.68/1.78 **** run 79 fork 6 starts with strategy
% 10.68/1.78 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 10.68/1.78
% 10.68/1.78
% 10.68/1.78 fork 1: search terminated without proof.
% 10.68/1.79
% 10.68/1.79 **** run 86 fork 5 starts with strategy
% 10.68/1.79 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 10.68/1.81
% 10.68/1.81 **** run 90 fork 1 starts with strategy
% 10.68/1.81 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"rewrite":0}
% 11.24/1.86
% 11.24/1.86 fork 7: search finished without proof.
% 11.70/1.88
% 11.70/1.88 **** run 88 fork 7 starts with strategy
% 11.70/1.88 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0,"sine":2}
% 11.70/1.89
% 11.70/1.89
% 11.70/1.89 fork 4: search terminated without proof.
% 11.70/1.89
% 11.70/1.89
% 11.70/1.89 fork 0: search terminated without proof.
% 11.70/1.90
% 11.70/1.90 **** run 81 fork 0 starts with strategy
% 11.70/1.90 {"max_dseconds":1,"strategy":["unit","prohibit_nested_para"],"query_preference":1,"reverse_clauselist":1}
% 11.70/1.91
% 11.70/1.91 **** run 93 fork 4 starts with strategy
% 11.70/1.91 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"sine":1}
% 11.70/1.91
% 11.70/1.91
% 11.70/1.91 fork 2: search terminated without proof.
% 11.70/1.91
% 11.70/1.91 fork 7: search finished without proof.
% 11.70/1.91
% 11.70/1.91
% 11.70/1.91 fork 3: search terminated without proof.
% 11.70/1.91
% 11.70/1.91
% 11.70/1.91 fork 6: search terminated without proof.
% 11.70/1.92
% 11.70/1.92
% 11.70/1.92 fork 5: search terminated without proof.
% 11.70/1.93
% 11.70/1.93 **** run 96 fork 7 starts with strategy
% 11.70/1.93 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":2}
% 11.70/1.93
% 11.70/1.93 **** run 83 fork 2 starts with strategy
% 11.70/1.93 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1,"length_penalty":100}
% 11.70/1.93
% 11.70/1.93 **** run 87 fork 6 starts with strategy
% 11.70/1.93 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"depth_penalty":100,"sine":1}
% 11.70/1.93
% 11.70/1.93 **** run 92 fork 3 starts with strategy
% 11.70/1.93 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 11.70/1.94
% 11.70/1.94
% 11.70/1.94 fork 1: search terminated without proof.
% 11.70/1.95
% 11.70/1.95 **** run 94 fork 5 starts with strategy
% 11.70/1.95 {"max_dseconds":1,"strategy":["unit","pure_unit"],"weight_select_ratio":1,"query_preference":0}
% 11.70/1.97
% 11.70/1.97 **** run 98 fork 1 starts with strategy
% 11.70/1.97 {"sine":1,"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":1,"strategy":["query_focus","max_weight"],"max_dseconds":1}
% 11.70/2.03
% 11.70/2.03
% 11.70/2.03 fork 0: search terminated without proof.
% 12.73/2.05
% 12.73/2.05 **** run 89 fork 0 starts with strategy
% 12.73/2.05 {"sine":1,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":1}
% 12.73/2.05
% 12.73/2.05 fork 7: search finished without proof.
% 12.73/2.06
% 12.73/2.06
% 12.73/2.06 fork 6: search terminated without proof.
% 12.73/2.07
% 12.73/2.07
% 12.73/2.07 fork 3: search terminated without proof.
% 12.73/2.07
% 12.73/2.07
% 12.73/2.07 fork 2: search terminated without proof.
% 13.22/2.07
% 13.22/2.07 **** run 104 fork 7 starts with strategy
% 13.22/2.07 {"var_weight":70,"repeat_var_weight":70,"length_penalty":100,"depth_penalty":100,"query_preference":1,"strategy":["positive_pref","unit"],"max_dseconds":1}
% 13.22/2.08
% 13.22/2.08
% 13.22/2.08 fork 5: search terminated without proof.
% 13.22/2.08
% 13.22/2.08 **** run 95 fork 6 starts with strategy
% 13.22/2.08 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"query_preference":0,"strategy":["query_focus","posunitpara"],"max_dseconds":1}
% 13.22/2.09
% 13.22/2.09
% 13.22/2.09 fork 4: search terminated without proof.
% 13.22/2.09
% 13.22/2.09 **** run 100 fork 3 starts with strategy
% 13.22/2.09 {"weight_select_ratio":100,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":1}
% 13.22/2.09
% 13.22/2.09 **** run 91 fork 2 starts with strategy
% 13.22/2.09 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 13.22/2.10
% 13.22/2.10 **** run 102 fork 5 starts with strategy
% 13.22/2.10 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 13.22/2.11
% 13.22/2.11 **** run 101 fork 4 starts with strategy
% 13.22/2.11 {"sine":1,"rewrite":0,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 13.60/2.12
% 13.60/2.12
% 13.60/2.12 fork 1: search terminated without proof.
% 13.81/2.15
% 13.81/2.15 **** run 106 fork 1 starts with strategy
% 13.81/2.15 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"equality":0}
% 13.81/2.18
% 13.81/2.18 fork 1: search finished without proof.
% 13.81/2.18
% 13.81/2.18
% 13.81/2.18 fork 0: search terminated without proof.
% 13.81/2.19
% 13.81/2.19 **** run 114 fork 1 starts with strategy
% 13.81/2.19 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"max_depth":4}
% 13.81/2.20
% 13.81/2.20 **** run 97 fork 0 starts with strategy
% 13.81/2.20 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100,"sine":2}
% 13.81/2.20
% 13.81/2.20
% 13.81/2.20 fork 7: search terminated without proof.
% 13.81/2.21
% 13.81/2.21
% 13.81/2.21 fork 6: search terminated without proof.
% 13.81/2.22
% 13.81/2.22
% 13.81/2.22 fork 2: search terminated without proof.
% 14.44/2.22
% 14.44/2.22
% 14.44/2.22 fork 3: search terminated without proof.
% 14.44/2.22
% 14.44/2.22 **** run 112 fork 7 starts with strategy
% 14.44/2.22 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"length_penalty":100,"query_preference":1,"strategy":["query_focus","prohibit_nested_para"],"max_dseconds":1}
% 14.44/2.23
% 14.44/2.23 fork 0: search finished without proof.
% 14.44/2.23
% 14.44/2.23 fork 5: search finished without proof.
% 14.44/2.24
% 14.44/2.24 **** run 103 fork 6 starts with strategy
% 14.44/2.24 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":1,"strategy":["positive_pref","unit"],"max_dseconds":1}
% 14.44/2.24
% 14.44/2.24
% 14.44/2.24 fork 4: search terminated without proof.
% 14.44/2.25
% 14.44/2.25 **** run 99 fork 2 starts with strategy
% 14.44/2.25 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"query_preference":1,"strategy":["query_focus","max_weight"],"max_dseconds":1}
% 14.44/2.25
% 14.44/2.25 **** run 108 fork 3 starts with strategy
% 14.44/2.25 {"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["positive_pref"],"max_dseconds":1}
% 14.44/2.25
% 14.44/2.25 **** run 110 fork 5 starts with strategy
% 14.44/2.25 {"max_dseconds":1,"strategy":["query_focus","posunitpara"],"query_preference":1,"depth_penalty":50,"length_penalty":100}
% 14.44/2.25
% 14.44/2.25 **** run 105 fork 0 starts with strategy
% 14.44/2.25 {"max_dseconds":1,"strategy":["hardness_pref","posunitpara"],"query_preference":1,"sine":1}
% 14.44/2.26
% 14.44/2.26 **** run 109 fork 4 starts with strategy
% 14.44/2.26 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 14.87/2.32
% 14.87/2.32
% 14.87/2.32 fork 1: search terminated without proof.
% 14.87/2.34
% 14.87/2.34 **** run 122 fork 1 starts with strategy
% 14.87/2.34 {"max_dseconds":10,"strategy":["unit","prohibit_unordered_para"],"query_preference":1}
% 15.43/2.36
% 15.43/2.36
% 15.43/2.36 fork 7: search terminated without proof.
% 15.43/2.37
% 15.43/2.37
% 15.43/2.37 fork 6: search terminated without proof.
% 15.59/2.38
% 15.59/2.38 **** run 120 fork 7 starts with strategy
% 15.59/2.38 {"max_dseconds":10,"strategy":["negative_pref","prohibit_unordered_para"],"query_preference":0}
% 15.59/2.38
% 15.59/2.38
% 15.59/2.38 fork 3: search terminated without proof.
% 15.59/2.38
% 15.59/2.38
% 15.59/2.38 fork 2: search terminated without proof.
% 15.59/2.39
% 15.59/2.39 **** run 111 fork 6 starts with strategy
% 15.59/2.39 {"var_weight":70,"repeat_var_weight":70,"length_penalty":100,"depth_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 15.59/2.39
% 15.59/2.39
% 15.59/2.39 fork 5: search terminated without proof.
% 15.59/2.39
% 15.59/2.39
% 15.59/2.39 fork 0: search terminated without proof.
% 15.59/2.39
% 15.59/2.39
% 15.59/2.39 fork 4: search terminated without proof.
% 15.59/2.40
% 15.59/2.40 **** run 116 fork 3 starts with strategy
% 15.59/2.40 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 15.59/2.40 **** run 107 fork 2 starts with strategy
% 15.59/2.40 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1}
% 15.59/2.40
% 15.59/2.41
% 15.59/2.41 **** run 117 fork 4 starts with strategy
% 15.59/2.41 {"max_dseconds":10,"sine":3,"strategy":["hardness_pref"],"query_preference":0}
% 15.59/2.41
% 15.59/2.41 **** run 113 fork 0 starts with strategy
% 15.59/2.41 {"query_preference":1,"strategy":["unit","max_weight"],"max_dseconds":1}
% 15.59/2.41
% 15.59/2.41 **** run 118 fork 5 starts with strategy
% 15.59/2.41 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 15.97/2.44
% 15.97/2.44 fork 4: search finished without proof.
% 16.19/2.45
% 16.19/2.45 **** run 125 fork 4 starts with strategy
% 16.19/2.45 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"],"query_preference":1}
% 16.19/2.52
% 16.19/2.52
% 16.19/2.52 fork 6: search terminated without proof.
% 16.86/2.53
% 16.86/2.53
% 16.86/2.53 fork 2: search terminated without proof.
% 16.86/2.54
% 16.86/2.54 **** run 119 fork 6 starts with strategy
% 16.86/2.54 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 16.86/2.54
% 16.86/2.54
% 16.86/2.54 fork 0: search terminated without proof.
% 16.86/2.55
% 16.86/2.55 **** run 115 fork 2 starts with strategy
% 16.86/2.55 {"sine":2,"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"depth_penalty":50,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 16.86/2.56
% 16.86/2.56 **** run 121 fork 0 starts with strategy
% 16.86/2.56 {"max_dseconds":10,"strategy":["unit","prohibit_unordered_para"],"query_preference":0}
% 16.86/2.58
% 16.86/2.58 fork 2: search finished without proof.
% 16.86/2.59
% 16.86/2.59 **** run 123 fork 2 starts with strategy
% 16.86/2.59 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 23.15/3.43
% 23.15/3.43
% 23.15/3.43 fork 7: search terminated without proof.
% 23.42/3.45
% 23.42/3.45
% 23.42/3.45 fork 5: search terminated without proof.
% 23.42/3.45
% 23.42/3.45 **** run 128 fork 7 starts with strategy
% 23.42/3.45 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":1,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 23.42/3.46
% 23.42/3.46 **** run 126 fork 5 starts with strategy
% 23.42/3.46 {"max_dseconds":10,"strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"],"query_preference":0}
% 23.42/3.48
% 23.42/3.48
% 23.42/3.48 fork 4: search terminated without proof.
% 23.42/3.50
% 23.42/3.50 **** run 133 fork 4 starts with strategy
% 23.42/3.50 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":3}
% 23.42/3.53
% 23.42/3.53
% 23.42/3.53 fork 1: search terminated without proof.
% 24.10/3.55
% 24.10/3.55
% 24.10/3.55 result: proof found
% 24.10/3.55 for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.10/3.55 by run 116 fork 3 strategy {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 24.10/3.55 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.10/3.55
% 24.10/3.55 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.10/3.55 cnf('1', plain, (queue_145 = store(queue_143,tail,index_144)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp162'])).
% 24.10/3.55 cnf('2', plain, (select(store(X,Y,Z),U) = select(X,U) | Y = U),
% 24.10/3.55 inference(cnf_transformation,[],['a2'])).
% 24.10/3.55 cnf('3', plain, (select(queue_145,X) = select(queue_143,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['1','2'])).
% 24.10/3.55 cnf('4', plain, (q27 = queue_139),
% 24.10/3.55 inference(cnf_transformation,[],['hyp235'])).
% 24.10/3.55 cnf('5', plain, (queue_143 = store(q27,seq,earray_142)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp161'])).
% 24.10/3.55 cnf('6', plain, (queue_143 = store(queue_139,seq,earray_142)),
% 24.10/3.55 inference(paramodulation,[],['4','5'])).
% 24.10/3.55 cnf('7', plain, (select(queue_143,X) = select(queue_139,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['6','2'])).
% 24.10/3.55 cnf('8', plain, (queue_139 = store(queue_136,head,index_138)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp160'])).
% 24.10/3.55 cnf('9', plain, (select(store(X,Y,Z),Y) = Z),
% 24.10/3.55 inference(cnf_transformation,[],['a1'])).
% 24.10/3.55 cnf('10', plain, (select(queue_139,head) = index_138),
% 24.10/3.55 inference(paramodulation,[],['8','9'])).
% 24.10/3.55 cnf('11', plain, (select(queue_143,head) = index_138 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['7','10'])).
% 24.10/3.55 cnf('12', plain, (select(queue_145,head) = index_138 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['3','11'])).
% 24.10/3.55 cnf('13', plain, (q28 = queue_145),
% 24.10/3.55 inference(cnf_transformation,[],['hyp236'])).
% 24.10/3.55 cnf('14', plain, (queue_149 = store(q28,seq,earray_148)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp163'])).
% 24.10/3.55 cnf('15', plain, (queue_149 = store(queue_145,seq,earray_148)),
% 24.10/3.55 inference(paramodulation,[],['13','14'])).
% 24.10/3.55 cnf('16', plain, (select(queue_149,X) = select(queue_145,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['15','2'])).
% 24.10/3.55 cnf('17', plain, (select(queue_149,head) = index_138 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['12','16'])).
% 24.10/3.55 cnf('18', plain, (queue_136 = store(queue_134,tail,index_135)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp159'])).
% 24.10/3.55 cnf('19', plain, (select(queue_136,X) = select(queue_134,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['18','2'])).
% 24.10/3.55 cnf('20', plain, (index_137 = select(queue_136,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp77'])).
% 24.10/3.55 cnf('21', plain, (index_137 = select(queue_134,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['19','20'])).
% 24.10/3.55 cnf('22', plain, (q26 = queue_130),
% 24.10/3.55 inference(cnf_transformation,[],['hyp234'])).
% 24.10/3.55 cnf('23', plain, (queue_134 = store(q26,seq,earray_133)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp158'])).
% 24.10/3.55 cnf('24', plain, (queue_134 = store(queue_130,seq,earray_133)),
% 24.10/3.55 inference(paramodulation,[],['22','23'])).
% 24.10/3.55 cnf('25', plain, (select(queue_134,X) = select(queue_130,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['24','2'])).
% 24.10/3.55 cnf('26', plain, (index_137 = select(queue_130,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['21','25'])).
% 24.10/3.55 cnf('27', plain, (queue_130 = store(queue_128,tail,index_129)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp157'])).
% 24.10/3.55 cnf('28', plain, (select(queue_130,X) = select(queue_128,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['27','2'])).
% 24.10/3.55 cnf('29', plain, (index_137 = select(queue_128,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['26','28'])).
% 24.10/3.55 cnf('30', plain, (queue_124 = store(queue_122,tail,index_123)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp154'])).
% 24.10/3.55 cnf('31', plain, (select(queue_124,X) = select(queue_122,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['30','2'])).
% 24.10/3.55 cnf('32', plain, (q24 = queue_118),
% 24.10/3.55 inference(cnf_transformation,[],['hyp232'])).
% 24.10/3.55 cnf('33', plain, (queue_122 = store(q24,seq,earray_121)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp153'])).
% 24.10/3.55 cnf('34', plain, (queue_122 = store(queue_118,seq,earray_121)),
% 24.10/3.55 inference(paramodulation,[],['32','33'])).
% 24.10/3.55 cnf('35', plain, (select(queue_122,X) = select(queue_118,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['34','2'])).
% 24.10/3.55 cnf('36', plain, (queue_118 = store(queue_115,head,index_117)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp152'])).
% 24.10/3.55 cnf('37', plain, (select(queue_118,head) = index_117),
% 24.10/3.55 inference(paramodulation,[],['36','9'])).
% 24.10/3.55 cnf('38', plain, (select(queue_122,head) = index_117 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['35','37'])).
% 24.10/3.55 cnf('39', plain, (select(queue_124,head) = index_117 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['31','38'])).
% 24.10/3.55 cnf('40', plain, (q25 = queue_124),
% 24.10/3.55 inference(cnf_transformation,[],['hyp233'])).
% 24.10/3.55 cnf('41', plain, (queue_128 = store(q25,seq,earray_127)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp155'])).
% 24.10/3.55 cnf('42', plain, (queue_128 = store(queue_124,seq,earray_127)),
% 24.10/3.55 inference(paramodulation,[],['40','41'])).
% 24.10/3.55 cnf('43', plain, (select(queue_128,X) = select(queue_124,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['42','2'])).
% 24.10/3.55 cnf('44', plain, (select(queue_128,head) = index_117 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['39','43'])).
% 24.10/3.55 cnf('45', plain, (seq = head | tail = head | index_137 = index_117),
% 24.10/3.55 inference(paramodulation,[],['29','44'])).
% 24.10/3.55 cnf('46', plain, (queue_115 = store(queue_113,tail,index_114)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp151'])).
% 24.10/3.55 cnf('47', plain, (select(queue_115,X) = select(queue_113,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['46','2'])).
% 24.10/3.55 cnf('48', plain, (index_116 = select(queue_115,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp68'])).
% 24.10/3.55 cnf('49', plain, (index_116 = select(queue_113,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['47','48'])).
% 24.10/3.55 cnf('50', plain, (q23 = queue_109),
% 24.10/3.55 inference(cnf_transformation,[],['hyp231'])).
% 24.10/3.55 cnf('51', plain, (queue_113 = store(q23,seq,earray_112)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp150'])).
% 24.10/3.55 cnf('52', plain, (queue_113 = store(queue_109,seq,earray_112)),
% 24.10/3.55 inference(paramodulation,[],['50','51'])).
% 24.10/3.55 cnf('53', plain, (select(queue_113,X) = select(queue_109,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['52','2'])).
% 24.10/3.55 cnf('54', plain, (index_116 = select(queue_109,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['49','53'])).
% 24.10/3.55 cnf('55', plain, (queue_109 = store(queue_107,tail,index_108)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp148'])).
% 24.10/3.55 cnf('56', plain, (select(queue_109,X) = select(queue_107,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['55','2'])).
% 24.10/3.55 cnf('57', plain, (index_116 = select(queue_107,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['54','56'])).
% 24.10/3.55 cnf('58', plain, (queue_103 = store(queue_101,tail,index_102)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp146'])).
% 24.10/3.55 cnf('59', plain, (select(queue_103,X) = select(queue_101,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['58','2'])).
% 24.10/3.55 cnf('60', plain, (queue_97 = store(queue_94,head,index_96)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp214'])).
% 24.10/3.55 cnf('61', plain, (select(queue_97,head) = index_96),
% 24.10/3.55 inference(paramodulation,[],['60','9'])).
% 24.10/3.55 cnf('62', plain, (q21 = queue_97),
% 24.10/3.55 inference(cnf_transformation,[],['hyp229'])).
% 24.10/3.55 cnf('63', plain, (queue_101 = store(q21,seq,earray_100)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp145'])).
% 24.10/3.55 cnf('64', plain, (queue_101 = store(queue_97,seq,earray_100)),
% 24.10/3.55 inference(paramodulation,[],['62','63'])).
% 24.10/3.55 cnf('65', plain, (select(queue_101,X) = select(queue_97,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['64','2'])).
% 24.10/3.55 cnf('66', plain, (select(queue_101,head) = index_96 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['61','65'])).
% 24.10/3.55 cnf('67', plain, (select(queue_103,head) = index_96 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['59','66'])).
% 24.10/3.55 cnf('68', plain, (q22 = queue_103),
% 24.10/3.55 inference(cnf_transformation,[],['hyp230'])).
% 24.10/3.55 cnf('69', plain, (queue_107 = store(q22,seq,earray_106)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp147'])).
% 24.10/3.55 cnf('70', plain, (queue_107 = store(queue_103,seq,earray_106)),
% 24.10/3.55 inference(paramodulation,[],['68','69'])).
% 24.10/3.55 cnf('71', plain, (select(queue_107,X) = select(queue_103,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['70','2'])).
% 24.10/3.55 cnf('72', plain, (select(queue_107,head) = index_96 | seq = head | tail = head),
% 24.10/3.55 inf
% 24.10/3.55 **** run 130 fork 1 starts with strategy
% 24.10/3.55 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":1}
% 24.10/3.55 erence(paramodulation,[],['67','71'])).
% 24.10/3.55 cnf('73', plain, (seq = head | tail = head | index_116 = index_96),
% 24.10/3.55 inference(paramodulation,[],['57','72'])).
% 24.10/3.55 cnf('74', plain, (head != seq),
% 24.10/3.55 inference(cnf_transformation,[],['head_distinct_from_seq'])).
% 24.10/3.55 cnf('75', plain, (tail = head | index_116 = index_96),
% 24.10/3.55 inference(paramodulation,[],['73','74'])).
% 24.10/3.55 cnf('76', plain, (head != tail),
% 24.10/3.55 inference(cnf_transformation,[],['head_distinct_from_tail'])).
% 24.10/3.55 cnf('77', plain, (index_116 = index_96),
% 24.10/3.55 inference(paramodulation,[],['75','76'])).
% 24.10/3.55 cnf('78', plain, (index_117 = s(index_116)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp69'])).
% 24.10/3.55 cnf('79', plain, (index_117 = s(index_96)),
% 24.10/3.55 inference(paramodulation,[],['77','78'])).
% 24.10/3.55 cnf('80', plain, (queue_13 = store(queue_11,tail,index_12)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp156'])).
% 24.10/3.55 cnf('81', plain, (select(queue_13,X) = select(queue_11,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['80','2'])).
% 24.10/3.55 cnf('82', plain, (queue_211 = store(queue_208,head,index_210)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp186'])).
% 24.10/3.55 cnf('83', plain, (select(queue_211,head) = index_210),
% 24.10/3.55 inference(paramodulation,[],['82','9'])).
% 24.10/3.55 cnf('84', plain, (q9 = queue_211),
% 24.10/3.55 inference(cnf_transformation,[],['hyp245'])).
% 24.10/3.55 cnf('85', plain, (queue_11 = store(q9,seq,earray_10)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp149'])).
% 24.10/3.55 cnf('86', plain, (queue_11 = store(queue_211,seq,earray_10)),
% 24.10/3.55 inference(paramodulation,[],['84','85'])).
% 24.10/3.55 cnf('87', plain, (select(queue_11,X) = select(queue_211,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['86','2'])).
% 24.10/3.55 cnf('88', plain, (select(queue_11,head) = index_210 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['83','87'])).
% 24.10/3.55 cnf('89', plain, (select(queue_13,head) = index_210 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['81','88'])).
% 24.10/3.55 cnf('90', plain, (q10 = queue_13),
% 24.10/3.55 inference(cnf_transformation,[],['hyp217'])).
% 24.10/3.55 cnf('91', plain, (queue_17 = store(q10,seq,earray_16)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp171'])).
% 24.10/3.55 cnf('92', plain, (queue_17 = store(queue_13,seq,earray_16)),
% 24.10/3.55 inference(paramodulation,[],['90','91'])).
% 24.10/3.55 cnf('93', plain, (select(queue_17,X) = select(queue_13,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['92','2'])).
% 24.10/3.55 cnf('94', plain, (select(queue_17,head) = index_210 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['89','93'])).
% 24.10/3.55 cnf('95', plain, (queue_25 = store(queue_23,tail,index_24)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp188'])).
% 24.10/3.55 cnf('96', plain, (select(queue_25,X) = select(queue_23,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['95','2'])).
% 24.10/3.55 cnf('97', plain, (index_26 = select(queue_25,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp112'])).
% 24.10/3.55 cnf('98', plain, (index_26 = select(queue_23,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['96','97'])).
% 24.10/3.55 cnf('99', plain, (q11 = queue_19),
% 24.10/3.55 inference(cnf_transformation,[],['hyp218'])).
% 24.10/3.55 cnf('100', plain, (queue_23 = store(q11,seq,earray_22)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp187'])).
% 24.10/3.55 cnf('101', plain, (queue_23 = store(queue_19,seq,earray_22)),
% 24.10/3.55 inference(paramodulation,[],['99','100'])).
% 24.10/3.55 cnf('102', plain, (select(queue_23,X) = select(queue_19,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['101','2'])).
% 24.10/3.55 cnf('103', plain, (index_26 = select(queue_19,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['98','102'])).
% 24.10/3.55 cnf('104', plain, (queue_19 = store(queue_17,tail,index_18)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp178'])).
% 24.10/3.55 cnf('105', plain, (select(queue_19,X) = select(queue_17,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['104','2'])).
% 24.10/3.55 cnf('106', plain, (index_26 = select(queue_17,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['103','105'])).
% 24.10/3.55 cnf('107', plain, (seq = head | tail = head | index_26 = index_210),
% 24.10/3.55 inference(paramodulation,[],['94','106'])).
% 24.10/3.55 cnf('108', plain, (tail = head | index_26 = index_210),
% 24.10/3.55 inference(paramodulation,[],['107','74'])).
% 24.10/3.55 cnf('109', plain, (index_26 = index_210),
% 24.10/3.55 inference(paramodulation,[],['108','76'])).
% 24.10/3.55 cnf('110', plain, (queue_175 = store(queue_173,tail,index_174)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp173'])).
% 24.10/3.55 cnf('111', plain, (select(queue_175,X) = select(queue_173,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['110','2'])).
% 24.10/3.55 cnf('112', plain, (q3 = queue_160),
% 24.10/3.55 inference(cnf_transformation,[],['hyp238'])).
% 24.10/3.55 cnf('113', plain, (queue_173 = store(q3,seq,earray_172)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp172'])).
% 24.10/3.55 cnf('114', plain, (queue_173 = store(queue_160,seq,earray_172)),
% 24.10/3.55 inference(paramodulation,[],['112','113'])).
% 24.10/3.55 cnf('115', plain, (select(queue_173,X) = select(queue_160,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['114','2'])).
% 24.10/3.55 cnf('116', plain, (queue_160 = store(queue_157,head,index_159)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp167'])).
% 24.10/3.55 cnf('117', plain, (select(queue_160,head) = index_159),
% 24.10/3.55 inference(paramodulation,[],['116','9'])).
% 24.10/3.55 cnf('118', plain, (select(queue_173,head) = index_159 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['115','117'])).
% 24.10/3.55 cnf('119', plain, (select(queue_175,head) = index_159 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['111','118'])).
% 24.10/3.55 cnf('120', plain, (q4 = queue_175),
% 24.10/3.55 inference(cnf_transformation,[],['hyp240'])).
% 24.10/3.55 cnf('121', plain, (queue_179 = store(q4,seq,earray_178)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp174'])).
% 24.10/3.55 cnf('122', plain, (queue_179 = store(queue_175,seq,earray_178)),
% 24.10/3.55 inference(paramodulation,[],['120','121'])).
% 24.10/3.55 cnf('123', plain, (select(queue_179,X) = select(queue_175,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['122','2'])).
% 24.10/3.55 cnf('124', plain, (select(queue_179,head) = index_159 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['119','123'])).
% 24.10/3.55 cnf('125', plain, (queue_157 = store(queue_155,tail,index_156)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp166'])).
% 24.10/3.55 cnf('126', plain, (select(queue_157,X) = select(queue_155,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['125','2'])).
% 24.10/3.55 cnf('127', plain, (index_158 = select(queue_157,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp86'])).
% 24.10/3.55 cnf('128', plain, (index_158 = select(queue_155,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['126','127'])).
% 24.10/3.55 cnf('129', plain, (q2 = queue_82),
% 24.10/3.55 inference(cnf_transformation,[],['hyp227'])).
% 24.10/3.55 cnf('130', plain, (queue_155 = store(q2,seq,earray_154)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp165'])).
% 24.10/3.55 cnf('131', plain, (queue_155 = store(queue_82,seq,earray_154)),
% 24.10/3.55 inference(paramodulation,[],['129','130'])).
% 24.10/3.55 cnf('132', plain, (select(queue_155,X) = select(queue_82,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['131','2'])).
% 24.10/3.55 cnf('133', plain, (index_158 = select(queue_82,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['128','132'])).
% 24.10/3.55 cnf('134', plain, (queue_82 = store(queue_80,tail,index_81)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp209'])).
% 24.10/3.55 cnf('135', plain, (select(queue_82,X) = select(queue_80,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['134','2'])).
% 24.10/3.55 cnf('136', plain, (index_158 = select(queue_80,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['133','135'])).
% 24.10/3.55 cnf('137', plain, (queue_7 = store(queue_5,tail,index_6)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp204'])).
% 24.10/3.55 cnf('138', plain, (select(queue_7,X) = select(queue_5,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['137','2'])).
% 24.10/3.55 cnf('139', plain, (q0 = queue_1),
% 24.10/3.55 inference(cnf_transformation,[],['hyp215'])).
% 24.10/3.55 cnf('140', plain, (queue_5 = store(q0,seq,earray_4)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp197'])).
% 24.10/3.55 cnf('141', plain, (queue_5 = store(queue_1,seq,earray_4)),
% 24.10/3.55 inference(paramodulation,[],['139','140'])).
% 24.10/3.55 cnf('142', plain, (select(queue_5,X) = select(queue_1,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['141','2'])).
% 24.10/3.55 cnf('143', plain, (queue_1 = store(q,head,index_0)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp144'])).
% 24.10/3.55 cnf('144', plain, (select(queue_1,head) = index_0),
% 24.10/3.55 inference(paramodulation,[],['143','9'])).
% 24.10/3.55 cnf('145', plain, (select(queue_5,head) = index_0 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['142','144'])).
% 24.10/3.55 cnf('146', plain, (select(queue_7,head) = index_0 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['138','145'])).
% 24.10/3.55 cnf('147', plain, (q1 = queue_7),
% 24.10/3.55 inference(cnf_transformation,[],['hyp216'])).
% 24.10/3.55 cnf('148', plain, (queue_80 = store(q1,seq,earray_79)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp208'])).
% 24.10/3.55 cnf('149', plain, (queue_80 = store(queue_7,seq,earray_79)),
% 24.10/3.55 inference(paramodulation,[],['147','148'])).
% 24.10/3.55 cnf('150', plain, (select(queue_80,X) = select(queue_7,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['149','2'])).
% 24.10/3.55 cnf('151', plain, (select(queue_80,head) = index_0 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['146','150'])).
% 24.10/3.55 cnf('152', plain, (seq = head | tail = head | index_158 = index_0),
% 24.10/3.55 inference(paramodulation,[],['136','151'])).
% 24.10/3.55 cnf('153', plain, (tail = head | index_158 = index_0),
% 24.10/3.55 inference(paramodulation,[],['152','74'])).
% 24.10/3.55 cnf('154', plain, (index_158 = index_0),
% 24.10/3.55 inference(paramodulation,[],['153','76'])).
% 24.10/3.55 cnf('155', plain, (select(queue_1,X) = select(q,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['143','2'])).
% 24.10/3.55 cnf('156', plain, (index_0 = select(q,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp62'])).
% 24.10/3.55 cnf('157', plain, (head != tail),
% 24.10/3.55 inference(cnf_transformation,[],['head_distinct_from_tail'])).
% 24.10/3.55 cnf('158', plain, (index_0 = select(queue_1,tail)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['155','156','157'])).
% 24.10/3.55 cnf('159', plain, (index_3 = select(q0,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp114'])).
% 24.10/3.55 cnf('160', plain, (index_3 = select(queue_1,tail)),
% 24.10/3.55 inference(paramodulation,[],['139','159'])).
% 24.10/3.55 cnf('161', plain, (index_0 = index_3),
% 24.10/3.55 inference(simplify,[],['158','160'])).
% 24.10/3.55 cnf('162', plain, (index_6 = s(index_3)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp126'])).
% 24.10/3.55 cnf('163', plain, (index_6 = s(index_0)),
% 24.10/3.55 inference(paramodulation,[],['161','162'])).
% 24.10/3.55 cnf('164', plain, (index_6 = s(index_158)),
% 24.10/3.55 inference(paramodulation,[],['154','163'])).
% 24.10/3.55 cnf('165', plain, (index_159 = s(index_158)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp87'])).
% 24.10/3.55 cnf('166', plain, (index_6 = index_159),
% 24.10/3.55 inference(simplify,[],['164','165'])).
% 24.10/3.55 cnf('167', plain, (select(queue_179,head) = index_6 | seq = head | tail = head),
% 24.10/3.55 inference(simplify,[],['124','166'])).
% 24.10/3.55 cnf('168', plain, (queue_187 = store(queue_185,tail,index_186)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp177'])).
% 24.10/3.55 cnf('169', plain, (select(queue_187,X) = select(queue_185,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['168','2'])).
% 24.10/3.55 cnf('170', plain, (index_188 = select(queue_187,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp99'])).
% 24.10/3.55 cnf('171', plain, (index_188 = select(queue_185,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['169','170'])).
% 24.10/3.55 cnf('172', plain, (q5 = queue_181),
% 24.10/3.55 inference(cnf_transformation,[],['hyp241'])).
% 24.10/3.55 cnf('173', plain, (queue_185 = store(q5,seq,earray_184)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp176'])).
% 24.10/3.55 cnf('174', plain, (queue_185 = store(queue_181,seq,earray_184)),
% 24.10/3.55 inference(paramodulation,[],['172','173'])).
% 24.10/3.55 cnf('175', plain, (select(queue_185,X) = select(queue_181,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['174','2'])).
% 24.10/3.55 cnf('176', plain, (index_188 = select(queue_181,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['171','175'])).
% 24.10/3.55 cnf('177', plain, (queue_181 = store(queue_179,tail,index_180)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp175'])).
% 24.10/3.55 cnf('178', plain, (select(queue_181,X) = select(queue_179,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['177','2'])).
% 24.10/3.55 cnf('179', plain, (index_188 = select(queue_179,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['176','178'])).
% 24.10/3.55 cnf('180', plain, (index_188 = index_6 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['167','179'])).
% 24.10/3.55 cnf('181', plain, (index_189 = s(index_188)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp100'])).
% 24.10/3.55 cnf('182', plain, (index_189 = s(index_6) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['180','181'])).
% 24.10/3.55 cnf('183', plain, (queue_196 = store(queue_194,tail,index_195)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp181'])).
% 24.10/3.55 cnf('184', plain, (select(queue_196,X) = select(queue_194,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['183','2'])).
% 24.10/3.55 cnf('185', plain, (q6 = queue_190),
% 24.10/3.55 inference(cnf_transformation,[],['hyp242'])).
% 24.10/3.55 cnf('186', plain, (queue_194 = store(q6,seq,earray_193)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp180'])).
% 24.10/3.55 cnf('187', plain, (queue_194 = store(queue_190,seq,earray_193)),
% 24.10/3.55 inference(paramodulation,[],['185','186'])).
% 24.10/3.55 cnf('188', plain, (select(queue_194,X) = select(queue_190,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['187','2'])).
% 24.10/3.55 cnf('189', plain, (queue_190 = store(queue_187,head,index_189)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp179'])).
% 24.10/3.55 cnf('190', plain, (select(queue_190,head) = index_189),
% 24.10/3.55 inference(paramodulation,[],['189','9'])).
% 24.10/3.55 cnf('191', plain, (select(queue_194,head) = index_189 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['188','190'])).
% 24.10/3.55 cnf('192', plain, (select(queue_196,head) = index_189 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['184','191'])).
% 24.10/3.55 cnf('193', plain, (q7 = queue_196),
% 24.10/3.55 inference(cnf_transformation,[],['hyp243'])).
% 24.10/3.55 cnf('194', plain, (queue_200 = store(q7,seq,earray_199)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp182'])).
% 24.10/3.55 cnf('195', plain, (queue_200 = store(queue_196,seq,earray_199)),
% 24.10/3.55 inference(paramodulation,[],['193','194'])).
% 24.10/3.55 cnf('196', plain, (select(queue_200,X) = select(queue_196,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['195','2'])).
% 24.10/3.55 cnf('197', plain, (select(queue_200,head) = index_189 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['192','196'])).
% 24.10/3.55 cnf('198', plain, (queue_208 = store(queue_206,tail,index_207)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp185'])).
% 24.10/3.55 cnf('199', plain, (select(queue_208,X) = select(queue_206,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['198','2'])).
% 24.10/3.55 cnf('200', plain, (index_209 = select(queue_208,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp107'])).
% 24.10/3.55 cnf('201', plain, (index_209 = select(queue_206,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['199','200'])).
% 24.10/3.55 cnf('202', plain, (q8 = queue_202),
% 24.10/3.55 inference(cnf_transformation,[],['hyp244'])).
% 24.10/3.55 cnf('203', plain, (queue_206 = store(q8,seq,earray_205)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp184'])).
% 24.10/3.55 cnf('204', plain, (queue_206 = store(queue_202,seq,earray_205)),
% 24.10/3.55 inference(paramodulation,[],['202','203'])).
% 24.10/3.55 cnf('205', plain, (select(queue_206,X) = select(queue_202,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['204','2'])).
% 24.10/3.55 cnf('206', plain, (index_209 = select(queue_202,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['201','205'])).
% 24.10/3.55 cnf('207', plain, (queue_202 = store(queue_200,tail,index_201)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp183'])).
% 24.10/3.55 cnf('208', plain, (select(queue_202,X) = select(queue_200,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['207','2'])).
% 24.10/3.55 cnf('209', plain, (index_209 = select(queue_200,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['206','208'])).
% 24.10/3.55 cnf('210', plain, (seq = head | tail = head | index_209 = index_189),
% 24.10/3.55 inference(paramodulation,[],['197','209'])).
% 24.10/3.55 cnf('211', plain, (tail = head | index_209 = index_189),
% 24.10/3.55 inference(paramodulation,[],['210','74'])).
% 24.10/3.55 cnf('212', plain, (index_209 = index_189),
% 24.10/3.55 inference(paramodulation,[],['211','76'])).
% 24.10/3.55 cnf('213', plain, (select(queue_7,tail) = index_6),
% 24.10/3.55 inference(paramodulation,[],['137','9'])).
% 24.10/3.55 cnf('214', plain, (index_78 = select(q1,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp134'])).
% 24.10/3.55 cnf('215', plain, (index_78 = select(queue_7,tail)),
% 24.10/3.55 inference(paramodulation,[],['147','214'])).
% 24.10/3.55 cnf('216', plain, (index_78 = index_6),
% 24.10/3.55 inference(simplify,[],['213','215'])).
% 24.10/3.55 cnf('217', plain, (index_81 = s(index_78)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp135'])).
% 24.10/3.55 cnf('218', plain, (index_81 = s(index_6)),
% 24.10/3.55 inference(paramodulation,[],['216','217'])).
% 24.10/3.55 cnf('219', plain, (index_209 = index_81 | seq = head | tail = head),
% 24.10/3.55 inference(simplify,[then_simplify],['182','212','218'])).
% 24.10/3.55 cnf('220', plain, (seq = head | tail = head | index_81 = index_189),
% 24.10/3.55 inference(paramodulation,[],['219','212'])).
% 24.10/3.55 cnf('221', plain, (seq = head | tail = head | index_81 = index_209),
% 24.10/3.55 inference(simplify,[],['220','212'])).
% 24.10/3.55 cnf('222', plain, (tail = head | index_81 = index_209),
% 24.10/3.55 inference(paramodulation,[],['221','74'])).
% 24.10/3.55 cnf('223', plain, (index_81 = index_209),
% 24.10/3.55 inference(paramodulation,[],['222','76'])).
% 24.10/3.55 cnf('224', plain, (index_210 = s(index_209)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp109'])).
% 24.10/3.55 cnf('225', plain, (index_210 = s(index_81)),
% 24.10/3.55 inference(paramodulation,[],['223','224'])).
% 24.10/3.55 cnf('226', plain, (select(queue_82,tail) = index_81),
% 24.10/3.55 inference(paramodulation,[],['134','9'])).
% 24.10/3.55 cnf('227', plain, (index_153 = select(q2,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp84'])).
% 24.10/3.55 cnf('228', plain, (index_153 = select(queue_82,tail)),
% 24.10/3.55 inference(paramodulation,[],['129','227'])).
% 24.10/3.55 cnf('229', plain, (index_153 = index_81),
% 24.10/3.55 inference(simplify,[],['226','228'])).
% 24.10/3.55 cnf('230', plain, (index_156 = s(index_153)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp85'])).
% 24.10/3.55 cnf('231', plain, (index_156 = s(index_81)),
% 24.10/3.55 inference(paramodulation,[],['229','230'])).
% 24.10/3.55 cnf('232', plain, (index_210 = index_156),
% 24.10/3.55 inference(simplify,[],['225','231'])).
% 24.10/3.55 cnf('233', plain, (select(queue_160,X) = select(queue_157,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['116','2'])).
% 24.10/3.55 cnf('234', plain, (select(queue_157,tail) = index_156),
% 24.10/3.55 inference(paramodulation,[],['125','9'])).
% 24.10/3.55 cnf('235', plain, (select(queue_160,tail) = index_156),
% 24.10/3.55 inference(paramodulation,[then_simplify],['233','234','157'])).
% 24.10/3.55 cnf('236', plain, (index_171 = select(q3,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp92'])).
% 24.10/3.55 cnf('237', plain, (index_171 = select(queue_160,tail)),
% 24.10/3.55 inference(paramodulation,[],['112','236'])).
% 24.10/3.55 cnf('238', plain, (index_171 = index_156),
% 24.10/3.55 inference(simplify,[],['235','237'])).
% 24.10/3.55 cnf('239', plain, (index_174 = s(index_171)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp93'])).
% 24.10/3.55 cnf('240', plain, (index_174 = s(index_156)),
% 24.10/3.55 inference(paramodulation,[],['238','239'])).
% 24.10/3.55 cnf('241', plain, (index_174 = s(index_210)),
% 24.10/3.55 inference(paramodulation,[],['232','240'])).
% 24.10/3.55 cnf('242', plain, (index_174 = s(index_26)),
% 24.10/3.55 inference(paramodulation,[],['109','241'])).
% 24.10/3.55 cnf('243', plain, (index_27 = s(index_26)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp113'])).
% 24.10/3.55 cnf('244', plain, (queue_34 = store(queue_32,tail,index_33)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp191'])).
% 24.10/3.55 cnf('245', plain, (select(queue_34,X) = select(queue_32,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['244','2'])).
% 24.10/3.55 cnf('246', plain, (q12 = queue_28),
% 24.10/3.55 inference(cnf_transformation,[],['hyp219'])).
% 24.10/3.55 cnf('247', plain, (queue_32 = store(q12,seq,earray_31)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp190'])).
% 24.10/3.55 cnf('248', plain, (queue_32 = store(queue_28,seq,earray_31)),
% 24.10/3.55 inference(paramodulation,[],['246','247'])).
% 24.10/3.55 cnf('249', plain, (select(queue_32,X) = select(queue_28,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['248','2'])).
% 24.10/3.55 cnf('250', plain, (queue_28 = store(queue_25,head,index_27)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp189'])).
% 24.10/3.55 cnf('251', plain, (select(queue_28,head) = index_27),
% 24.10/3.55 inference(paramodulation,[],['250','9'])).
% 24.10/3.55 cnf('252', plain, (select(queue_32,head) = index_27 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['249','251'])).
% 24.10/3.55 cnf('253', plain, (select(queue_34,head) = index_27 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['245','252'])).
% 24.10/3.55 cnf('254', plain, (q13 = queue_34),
% 24.10/3.55 inference(cnf_transformation,[],['hyp220'])).
% 24.10/3.55 cnf('255', plain, (queue_38 = store(q13,seq,earray_37)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp192'])).
% 24.10/3.55 cnf('256', plain, (queue_38 = store(queue_34,seq,earray_37)),
% 24.10/3.55 inference(paramodulation,[],['254','255'])).
% 24.10/3.55 cnf('257', plain, (select(queue_38,X) = select(queue_34,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['256','2'])).
% 24.10/3.55 cnf('258', plain, (select(queue_38,head) = index_27 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['253','257'])).
% 24.10/3.55 cnf('259', plain, (queue_46 = store(queue_44,tail,index_45)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp195'])).
% 24.10/3.55 cnf('260', plain, (select(queue_46,X) = select(queue_44,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['259','2'])).
% 24.10/3.55 cnf('261', plain, (index_47 = select(queue_46,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp121'])).
% 24.10/3.55 cnf('262', plain, (index_47 = select(queue_44,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['260','261'])).
% 24.10/3.55 cnf('263', plain, (q14 = queue_40),
% 24.10/3.55 inference(cnf_transformation,[],['hyp221'])).
% 24.10/3.55 cnf('264', plain, (queue_44 = store(q14,seq,earray_43)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp194'])).
% 24.10/3.55 cnf('265', plain, (queue_44 = store(queue_40,seq,earray_43)),
% 24.10/3.55 inference(paramodulation,[],['263','264'])).
% 24.10/3.55 cnf('266', plain, (select(queue_44,X) = select(queue_40,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['265','2'])).
% 24.10/3.55 cnf('267', plain, (index_47 = select(queue_40,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['262','266'])).
% 24.10/3.55 cnf('268', plain, (queue_40 = store(queue_38,tail,index_39)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp193'])).
% 24.10/3.55 cnf('269', plain, (select(queue_40,X) = select(queue_38,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['268','2'])).
% 24.10/3.55 cnf('270', plain, (index_47 = select(queue_38,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['267','269'])).
% 24.10/3.55 cnf('271', plain, (seq = head | tail = head | index_47 = index_27),
% 24.10/3.55 inference(paramodulation,[],['258','270'])).
% 24.10/3.55 cnf('272', plain, (tail = head | index_47 = index_27),
% 24.10/3.55 inference(paramodulation,[],['271','74'])).
% 24.10/3.55 cnf('273', plain, (index_47 = index_27),
% 24.10/3.55 inference(paramodulation,[],['272','76'])).
% 24.10/3.55 cnf('274', plain, (index_174 = index_47),
% 24.10/3.55 inference(simplify,[then_simplify],['242','243','273'])).
% 24.10/3.55 cnf('275', plain, (select(queue_175,tail) = index_174),
% 24.10/3.55 inference(paramodulation,[],['110','9'])).
% 24.10/3.55 cnf('276', plain, (index_177 = select(q4,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp94'])).
% 24.10/3.55 cnf('277', plain, (index_177 = select(queue_175,tail)),
% 24.10/3.55 inference(paramodulation,[],['120','276'])).
% 24.10/3.55 cnf('278', plain, (index_177 = index_174),
% 24.10/3.55 inference(simplify,[],['275','277'])).
% 24.10/3.55 cnf('279', plain, (index_180 = s(index_177)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp96'])).
% 24.10/3.55 cnf('280', plain, (index_180 = s(index_174)),
% 24.10/3.55 inference(paramodulation,[],['278','279'])).
% 24.10/3.55 cnf('281', plain, (index_180 = s(index_47)),
% 24.10/3.55 inference(paramodulation,[],['274','280'])).
% 24.10/3.55 cnf('282', plain, (index_48 = s(index_47)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp122'])).
% 24.10/3.55 cnf('283', plain, (queue_55 = store(queue_53,tail,index_54)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp199'])).
% 24.10/3.55 cnf('284', plain, (select(queue_55,X) = select(queue_53,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['283','2'])).
% 24.10/3.55 cnf('285', plain, (q15 = queue_49),
% 24.10/3.55 inference(cnf_transformation,[],['hyp222'])).
% 24.10/3.55 cnf('286', plain, (queue_53 = store(q15,seq,earray_52)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp198'])).
% 24.10/3.55 cnf('287', plain, (queue_53 = store(queue_49,seq,earray_52)),
% 24.10/3.55 inference(paramodulation,[],['285','286'])).
% 24.10/3.55 cnf('288', plain, (select(queue_53,X) = select(queue_49,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['287','2'])).
% 24.10/3.55 cnf('289', plain, (queue_49 = store(queue_46,head,index_48)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp196'])).
% 24.10/3.55 cnf('290', plain, (select(queue_49,head) = index_48),
% 24.10/3.55 inference(paramodulation,[],['289','9'])).
% 24.10/3.55 cnf('291', plain, (select(queue_53,head) = index_48 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['288','290'])).
% 24.10/3.55 cnf('292', plain, (select(queue_55,head) = index_48 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['284','291'])).
% 24.10/3.55 cnf('293', plain, (q16 = queue_55),
% 24.10/3.55 inference(cnf_transformation,[],['hyp223'])).
% 24.10/3.55 cnf('294', plain, (queue_59 = store(q16,seq,earray_58)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp200'])).
% 24.10/3.55 cnf('295', plain, (queue_59 = store(queue_55,seq,earray_58)),
% 24.10/3.55 inference(paramodulation,[],['293','294'])).
% 24.10/3.55 cnf('296', plain, (select(queue_59,X) = select(queue_55,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['295','2'])).
% 24.10/3.55 cnf('297', plain, (select(queue_59,head) = index_48 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['292','296'])).
% 24.10/3.55 cnf('298', plain, (queue_67 = store(queue_65,tail,index_66)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp203'])).
% 24.10/3.55 cnf('299', plain, (select(queue_67,X) = select(queue_65,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['298','2'])).
% 24.10/3.55 cnf('300', plain, (index_68 = select(queue_67,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp130'])).
% 24.10/3.55 cnf('301', plain, (index_68 = select(queue_65,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['299','300'])).
% 24.10/3.55 cnf('302', plain, (q17 = queue_61),
% 24.10/3.55 inference(cnf_transformation,[],['hyp224'])).
% 24.10/3.55 cnf('303', plain, (queue_65 = store(q17,seq,earray_64)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp202'])).
% 24.10/3.55 cnf('304', plain, (queue_65 = store(queue_61,seq,earray_64)),
% 24.10/3.55 inference(paramodulation,[],['302','303'])).
% 24.10/3.55 cnf('305', plain, (select(queue_65,X) = select(queue_61,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['304','2'])).
% 24.10/3.55 cnf('306', plain, (index_68 = select(queue_61,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['301','305'])).
% 24.10/3.55 cnf('307', plain, (queue_61 = store(queue_59,tail,index_60)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp201'])).
% 24.10/3.55 cnf('308', plain, (select(queue_61,X) = select(queue_59,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['307','2'])).
% 24.10/3.55 cnf('309', plain, (index_68 = select(queue_59,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['306','308'])).
% 24.10/3.55 cnf('310', plain, (seq = head | tail = head | index_68 = index_48),
% 24.10/3.55 inference(paramodulation,[],['297','309'])).
% 24.10/3.55 cnf('311', plain, (tail = head | index_68 = index_48),
% 24.10/3.55 inference(paramodulation,[],['310','74'])).
% 24.10/3.55 cnf('312', plain, (index_68 = index_48),
% 24.10/3.55 inference(paramodulation,[],['311','76'])).
% 24.10/3.55 cnf('313', plain, (index_180 = index_68),
% 24.10/3.55 inference(simplify,[then_simplify],['281','282','312'])).
% 24.10/3.55 cnf('314', plain, (select(queue_181,tail) = index_180),
% 24.10/3.55 inference(paramodulation,[],['177','9'])).
% 24.10/3.55 cnf('315', plain, (index_183 = select(q5,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp97'])).
% 24.10/3.55 cnf('316', plain, (index_183 = select(queue_181,tail)),
% 24.10/3.55 inference(paramodulation,[],['172','315'])).
% 24.10/3.55 cnf('317', plain, (index_183 = index_180),
% 24.10/3.55 inference(simplify,[],['314','316'])).
% 24.10/3.55 cnf('318', plain, (index_186 = s(index_183)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp98'])).
% 24.10/3.55 cnf('319', plain, (index_186 = s(index_180)),
% 24.10/3.55 inference(paramodulation,[],['317','318'])).
% 24.10/3.55 cnf('320', plain, (index_186 = s(index_68)),
% 24.10/3.55 inference(paramodulation,[],['313','319'])).
% 24.10/3.55 cnf('321', plain, (index_69 = s(index_68)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp131'])).
% 24.10/3.55 cnf('322', plain, (queue_76 = store(queue_74,tail,index_75)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp207'])).
% 24.10/3.55 cnf('323', plain, (select(queue_76,X) = select(queue_74,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['322','2'])).
% 24.10/3.55 cnf('324', plain, (q18 = queue_70),
% 24.10/3.55 inference(cnf_transformation,[],['hyp225'])).
% 24.10/3.55 cnf('325', plain, (queue_74 = store(q18,seq,earray_73)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp206'])).
% 24.10/3.55 cnf('326', plain, (queue_74 = store(queue_70,seq,earray_73)),
% 24.10/3.55 inference(paramodulation,[],['324','325'])).
% 24.10/3.55 cnf('327', plain, (select(queue_74,X) = select(queue_70,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['326','2'])).
% 24.10/3.55 cnf('328', plain, (queue_70 = store(queue_67,head,index_69)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp205'])).
% 24.10/3.55 cnf('329', plain, (select(queue_70,head) = index_69),
% 24.10/3.55 inference(paramodulation,[],['328','9'])).
% 24.10/3.55 cnf('330', plain, (select(queue_74,head) = index_69 | seq = head),
% 24.10/3.55 inference(paramodulation,[],['327','329'])).
% 24.10/3.55 cnf('331', plain, (select(queue_76,head) = index_69 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['323','330'])).
% 24.10/3.55 cnf('332', plain, (q19 = queue_76),
% 24.10/3.55 inference(cnf_transformation,[],['hyp226'])).
% 24.10/3.55 cnf('333', plain, (queue_86 = store(q19,seq,earray_85)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp210'])).
% 24.10/3.55 cnf('334', plain, (queue_86 = store(queue_76,seq,earray_85)),
% 24.10/3.55 inference(paramodulation,[],['332','333'])).
% 24.10/3.55 cnf('335', plain, (select(queue_86,X) = select(queue_76,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['334','2'])).
% 24.10/3.55 cnf('336', plain, (select(queue_86,head) = index_69 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['331','335'])).
% 24.10/3.55 cnf('337', plain, (queue_94 = store(queue_92,tail,index_93)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp213'])).
% 24.10/3.55 cnf('338', plain, (select(queue_94,X) = select(queue_92,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['337','2'])).
% 24.10/3.55 cnf('339', plain, (index_95 = select(queue_94,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp141'])).
% 24.10/3.55 cnf('340', plain, (index_95 = select(queue_92,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['338','339'])).
% 24.10/3.55 cnf('341', plain, (q20 = queue_88),
% 24.10/3.55 inference(cnf_transformation,[],['hyp228'])).
% 24.10/3.55 cnf('342', plain, (queue_92 = store(q20,seq,earray_91)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp212'])).
% 24.10/3.55 cnf('343', plain, (queue_92 = store(queue_88,seq,earray_91)),
% 24.10/3.55 inference(paramodulation,[],['341','342'])).
% 24.10/3.55 cnf('344', plain, (select(queue_92,X) = select(queue_88,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['343','2'])).
% 24.10/3.55 cnf('345', plain, (index_95 = select(queue_88,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['340','344'])).
% 24.10/3.55 cnf('346', plain, (queue_88 = store(queue_86,tail,index_87)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp211'])).
% 24.10/3.55 cnf('347', plain, (select(queue_88,X) = select(queue_86,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['346','2'])).
% 24.10/3.55 cnf('348', plain, (index_95 = select(queue_86,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['345','347'])).
% 24.10/3.55 cnf('349', plain, (seq = head | tail = head | index_95 = index_69),
% 24.10/3.55 inference(paramodulation,[],['336','348'])).
% 24.10/3.55 cnf('350', plain, (tail = head | index_95 = index_69),
% 24.10/3.55 inference(paramodulation,[],['349','74'])).
% 24.10/3.55 cnf('351', plain, (index_95 = index_69),
% 24.10/3.55 inference(paramodulation,[],['350','76'])).
% 24.10/3.55 cnf('352', plain, (index_186 = index_95),
% 24.10/3.55 inference(simplify,[then_simplify],['320','321','351'])).
% 24.10/3.55 cnf('353', plain, (select(queue_190,X) = select(queue_187,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['189','2'])).
% 24.10/3.55 cnf('354', plain, (select(queue_187,tail) = index_186),
% 24.10/3.55 inference(paramodulation,[],['168','9'])).
% 24.10/3.55 cnf('355', plain, (select(queue_190,tail) = index_186),
% 24.10/3.55 inference(paramodulation,[then_simplify],['353','354','157'])).
% 24.10/3.55 cnf('356', plain, (index_192 = select(q6,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp101'])).
% 24.10/3.55 cnf('357', plain, (index_192 = select(queue_190,tail)),
% 24.10/3.55 inference(paramodulation,[],['185','356'])).
% 24.10/3.55 cnf('358', plain, (index_192 = index_186),
% 24.10/3.55 inference(simplify,[],['355','357'])).
% 24.10/3.55 cnf('359', plain, (index_195 = s(index_192)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp102'])).
% 24.10/3.55 cnf('360', plain, (index_195 = s(index_186)),
% 24.10/3.55 inference(paramodulation,[],['358','359'])).
% 24.10/3.55 cnf('361', plain, (index_195 = s(index_95)),
% 24.10/3.55 inference(paramodulation,[],['352','360'])).
% 24.10/3.55 cnf('362', plain, (index_96 = s(index_95)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp142'])).
% 24.10/3.55 cnf('363', plain, (index_195 = index_96),
% 24.10/3.55 inference(simplify,[],['361','362'])).
% 24.10/3.55 cnf('364', plain, (select(queue_196,tail) = index_195),
% 24.10/3.55 inference(paramodulation,[],['183','9'])).
% 24.10/3.55 cnf('365', plain, (index_198 = select(q7,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp103'])).
% 24.10/3.55 cnf('366', plain, (index_198 = select(queue_196,tail)),
% 24.10/3.55 inference(paramodulation,[],['193','365'])).
% 24.10/3.55 cnf('367', plain, (index_198 = index_195),
% 24.10/3.55 inference(simplify,[],['364','366'])).
% 24.10/3.55 cnf('368', plain, (index_201 = s(index_198)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp104'])).
% 24.10/3.55 cnf('369', plain, (index_201 = s(index_195)),
% 24.10/3.55 inference(paramodulation,[],['367','368'])).
% 24.10/3.55 cnf('370', plain, (index_201 = s(index_96)),
% 24.10/3.55 inference(paramodulation,[],['363','369'])).
% 24.10/3.55 cnf('371', plain, (index_117 = index_201),
% 24.10/3.55 inference(simplify,[],['79','370'])).
% 24.10/3.55 cnf('372', plain, (seq = head | tail = head | index_137 = index_201),
% 24.10/3.55 inference(simplify,[],['45','371'])).
% 24.10/3.55 cnf('373', plain, (tail = head | index_137 = index_201),
% 24.10/3.55 inference(paramodulation,[],['372','74'])).
% 24.10/3.55 cnf('374', plain, (index_137 = index_201),
% 24.10/3.55 inference(paramodulation,[],['373','76'])).
% 24.10/3.55 cnf('375', plain, (index_138 = s(index_137)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp78'])).
% 24.10/3.55 cnf('376', plain, (index_138 = s(index_201)),
% 24.10/3.55 inference(paramodulation,[],['374','375'])).
% 24.10/3.55 cnf('377', plain, (select(queue_202,tail) = index_201),
% 24.10/3.55 inference(paramodulation,[],['207','9'])).
% 24.10/3.55 cnf('378', plain, (index_204 = select(q8,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp105'])).
% 24.10/3.55 cnf('379', plain, (index_204 = select(queue_202,tail)),
% 24.10/3.55 inference(paramodulation,[],['202','378'])).
% 24.10/3.55 cnf('380', plain, (index_204 = index_201),
% 24.10/3.55 inference(simplify,[],['377','379'])).
% 24.10/3.55 cnf('381', plain, (index_207 = s(index_204)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp106'])).
% 24.10/3.55 cnf('382', plain, (index_207 = s(index_201)),
% 24.10/3.55 inference(paramodulation,[],['380','381'])).
% 24.10/3.55 cnf('383', plain, (index_138 = index_207),
% 24.10/3.55 inference(simplify,[],['376','382'])).
% 24.10/3.55 cnf('384', plain, (select(queue_149,head) = index_207 | seq = head | tail = head),
% 24.10/3.55 inference(simplify,[],['17','383'])).
% 24.10/3.55 cnf('385', plain, (queue_166 = store(queue_164,tail,index_165)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp169'])).
% 24.10/3.55 cnf('386', plain, (select(queue_166,X) = select(queue_164,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['385','2'])).
% 24.10/3.55 cnf('387', plain, (index_167 = select(queue_166,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp90'])).
% 24.10/3.55 cnf('388', plain, (index_167 = select(queue_164,head) | tail = head),
% 24.10/3.55 inference(paramodulation,[],['386','387'])).
% 24.10/3.55 cnf('389', plain, (q29 = queue_151),
% 24.10/3.55 inference(cnf_transformation,[],['hyp237'])).
% 24.10/3.55 cnf('390', plain, (queue_164 = store(q29,seq,earray_163)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp168'])).
% 24.10/3.55 cnf('391', plain, (queue_164 = store(queue_151,seq,earray_163)),
% 24.10/3.55 inference(paramodulation,[],['389','390'])).
% 24.10/3.55 cnf('392', plain, (select(queue_164,X) = select(queue_151,X) | seq = X),
% 24.10/3.55 inference(paramodulation,[],['391','2'])).
% 24.10/3.55 cnf('393', plain, (index_167 = select(queue_151,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['388','392'])).
% 24.10/3.55 cnf('394', plain, (queue_151 = store(queue_149,tail,index_150)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp164'])).
% 24.10/3.55 cnf('395', plain, (select(queue_151,X) = select(queue_149,X) | tail = X),
% 24.10/3.55 inference(paramodulation,[],['394','2'])).
% 24.10/3.55 cnf('396', plain, (index_167 = select(queue_149,head) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['393','395'])).
% 24.10/3.55 cnf('397', plain, (index_167 = index_207 | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['384','396'])).
% 24.10/3.55 cnf('398', plain, (index_168 = s(index_167)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp91'])).
% 24.10/3.55 cnf('399', plain, (index_168 = s(index_207) | seq = head | tail = head),
% 24.10/3.55 inference(paramodulation,[],['397','398'])).
% 24.10/3.55 cnf('400', plain, (select(queue_211,X) = select(queue_208,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['82','2'])).
% 24.10/3.55 cnf('401', plain, (select(queue_208,tail) = index_207),
% 24.10/3.55 inference(paramodulation,[],['198','9'])).
% 24.10/3.55 cnf('402', plain, (select(queue_211,tail) = index_207),
% 24.10/3.55 inference(paramodulation,[then_simplify],['400','401','157'])).
% 24.10/3.55 cnf('403', plain, (index_9 = select(q9,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp138'])).
% 24.10/3.55 cnf('404', plain, (index_9 = select(queue_211,tail)),
% 24.10/3.55 inference(paramodulation,[],['84','403'])).
% 24.10/3.55 cnf('405', plain, (index_9 = index_207),
% 24.10/3.55 inference(simplify,[],['402','404'])).
% 24.10/3.55 cnf('406', plain, (index_12 = s(index_9)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp70'])).
% 24.10/3.55 cnf('407', plain, (index_12 = s(index_207)),
% 24.10/3.55 inference(paramodulation,[],['405','406'])).
% 24.10/3.55 cnf('408', plain, (index_168 = index_12 | seq = head | tail = head),
% 24.10/3.55 inference(simplify,[],['399','407'])).
% 24.10/3.55 cnf('409', plain, (select(queue_13,tail) = index_12),
% 24.10/3.55 inference(paramodulation,[],['80','9'])).
% 24.10/3.55 cnf('410', plain, (index_15 = select(q10,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp82'])).
% 24.10/3.55 cnf('411', plain, (index_15 = select(queue_13,tail)),
% 24.10/3.55 inference(paramodulation,[],['90','410'])).
% 24.10/3.55 cnf('412', plain, (index_15 = index_12),
% 24.10/3.55 inference(simplify,[],['409','411'])).
% 24.10/3.55 cnf('413', plain, (seq = head | tail = head | index_15 = index_168),
% 24.10/3.55 inference(paramodulation,[],['408','412'])).
% 24.10/3.55 cnf('414', plain, (seq = head | tail = head | index_12 = index_168),
% 24.10/3.55 inference(simplify,[],['413','412'])).
% 24.10/3.55 cnf('415', plain, (tail = head | index_12 = index_168),
% 24.10/3.55 inference(paramodulation,[],['414','74'])).
% 24.10/3.55 cnf('416', plain, (index_12 = index_168),
% 24.10/3.55 inference(paramodulation,[],['415','76'])).
% 24.10/3.55 cnf('417', plain, (select(queue_28,X) = select(queue_25,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['250','2'])).
% 24.10/3.55 cnf('418', plain, (select(queue_23,seq) = earray_22),
% 24.10/3.55 inference(paramodulation,[],['100','9'])).
% 24.10/3.55 cnf('419', plain, (tail != seq),
% 24.10/3.55 inference(cnf_transformation,[],['tail_distinct_from_seq'])).
% 24.10/3.55 cnf('420', plain, (select(queue_25,seq) = earray_22),
% 24.10/3.55 inference(paramodulation,[then_simplify],['418','96','419'])).
% 24.10/3.55 cnf('421', plain, (head != seq),
% 24.10/3.55 inference(cnf_transformation,[],['head_distinct_from_seq'])).
% 24.10/3.55 cnf('422', plain, (select(queue_28,seq) = earray_22),
% 24.10/3.55 inference(paramodulation,[then_simplify],['417','420','421'])).
% 24.10/3.55 cnf('423', plain, (earray_29 = select(q12,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp38'])).
% 24.10/3.55 cnf('424', plain, (earray_29 = select(queue_28,seq)),
% 24.10/3.55 inference(paramodulation,[],['246','423'])).
% 24.10/3.55 cnf('425', plain, (earray_29 = earray_22),
% 24.10/3.55 inference(simplify,[],['422','424'])).
% 24.10/3.55 cnf('426', plain, (select(queue_17,seq) = earray_16),
% 24.10/3.55 inference(paramodulation,[],['91','9'])).
% 24.10/3.55 cnf('427', plain, (select(queue_19,seq) = earray_16),
% 24.10/3.55 inference(paramodulation,[then_simplify],['105','426','419'])).
% 24.10/3.55 cnf('428', plain, (earray_20 = select(q11,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp33'])).
% 24.10/3.55 cnf('429', plain, (earray_20 = select(queue_19,seq)),
% 24.10/3.55 inference(paramodulation,[],['99','428'])).
% 24.10/3.55 cnf('430', plain, (earray_20 = earray_16),
% 24.10/3.55 inference(simplify,[],['427','429'])).
% 24.10/3.55 cnf('431', plain, (earray_16 = store(earray_14,index_15,e10)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp19'])).
% 24.10/3.55 cnf('432', plain, (select(earray_16,index_15) = e10),
% 24.10/3.55 inference(paramodulation,[],['431','9'])).
% 24.10/3.55 cnf('433', plain, (select(earray_16,index_12) = e10),
% 24.10/3.55 inference(paramodulation,[],['412','432'])).
% 24.10/3.55 cnf('434', plain, (select(earray_20,index_12) = e10),
% 24.10/3.55 inference(paramodulation,[],['430','433'])).
% 24.10/3.55 cnf('435', plain, (select(queue_19,tail) = index_18),
% 24.10/3.55 inference(paramodulation,[],['104','9'])).
% 24.10/3.55 cnf('436', plain, (index_21 = select(q11,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp108'])).
% 24.10/3.55 cnf('437', plain, (index_21 = select(queue_19,tail)),
% 24.10/3.55 inference(paramodulation,[],['99','436'])).
% 24.10/3.55 cnf('438', plain, (index_21 = index_18),
% 24.10/3.55 inference(simplify,[],['435','437'])).
% 24.10/3.55 cnf('439', plain, (earray_22 = store(earray_20,index_21,e11)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp37'])).
% 24.10/3.55 cnf('440', plain, (earray_22 = store(earray_20,index_18,e11)),
% 24.10/3.55 inference(paramodulation,[],['438','439'])).
% 24.10/3.55 cnf('441', plain, (select(earray_22,X) = select(earray_20,X) | index_18 = X),
% 24.10/3.55 inference(paramodulation,[],['440','2'])).
% 24.10/3.55 cnf('442', plain, (index_18 = s(index_15)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp95'])).
% 24.10/3.55 cnf('443', plain, (index_18 = s(index_12)),
% 24.10/3.55 inference(paramodulation,[],['412','442'])).
% 24.10/3.55 cnf('444', plain, (s(X) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as1'])).
% 24.10/3.55 cnf('445', plain, (index_18 != index_12),
% 24.10/3.55 inference(paramodulation,[],['443','444'])).
% 24.10/3.55 cnf('446', plain, (select(earray_22,index_12) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['434','441','445'])).
% 24.10/3.55 cnf('447', plain, (select(earray_29,index_12) = e10),
% 24.10/3.55 inference(paramodulation,[],['425','446'])).
% 24.10/3.55 cnf('448', plain, (select(earray_29,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[],['416','447'])).
% 24.10/3.55 cnf('449', plain, (earray_31 = store(earray_29,index_30,e12)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp39'])).
% 24.10/3.55 cnf('450', plain, (select(earray_31,X3) = select(earray_29,X3) | index_30 = X3),
% 24.10/3.55 inference(paramodulation,[],['449','2'])).
% 24.10/3.55 cnf('451', plain, (select(queue_32,seq) = earray_31),
% 24.10/3.55 inference(paramodulation,[],['247','9'])).
% 24.10/3.55 cnf('452', plain, (select(queue_34,seq) = earray_31),
% 24.10/3.55 inference(paramodulation,[then_simplify],['245','451','419'])).
% 24.10/3.55 cnf('453', plain, (earray_35 = select(q13,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp40'])).
% 24.10/3.55 cnf('454', plain, (earray_35 = select(queue_34,seq)),
% 24.10/3.55 inference(paramodulation,[],['254','453'])).
% 24.10/3.55 cnf('455', plain, (earray_35 = earray_31),
% 24.10/3.55 inference(simplify,[],['452','454'])).
% 24.10/3.55 cnf('456', plain, (select(queue_25,tail) = index_24),
% 24.10/3.55 inference(paramodulation,[],['95','9'])).
% 24.10/3.55 cnf('457', plain, (select(queue_28,tail) = index_24),
% 24.10/3.55 inference(paramodulation,[then_simplify],['417','456','157'])).
% 24.10/3.55 cnf('458', plain, (index_30 = select(q12,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp115'])).
% 24.10/3.55 cnf('459', plain, (index_30 = select(queue_28,tail)),
% 24.10/3.55 inference(paramodulation,[],['246','458'])).
% 24.10/3.55 cnf('460', plain, (index_30 = index_24),
% 24.10/3.55 inference(simplify,[],['457','459'])).
% 24.10/3.55 cnf('461', plain, (select(earray_35,X) = select(earray_29,X) | index_24 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['450','455','460'])).
% 24.10/3.55 cnf('462', plain, (s(s(X)) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as2'])).
% 24.10/3.55 cnf('463', plain, (s(index_18) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','462'])).
% 24.10/3.55 cnf('464', plain, (index_24 = s(index_21)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp111'])).
% 24.10/3.55 cnf('465', plain, (index_24 = s(index_18)),
% 24.10/3.55 inference(paramodulation,[],['438','464'])).
% 24.10/3.55 cnf('466', plain, (index_24 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['463','465','412'])).
% 24.10/3.55 cnf('467', plain, (index_24 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','466'])).
% 24.10/3.55 cnf('468', plain, (select(earray_35,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['448','461','467'])).
% 24.10/3.55 cnf('469', plain, (earray_37 = store(earray_35,index_36,e13)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp41'])).
% 24.10/3.55 cnf('470', plain, (select(earray_37,X3) = select(earray_35,X3) | index_36 = X3),
% 24.10/3.55 inference(paramodulation,[],['469','2'])).
% 24.10/3.55 cnf('471', plain, (select(queue_38,seq) = earray_37),
% 24.10/3.55 inference(paramodulation,[],['255','9'])).
% 24.10/3.55 cnf('472', plain, (select(queue_40,seq) = earray_37),
% 24.10/3.55 inference(paramodulation,[then_simplify],['269','471','419'])).
% 24.10/3.55 cnf('473', plain, (earray_41 = select(q14,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp43'])).
% 24.10/3.55 cnf('474', plain, (earray_41 = select(queue_40,seq)),
% 24.10/3.55 inference(paramodulation,[],['263','473'])).
% 24.10/3.55 cnf('475', plain, (earray_41 = earray_37),
% 24.10/3.55 inference(simplify,[],['472','474'])).
% 24.10/3.55 cnf('476', plain, (select(queue_34,tail) = index_33),
% 24.10/3.55 inference(paramodulation,[],['244','9'])).
% 24.10/3.55 cnf('477', plain, (index_36 = select(q13,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp117'])).
% 24.10/3.55 cnf('478', plain, (index_36 = select(queue_34,tail)),
% 24.10/3.55 inference(paramodulation,[],['254','477'])).
% 24.10/3.55 cnf('479', plain, (index_36 = index_33),
% 24.10/3.55 inference(simplify,[],['476','478'])).
% 24.10/3.55 cnf('480', plain, (select(earray_41,X) = select(earray_35,X) | index_33 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['470','475','479'])).
% 24.10/3.55 cnf('481', plain, (index_33 = s(index_30)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp116'])).
% 24.10/3.55 cnf('482', plain, (index_33 = s(index_24)),
% 24.10/3.55 inference(paramodulation,[],['460','481'])).
% 24.10/3.55 cnf('483', plain, (s(s(s(X))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as3'])).
% 24.10/3.55 cnf('484', plain, (s(s(index_18)) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','483'])).
% 24.10/3.55 cnf('485', plain, (s(index_24) != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['484','465','412'])).
% 24.10/3.55 cnf('486', plain, (index_33 != index_12),
% 24.10/3.55 inference(paramodulation,[],['482','485'])).
% 24.10/3.55 cnf('487', plain, (index_33 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','486'])).
% 24.10/3.55 cnf('488', plain, (select(earray_41,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['468','480','487'])).
% 24.10/3.55 cnf('489', plain, (earray_43 = store(earray_41,index_42,e14)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp44'])).
% 24.10/3.55 cnf('490', plain, (select(earray_43,X3) = select(earray_41,X3) | index_42 = X3),
% 24.10/3.55 inference(paramodulation,[],['489','2'])).
% 24.10/3.55 cnf('491', plain, (earray_50 = select(q15,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp45'])).
% 24.10/3.55 cnf('492', plain, (earray_50 = select(queue_49,seq)),
% 24.10/3.55 inference(paramodulation,[],['285','491'])).
% 24.10/3.55 cnf('493', plain, (select(queue_49,X) = select(queue_46,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['289','2'])).
% 24.10/3.55 cnf('494', plain, (earray_50 = select(queue_46,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['492','493','421'])).
% 24.10/3.55 cnf('495', plain, (earray_50 = select(queue_44,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['260','494','419'])).
% 24.10/3.55 cnf('496', plain, (select(queue_44,seq) = earray_43),
% 24.10/3.55 inference(paramodulation,[],['264','9'])).
% 24.10/3.55 cnf('497', plain, (earray_50 = earray_43),
% 24.10/3.55 inference(simplify,[],['495','496'])).
% 24.10/3.55 cnf('498', plain, (select(queue_40,tail) = index_39),
% 24.10/3.55 inference(paramodulation,[],['268','9'])).
% 24.10/3.55 cnf('499', plain, (index_42 = select(q14,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp119'])).
% 24.10/3.55 cnf('500', plain, (index_42 = select(queue_40,tail)),
% 24.10/3.55 inference(paramodulation,[],['263','499'])).
% 24.10/3.55 cnf('501', plain, (index_42 = index_39),
% 24.10/3.55 inference(simplify,[],['498','500'])).
% 24.10/3.55 cnf('502', plain, (select(earray_50,X) = select(earray_41,X) | index_39 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['490','497','501'])).
% 24.10/3.55 cnf('503', plain, (s(s(s(s(X)))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as4'])).
% 24.10/3.55 cnf('504', plain, (s(s(s(index_18))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','503'])).
% 24.10/3.55 cnf('505', plain, (s(s(index_24)) != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['504','465','412'])).
% 24.10/3.55 cnf('506', plain, (s(index_33) != index_12),
% 24.10/3.55 inference(paramodulation,[],['482','505'])).
% 24.10/3.55 cnf('507', plain, (index_39 = s(index_36)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp118'])).
% 24.10/3.55 cnf('508', plain, (index_39 = s(index_33)),
% 24.10/3.55 inference(paramodulation,[],['479','507'])).
% 24.10/3.55 cnf('509', plain, (index_39 != index_12),
% 24.10/3.55 inference(simplify,[],['506','508'])).
% 24.10/3.55 cnf('510', plain, (index_39 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','509'])).
% 24.10/3.55 cnf('511', plain, (select(earray_50,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['488','502','510'])).
% 24.10/3.55 cnf('512', plain, (earray_52 = store(earray_50,index_51,e15)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp46'])).
% 24.10/3.55 cnf('513', plain, (select(earray_52,X3) = select(earray_50,X3) | index_51 = X3),
% 24.10/3.55 inference(paramodulation,[],['512','2'])).
% 24.10/3.55 cnf('514', plain, (select(queue_53,seq) = earray_52),
% 24.10/3.55 inference(paramodulation,[],['286','9'])).
% 24.10/3.55 cnf('515', plain, (select(queue_55,seq) = earray_52),
% 24.10/3.55 inference(paramodulation,[then_simplify],['284','514','419'])).
% 24.10/3.55 cnf('516', plain, (earray_56 = select(q16,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp47'])).
% 24.10/3.55 cnf('517', plain, (earray_56 = select(queue_55,seq)),
% 24.10/3.55 inference(paramodulation,[],['293','516'])).
% 24.10/3.55 cnf('518', plain, (earray_56 = earray_52),
% 24.10/3.55 inference(simplify,[],['515','517'])).
% 24.10/3.55 cnf('519', plain, (select(queue_46,tail) = index_45),
% 24.10/3.55 inference(paramodulation,[],['259','9'])).
% 24.10/3.55 cnf('520', plain, (select(queue_49,tail) = index_45),
% 24.10/3.55 inference(paramodulation,[then_simplify],['493','519','157'])).
% 24.10/3.55 cnf('521', plain, (index_51 = select(q15,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp123'])).
% 24.10/3.55 cnf('522', plain, (index_51 = select(queue_49,tail)),
% 24.10/3.55 inference(paramodulation,[],['285','521'])).
% 24.10/3.55 cnf('523', plain, (index_51 = index_45),
% 24.10/3.55 inference(simplify,[],['520','522'])).
% 24.10/3.55 cnf('524', plain, (select(earray_56,X) = select(earray_50,X) | index_45 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['513','518','523'])).
% 24.10/3.55 cnf('525', plain, (s(s(s(s(s(X))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as5'])).
% 24.10/3.55 cnf('526', plain, (s(s(s(s(index_18)))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','525'])).
% 24.10/3.55 cnf('527', plain, (s(s(s(index_24))) != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['526','465','412'])).
% 24.10/3.55 cnf('528', plain, (s(s(index_33)) != index_12),
% 24.10/3.55 inference(paramodulation,[],['482','527'])).
% 24.10/3.55 cnf('529', plain, (index_45 = s(index_42)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp120'])).
% 24.10/3.55 cnf('530', plain, (index_45 = s(index_39)),
% 24.10/3.55 inference(paramodulation,[],['501','529'])).
% 24.10/3.55 cnf('531', plain, (index_45 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['528','508','530'])).
% 24.10/3.55 cnf('532', plain, (index_45 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','531'])).
% 24.10/3.55 cnf('533', plain, (select(earray_56,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['511','524','532'])).
% 24.10/3.55 cnf('534', plain, (earray_58 = store(earray_56,index_57,e16)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp48'])).
% 24.10/3.55 cnf('535', plain, (select(earray_58,X3) = select(earray_56,X3) | index_57 = X3),
% 24.10/3.55 inference(paramodulation,[],['534','2'])).
% 24.10/3.55 cnf('536', plain, (select(queue_59,seq) = earray_58),
% 24.10/3.55 inference(paramodulation,[],['294','9'])).
% 24.10/3.55 cnf('537', plain, (select(queue_61,seq) = earray_58),
% 24.10/3.55 inference(paramodulation,[then_simplify],['308','536','419'])).
% 24.10/3.55 cnf('538', plain, (earray_62 = select(q17,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp49'])).
% 24.10/3.55 cnf('539', plain, (earray_62 = select(queue_61,seq)),
% 24.10/3.55 inference(paramodulation,[],['302','538'])).
% 24.10/3.55 cnf('540', plain, (earray_62 = earray_58),
% 24.10/3.55 inference(simplify,[],['537','539'])).
% 24.10/3.55 cnf('541', plain, (select(queue_55,tail) = index_54),
% 24.10/3.55 inference(paramodulation,[],['283','9'])).
% 24.10/3.55 cnf('542', plain, (index_57 = select(q16,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp125'])).
% 24.10/3.55 cnf('543', plain, (index_57 = select(queue_55,tail)),
% 24.10/3.55 inference(paramodulation,[],['293','542'])).
% 24.10/3.55 cnf('544', plain, (index_57 = index_54),
% 24.10/3.55 inference(simplify,[],['541','543'])).
% 24.10/3.55 cnf('545', plain, (select(earray_62,X) = select(earray_56,X) | index_54 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['535','540','544'])).
% 24.10/3.55 cnf('546', plain, (s(s(s(s(s(s(X)))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as6'])).
% 24.10/3.55 cnf('547', plain, (s(s(s(s(s(index_18))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','546'])).
% 24.10/3.55 cnf('548', plain, (s(s(s(s(index_24)))) != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['547','465','412'])).
% 24.10/3.55 cnf('549', plain, (s(s(s(index_33))) != index_12),
% 24.10/3.55 inference(paramodulation,[],['482','548'])).
% 24.10/3.55 cnf('550', plain, (index_54 = s(index_51)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp124'])).
% 24.10/3.55 cnf('551', plain, (index_54 = s(index_45)),
% 24.10/3.55 inference(paramodulation,[],['523','550'])).
% 24.10/3.55 cnf('552', plain, (index_54 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['549','508','530','551'])).
% 24.10/3.55 cnf('553', plain, (index_54 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','552'])).
% 24.10/3.55 cnf('554', plain, (select(earray_62,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['533','545','553'])).
% 24.10/3.55 cnf('555', plain, (earray_64 = store(earray_62,index_63,e17)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp50'])).
% 24.10/3.55 cnf('556', plain, (select(earray_64,X3) = select(earray_62,X3) | index_63 = X3),
% 24.10/3.55 inference(paramodulation,[],['555','2'])).
% 24.10/3.55 cnf('557', plain, (select(queue_70,X) = select(queue_67,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['328','2'])).
% 24.10/3.55 cnf('558', plain, (select(queue_65,seq) = earray_64),
% 24.10/3.55 inference(paramodulation,[],['303','9'])).
% 24.10/3.55 cnf('559', plain, (select(queue_67,seq) = earray_64),
% 24.10/3.55 inference(paramodulation,[then_simplify],['558','299','419'])).
% 24.10/3.55 cnf('560', plain, (select(queue_70,seq) = earray_64),
% 24.10/3.55 inference(paramodulation,[then_simplify],['557','559','421'])).
% 24.10/3.55 cnf('561', plain, (earray_71 = select(q18,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp51'])).
% 24.10/3.55 cnf('562', plain, (earray_71 = select(queue_70,seq)),
% 24.10/3.55 inference(paramodulation,[],['324','561'])).
% 24.10/3.55 cnf('563', plain, (earray_71 = earray_64),
% 24.10/3.55 inference(simplify,[],['560','562'])).
% 24.10/3.55 cnf('564', plain, (select(queue_61,tail) = index_60),
% 24.10/3.55 inference(paramodulation,[],['307','9'])).
% 24.10/3.55 cnf('565', plain, (index_63 = select(q17,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp128'])).
% 24.10/3.55 cnf('566', plain, (index_63 = select(queue_61,tail)),
% 24.10/3.55 inference(paramodulation,[],['302','565'])).
% 24.10/3.55 cnf('567', plain, (index_63 = index_60),
% 24.10/3.55 inference(simplify,[],['564','566'])).
% 24.10/3.55 cnf('568', plain, (select(earray_71,X) = select(earray_62,X) | index_60 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['556','563','567'])).
% 24.10/3.55 cnf('569', plain, (s(s(s(s(s(s(s(X))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as7'])).
% 24.10/3.55 cnf('570', plain, (s(s(s(s(s(s(index_18)))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','569'])).
% 24.10/3.55 cnf('571', plain, (s(s(s(s(s(index_24))))) != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['570','465','412'])).
% 24.10/3.55 cnf('572', plain, (s(s(s(s(index_33)))) != index_12),
% 24.10/3.55 inference(paramodulation,[],['482','571'])).
% 24.10/3.55 cnf('573', plain, (index_60 = s(index_57)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp127'])).
% 24.10/3.55 cnf('574', plain, (index_60 = s(index_54)),
% 24.10/3.55 inference(paramodulation,[],['544','573'])).
% 24.10/3.55 cnf('575', plain, (index_60 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['572','508','530','551','574'])).
% 24.10/3.55 cnf('576', plain, (index_60 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','575'])).
% 24.10/3.55 cnf('577', plain, (select(earray_71,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['554','568','576'])).
% 24.10/3.55 cnf('578', plain, (select(queue_67,tail) = index_66),
% 24.10/3.55 inference(paramodulation,[],['298','9'])).
% 24.10/3.55 cnf('579', plain, (select(queue_70,tail) = index_66),
% 24.10/3.55 inference(paramodulation,[then_simplify],['557','578','157'])).
% 24.10/3.55 cnf('580', plain, (index_72 = select(q18,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp132'])).
% 24.10/3.55 cnf('581', plain, (index_72 = select(queue_70,tail)),
% 24.10/3.55 inference(paramodulation,[],['324','580'])).
% 24.10/3.55 cnf('582', plain, (index_72 = index_66),
% 24.10/3.55 inference(simplify,[],['579','581'])).
% 24.10/3.55 cnf('583', plain, (earray_73 = store(earray_71,index_72,e18)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp52'])).
% 24.10/3.55 cnf('584', plain, (earray_73 = store(earray_71,index_66,e18)),
% 24.10/3.55 inference(paramodulation,[],['582','583'])).
% 24.10/3.55 cnf('585', plain, (select(queue_74,seq) = earray_73),
% 24.10/3.55 inference(paramodulation,[],['325','9'])).
% 24.10/3.55 cnf('586', plain, (select(queue_76,seq) = earray_73),
% 24.10/3.55 inference(paramodulation,[then_simplify],['323','585','419'])).
% 24.10/3.55 cnf('587', plain, (earray_83 = select(q19,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp56'])).
% 24.10/3.55 cnf('588', plain, (earray_83 = select(queue_76,seq)),
% 24.10/3.55 inference(paramodulation,[],['332','587'])).
% 24.10/3.55 cnf('589', plain, (earray_83 = earray_73),
% 24.10/3.55 inference(simplify,[],['586','588'])).
% 24.10/3.55 cnf('590', plain, (earray_83 = store(earray_71,index_66,e18)),
% 24.10/3.55 inference(simplify,[],['584','589'])).
% 24.10/3.55 cnf('591', plain, (select(earray_83,X) = select(earray_71,X) | index_66 = X),
% 24.10/3.55 inference(paramodulation,[],['590','2'])).
% 24.10/3.55 cnf('592', plain, (s(s(s(s(s(s(s(s(X)))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as8'])).
% 24.10/3.55 cnf('593', plain, (s(s(s(s(s(s(s(index_18))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','592'])).
% 24.10/3.55 cnf('594', plain, (index_66 = s(index_63)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp129'])).
% 24.10/3.55 cnf('595', plain, (index_66 = s(index_60)),
% 24.10/3.55 inference(paramodulation,[],['567','594'])).
% 24.10/3.55 cnf('596', plain, (index_66 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['593','465','482','508','530','551','574','595','412'])).
% 24.10/3.55 cnf('597', plain, (index_66 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','596'])).
% 24.10/3.55 cnf('598', plain, (select(earray_83,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['577','591','597'])).
% 24.10/3.55 cnf('599', plain, (earray_85 = store(earray_83,index_84,e19)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp57'])).
% 24.10/3.55 cnf('600', plain, (select(earray_85,X3) = select(earray_83,X3) | index_84 = X3),
% 24.10/3.55 inference(paramodulation,[],['599','2'])).
% 24.10/3.55 cnf('601', plain, (select(queue_86,seq) = earray_85),
% 24.10/3.55 inference(paramodulation,[],['333','9'])).
% 24.10/3.55 cnf('602', plain, (select(queue_88,seq) = earray_85),
% 24.10/3.55 inference(paramodulation,[then_simplify],['347','601','419'])).
% 24.10/3.55 cnf('603', plain, (earray_89 = select(q20,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp58'])).
% 24.10/3.55 cnf('604', plain, (earray_89 = select(queue_88,seq)),
% 24.10/3.55 inference(paramodulation,[],['341','603'])).
% 24.10/3.55 cnf('605', plain, (earray_89 = earray_85),
% 24.10/3.55 inference(simplify,[],['602','604'])).
% 24.10/3.55 cnf('606', plain, (select(queue_76,tail) = index_75),
% 24.10/3.55 inference(paramodulation,[],['322','9'])).
% 24.10/3.55 cnf('607', plain, (index_84 = select(q19,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp136'])).
% 24.10/3.55 cnf('608', plain, (index_84 = select(queue_76,tail)),
% 24.10/3.55 inference(paramodulation,[],['332','607'])).
% 24.10/3.55 cnf('609', plain, (index_84 = index_75),
% 24.10/3.55 inference(simplify,[],['606','608'])).
% 24.10/3.55 cnf('610', plain, (select(earray_89,X) = select(earray_83,X) | index_75 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['600','605','609'])).
% 24.10/3.55 cnf('611', plain, (s(s(s(s(s(s(s(s(s(X))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as9'])).
% 24.10/3.55 cnf('612', plain, (s(s(s(s(s(s(s(s(index_18)))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','611'])).
% 24.10/3.55 cnf('613', plain, (index_75 = s(index_72)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp133'])).
% 24.10/3.55 cnf('614', plain, (index_75 = s(index_66)),
% 24.10/3.55 inference(paramodulation,[],['582','613'])).
% 24.10/3.55 cnf('615', plain, (index_75 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['612','465','482','508','530','551','574','595','614','412'])).
% 24.10/3.55 cnf('616', plain, (index_75 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','615'])).
% 24.10/3.55 cnf('617', plain, (select(earray_89,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['598','610','616'])).
% 24.10/3.55 cnf('618', plain, (select(queue_88,tail) = index_87),
% 24.10/3.55 inference(paramodulation,[],['346','9'])).
% 24.10/3.55 cnf('619', plain, (index_90 = select(q20,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp139'])).
% 24.10/3.55 cnf('620', plain, (index_90 = select(queue_88,tail)),
% 24.10/3.55 inference(paramodulation,[],['341','619'])).
% 24.10/3.55 cnf('621', plain, (index_90 = index_87),
% 24.10/3.55 inference(simplify,[],['618','620'])).
% 24.10/3.55 cnf('622', plain, (earray_91 = store(earray_89,index_90,e20)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp59'])).
% 24.10/3.55 cnf('623', plain, (earray_91 = store(earray_89,index_87,e20)),
% 24.10/3.55 inference(paramodulation,[],['621','622'])).
% 24.10/3.55 cnf('624', plain, (select(earray_91,X) = select(earray_89,X) | index_87 = X),
% 24.10/3.55 inference(paramodulation,[],['623','2'])).
% 24.10/3.55 cnf('625', plain, (s(s(s(s(s(s(s(s(s(s(X)))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as10'])).
% 24.10/3.55 cnf('626', plain, (s(s(s(s(s(s(s(s(s(index_18))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','625'])).
% 24.10/3.55 cnf('627', plain, (index_87 = s(index_84)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp137'])).
% 24.10/3.55 cnf('628', plain, (index_87 = s(index_75)),
% 24.10/3.55 inference(paramodulation,[],['609','627'])).
% 24.10/3.55 cnf('629', plain, (index_87 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['626','465','482','508','530','551','574','595','614','628','412'])).
% 24.10/3.55 cnf('630', plain, (index_87 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','629'])).
% 24.10/3.55 cnf('631', plain, (select(earray_91,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['617','624','630'])).
% 24.10/3.55 cnf('632', plain, (earray_100 = store(earray_98,index_99,e21)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp1'])).
% 24.10/3.55 cnf('633', plain, (select(earray_100,X3) = select(earray_98,X3) | index_99 = X3),
% 24.10/3.55 inference(paramodulation,[],['632','2'])).
% 24.10/3.55 cnf('634', plain, (select(queue_101,seq) = earray_100),
% 24.10/3.55 inference(paramodulation,[],['63','9'])).
% 24.10/3.55 cnf('635', plain, (select(queue_103,seq) = earray_100),
% 24.10/3.55 inference(paramodulation,[then_simplify],['59','634','419'])).
% 24.10/3.55 cnf('636', plain, (earray_104 = select(q22,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp2'])).
% 24.10/3.55 cnf('637', plain, (earray_104 = select(queue_103,seq)),
% 24.10/3.55 inference(paramodulation,[],['68','636'])).
% 24.10/3.55 cnf('638', plain, (earray_104 = earray_100),
% 24.10/3.55 inference(simplify,[],['635','637'])).
% 24.10/3.55 cnf('639', plain, (earray_98 = select(q21,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp60'])).
% 24.10/3.55 cnf('640', plain, (earray_98 = select(queue_97,seq)),
% 24.10/3.55 inference(paramodulation,[],['62','639'])).
% 24.10/3.55 cnf('641', plain, (select(queue_97,X) = select(queue_94,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['60','2'])).
% 24.10/3.55 cnf('642', plain, (earray_98 = select(queue_94,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['640','641','421'])).
% 24.10/3.55 cnf('643', plain, (earray_98 = select(queue_92,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['338','642','419'])).
% 24.10/3.55 cnf('644', plain, (select(queue_92,seq) = earray_91),
% 24.10/3.55 inference(paramodulation,[],['342','9'])).
% 24.10/3.55 cnf('645', plain, (earray_98 = earray_91),
% 24.10/3.55 inference(simplify,[],['643','644'])).
% 24.10/3.55 cnf('646', plain, (select(queue_94,tail) = index_93),
% 24.10/3.55 inference(paramodulation,[],['337','9'])).
% 24.10/3.55 cnf('647', plain, (select(queue_97,tail) = index_93),
% 24.10/3.55 inference(paramodulation,[then_simplify],['641','646','157'])).
% 24.10/3.55 cnf('648', plain, (index_99 = select(q21,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp143'])).
% 24.10/3.55 cnf('649', plain, (index_99 = select(queue_97,tail)),
% 24.10/3.55 inference(paramodulation,[],['62','648'])).
% 24.10/3.55 cnf('650', plain, (index_99 = index_93),
% 24.10/3.55 inference(simplify,[],['647','649'])).
% 24.10/3.55 cnf('651', plain, (select(earray_104,X) = select(earray_91,X) | index_93 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['633','638','645','650'])).
% 24.10/3.55 cnf('652', plain, (s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as11'])).
% 24.10/3.55 cnf('653', plain, (s(s(s(s(s(s(s(s(s(s(index_18)))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','652'])).
% 24.10/3.55 cnf('654', plain, (index_93 = s(index_90)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp140'])).
% 24.10/3.55 cnf('655', plain, (index_93 = s(index_87)),
% 24.10/3.55 inference(paramodulation,[],['621','654'])).
% 24.10/3.55 cnf('656', plain, (index_93 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['653','465','482','508','530','551','574','595','614','628','655','412'])).
% 24.10/3.55 cnf('657', plain, (index_93 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','656'])).
% 24.10/3.55 cnf('658', plain, (select(earray_104,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['631','651','657'])).
% 24.10/3.55 cnf('659', plain, (earray_106 = store(earray_104,index_105,e22)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp3'])).
% 24.10/3.55 cnf('660', plain, (select(earray_106,X3) = select(earray_104,X3) | index_105 = X3),
% 24.10/3.55 inference(paramodulation,[],['659','2'])).
% 24.10/3.55 cnf('661', plain, (select(queue_107,seq) = earray_106),
% 24.10/3.55 inference(paramodulation,[],['69','9'])).
% 24.10/3.55 cnf('662', plain, (select(queue_109,seq) = earray_106),
% 24.10/3.55 inference(paramodulation,[then_simplify],['56','661','419'])).
% 24.10/3.55 cnf('663', plain, (earray_110 = select(q23,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp4'])).
% 24.10/3.55 cnf('664', plain, (earray_110 = select(queue_109,seq)),
% 24.10/3.55 inference(paramodulation,[],['50','663'])).
% 24.10/3.55 cnf('665', plain, (earray_110 = earray_106),
% 24.10/3.55 inference(simplify,[],['662','664'])).
% 24.10/3.55 cnf('666', plain, (select(queue_103,tail) = index_102),
% 24.10/3.55 inference(paramodulation,[],['58','9'])).
% 24.10/3.55 cnf('667', plain, (index_105 = select(q22,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp64'])).
% 24.10/3.55 cnf('668', plain, (index_105 = select(queue_103,tail)),
% 24.10/3.55 inference(paramodulation,[],['68','667'])).
% 24.10/3.55 cnf('669', plain, (index_105 = index_102),
% 24.10/3.55 inference(simplify,[],['666','668'])).
% 24.10/3.55 cnf('670', plain, (select(earray_110,X) = select(earray_104,X) | index_102 = X),
% 24.10/3.55 inference(simplify,[then_simplify],['660','665','669'])).
% 24.10/3.55 cnf('671', plain, (s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as12'])).
% 24.10/3.55 cnf('672', plain, (s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','671'])).
% 24.10/3.55 cnf('673', plain, (index_102 = s(index_99)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp63'])).
% 24.10/3.55 cnf('674', plain, (index_102 = s(index_93)),
% 24.10/3.55 inference(paramodulation,[],['650','673'])).
% 24.10/3.55 cnf('675', plain, (index_102 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['672','465','482','508','530','551','574','595','614','628','655','674','412'])).
% 24.10/3.55 cnf('676', plain, (index_102 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','675'])).
% 24.10/3.55 cnf('677', plain, (select(earray_110,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['658','670','676'])).
% 24.10/3.55 cnf('678', plain, (select(queue_118,X) = select(queue_115,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['36','2'])).
% 24.10/3.55 cnf('679', plain, (select(queue_113,seq) = earray_112),
% 24.10/3.55 inference(paramodulation,[],['51','9'])).
% 24.10/3.55 cnf('680', plain, (select(queue_115,seq) = earray_112),
% 24.10/3.55 inference(paramodulation,[then_simplify],['679','47','419'])).
% 24.10/3.55 cnf('681', plain, (select(queue_118,seq) = earray_112),
% 24.10/3.55 inference(paramodulation,[then_simplify],['678','680','421'])).
% 24.10/3.55 cnf('682', plain, (earray_119 = select(q24,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp6'])).
% 24.10/3.55 cnf('683', plain, (earray_119 = select(queue_118,seq)),
% 24.10/3.55 inference(paramodulation,[],['32','682'])).
% 24.10/3.55 cnf('684', plain, (earray_119 = earray_112),
% 24.10/3.55 inference(simplify,[],['681','683'])).
% 24.10/3.55 cnf('685', plain, (select(queue_109,tail) = index_108),
% 24.10/3.55 inference(paramodulation,[],['55','9'])).
% 24.10/3.55 cnf('686', plain, (index_111 = select(q23,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp66'])).
% 24.10/3.55 cnf('687', plain, (index_111 = select(queue_109,tail)),
% 24.10/3.55 inference(paramodulation,[],['50','686'])).
% 24.10/3.55 cnf('688', plain, (index_111 = index_108),
% 24.10/3.55 inference(simplify,[],['685','687'])).
% 24.10/3.55 cnf('689', plain, (earray_112 = store(earray_110,index_111,e23)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp5'])).
% 24.10/3.55 cnf('690', plain, (earray_112 = store(earray_110,index_108,e23)),
% 24.10/3.55 inference(paramodulation,[],['688','689'])).
% 24.10/3.55 cnf('691', plain, (select(earray_112,X) = select(earray_110,X) | index_108 = X),
% 24.10/3.55 inference(paramodulation,[],['690','2'])).
% 24.10/3.55 cnf('692', plain, (select(earray_119,X) = select(earray_110,X) | index_108 = X),
% 24.10/3.55 inference(paramodulation,[],['684','691'])).
% 24.10/3.55 cnf('693', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as13'])).
% 24.10/3.55 cnf('694', plain, (s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','693'])).
% 24.10/3.55 cnf('695', plain, (index_108 = s(index_105)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp65'])).
% 24.10/3.55 cnf('696', plain, (index_108 = s(index_102)),
% 24.10/3.55 inference(paramodulation,[],['669','695'])).
% 24.10/3.55 cnf('697', plain, (index_108 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['694','465','482','508','530','551','574','595','614','628','655','674','696','412'])).
% 24.10/3.55 cnf('698', plain, (index_108 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','697'])).
% 24.10/3.55 cnf('699', plain, (select(earray_119,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['677','692','698'])).
% 24.10/3.55 cnf('700', plain, (select(queue_122,seq) = earray_121),
% 24.10/3.55 inference(paramodulation,[],['33','9'])).
% 24.10/3.55 cnf('701', plain, (select(queue_124,seq) = earray_121),
% 24.10/3.55 inference(paramodulation,[then_simplify],['31','700','419'])).
% 24.10/3.55 cnf('702', plain, (earray_125 = select(q25,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp8'])).
% 24.10/3.55 cnf('703', plain, (earray_125 = select(queue_124,seq)),
% 24.10/3.55 inference(paramodulation,[],['40','702'])).
% 24.10/3.55 cnf('704', plain, (earray_125 = earray_121),
% 24.10/3.55 inference(simplify,[],['701','703'])).
% 24.10/3.55 cnf('705', plain, (earray_121 = store(earray_119,index_120,e24)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp7'])).
% 24.10/3.55 cnf('706', plain, (select(earray_121,X) = select(earray_119,X) | index_120 = X),
% 24.10/3.55 inference(paramodulation,[],['705','2'])).
% 24.10/3.55 cnf('707', plain, (select(earray_125,X3) = select(earray_119,X3) | index_120 = X3),
% 24.10/3.55 inference(paramodulation,[],['704','706'])).
% 24.10/3.55 cnf('708', plain, (select(queue_115,tail) = index_114),
% 24.10/3.55 inference(paramodulation,[],['46','9'])).
% 24.10/3.55 cnf('709', plain, (select(queue_118,tail) = index_114),
% 24.10/3.55 inference(paramodulation,[then_simplify],['678','708','157'])).
% 24.10/3.55 cnf('710', plain, (index_120 = select(q24,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp71'])).
% 24.10/3.55 cnf('711', plain, (index_120 = select(queue_118,tail)),
% 24.10/3.55 inference(paramodulation,[],['32','710'])).
% 24.10/3.55 cnf('712', plain, (index_120 = index_114),
% 24.10/3.55 inference(simplify,[],['709','711'])).
% 24.10/3.55 cnf('713', plain, (select(earray_125,X) = select(earray_119,X) | index_114 = X),
% 24.10/3.55 inference(simplify,[],['707','712'])).
% 24.10/3.55 cnf('714', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as14'])).
% 24.10/3.55 cnf('715', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','714'])).
% 24.10/3.55 cnf('716', plain, (index_114 = s(index_111)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp67'])).
% 24.10/3.55 cnf('717', plain, (index_114 = s(index_108)),
% 24.10/3.55 inference(paramodulation,[],['688','716'])).
% 24.10/3.55 cnf('718', plain, (index_114 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['715','465','482','508','530','551','574','595','614','628','655','674','696','717','412'])).
% 24.10/3.55 cnf('719', plain, (index_114 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','718'])).
% 24.10/3.55 cnf('720', plain, (select(earray_125,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['699','713','719'])).
% 24.10/3.55 cnf('721', plain, (select(queue_128,seq) = earray_127),
% 24.10/3.55 inference(paramodulation,[],['41','9'])).
% 24.10/3.55 cnf('722', plain, (select(queue_130,seq) = earray_127),
% 24.10/3.55 inference(paramodulation,[then_simplify],['28','721','419'])).
% 24.10/3.55 cnf('723', plain, (earray_131 = select(q26,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp10'])).
% 24.10/3.55 cnf('724', plain, (earray_131 = select(queue_130,seq)),
% 24.10/3.55 inference(paramodulation,[],['22','723'])).
% 24.10/3.55 cnf('725', plain, (earray_131 = earray_127),
% 24.10/3.55 inference(simplify,[],['722','724'])).
% 24.10/3.55 cnf('726', plain, (select(queue_124,tail) = index_123),
% 24.10/3.55 inference(paramodulation,[],['30','9'])).
% 24.10/3.55 cnf('727', plain, (index_126 = select(q25,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp73'])).
% 24.10/3.55 cnf('728', plain, (index_126 = select(queue_124,tail)),
% 24.10/3.55 inference(paramodulation,[],['40','727'])).
% 24.10/3.55 cnf('729', plain, (index_126 = index_123),
% 24.10/3.55 inference(simplify,[],['726','728'])).
% 24.10/3.55 cnf('730', plain, (earray_127 = store(earray_125,index_126,e25)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp9'])).
% 24.10/3.55 cnf('731', plain, (earray_127 = store(earray_125,index_123,e25)),
% 24.10/3.55 inference(paramodulation,[],['729','730'])).
% 24.10/3.55 cnf('732', plain, (select(earray_127,X) = select(earray_125,X) | index_123 = X),
% 24.10/3.55 inference(paramodulation,[],['731','2'])).
% 24.10/3.55 cnf('733', plain, (select(earray_131,X) = select(earray_125,X) | index_123 = X),
% 24.10/3.55 inference(paramodulation,[],['725','732'])).
% 24.10/3.55 cnf('734', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as15'])).
% 24.10/3.55 cnf('735', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','734'])).
% 24.10/3.55 cnf('736', plain, (index_123 = s(index_120)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp72'])).
% 24.10/3.55 cnf('737', plain, (index_123 = s(index_114)),
% 24.10/3.55 inference(paramodulation,[],['712','736'])).
% 24.10/3.55 cnf('738', plain, (index_123 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['735','465','482','508','530','551','574','595','614','628','655','674','696','717','737','412'])).
% 24.10/3.55 cnf('739', plain, (index_123 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','738'])).
% 24.10/3.55 cnf('740', plain, (select(earray_131,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['720','733','739'])).
% 24.10/3.55 cnf('741', plain, (earray_140 = select(q27,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp13'])).
% 24.10/3.55 cnf('742', plain, (earray_140 = select(queue_139,seq)),
% 24.10/3.55 inference(paramodulation,[],['4','741'])).
% 24.10/3.55 cnf('743', plain, (select(queue_139,X) = select(queue_136,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['8','2'])).
% 24.10/3.55 cnf('744', plain, (earray_140 = select(queue_136,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['742','743','421'])).
% 24.10/3.55 cnf('745', plain, (earray_140 = select(queue_134,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['19','744','419'])).
% 24.10/3.55 cnf('746', plain, (select(queue_134,seq) = earray_133),
% 24.10/3.55 inference(paramodulation,[],['23','9'])).
% 24.10/3.55 cnf('747', plain, (earray_140 = earray_133),
% 24.10/3.55 inference(simplify,[],['745','746'])).
% 24.10/3.55 cnf('748', plain, (select(queue_130,tail) = index_129),
% 24.10/3.55 inference(paramodulation,[],['27','9'])).
% 24.10/3.55 cnf('749', plain, (index_132 = select(q26,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp75'])).
% 24.10/3.55 cnf('750', plain, (index_132 = select(queue_130,tail)),
% 24.10/3.55 inference(paramodulation,[],['22','749'])).
% 24.10/3.55 cnf('751', plain, (index_132 = index_129),
% 24.10/3.55 inference(simplify,[],['748','750'])).
% 24.10/3.55 cnf('752', plain, (earray_133 = store(earray_131,index_132,e26)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp11'])).
% 24.10/3.55 cnf('753', plain, (earray_133 = store(earray_131,index_129,e26)),
% 24.10/3.55 inference(paramodulation,[],['751','752'])).
% 24.10/3.55 cnf('754', plain, (select(earray_133,X) = select(earray_131,X) | index_129 = X),
% 24.10/3.55 inference(paramodulation,[],['753','2'])).
% 24.10/3.55 cnf('755', plain, (select(earray_140,X) = select(earray_131,X) | index_129 = X),
% 24.10/3.55 inference(paramodulation,[],['747','754'])).
% 24.10/3.55 cnf('756', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as16'])).
% 24.10/3.55 cnf('757', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','756'])).
% 24.10/3.55 cnf('758', plain, (index_129 = s(index_126)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp74'])).
% 24.10/3.55 cnf('759', plain, (index_129 = s(index_123)),
% 24.10/3.55 inference(paramodulation,[],['729','758'])).
% 24.10/3.55 cnf('760', plain, (index_129 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['757','465','482','508','530','551','574','595','614','628','655','674','696','717','737','759','412'])).
% 24.10/3.55 cnf('761', plain, (index_129 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','760'])).
% 24.10/3.55 cnf('762', plain, (select(earray_140,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['740','755','761'])).
% 24.10/3.55 cnf('763', plain, (select(queue_136,tail) = index_135),
% 24.10/3.55 inference(paramodulation,[],['18','9'])).
% 24.10/3.55 cnf('764', plain, (select(queue_139,tail) = index_135),
% 24.10/3.55 inference(paramodulation,[then_simplify],['743','763','157'])).
% 24.10/3.55 cnf('765', plain, (index_141 = select(q27,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp79'])).
% 24.10/3.55 cnf('766', plain, (index_141 = select(queue_139,tail)),
% 24.10/3.55 inference(paramodulation,[],['4','765'])).
% 24.10/3.55 cnf('767', plain, (index_141 = index_135),
% 24.10/3.55 inference(simplify,[],['764','766'])).
% 24.10/3.55 cnf('768', plain, (earray_142 = store(earray_140,index_141,e27)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp14'])).
% 24.10/3.55 cnf('769', plain, (earray_142 = store(earray_140,index_135,e27)),
% 24.10/3.55 inference(paramodulation,[],['767','768'])).
% 24.10/3.55 cnf('770', plain, (select(earray_142,X3) = select(earray_140,X3) | index_135 = X3),
% 24.10/3.55 inference(paramodulation,[],['769','2'])).
% 24.10/3.55 cnf('771', plain, (select(queue_143,seq) = earray_142),
% 24.10/3.55 inference(paramodulation,[],['5','9'])).
% 24.10/3.55 cnf('772', plain, (select(queue_145,seq) = earray_142),
% 24.10/3.55 inference(paramodulation,[then_simplify],['3','771','419'])).
% 24.10/3.55 cnf('773', plain, (earray_146 = select(q28,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp15'])).
% 24.10/3.55 cnf('774', plain, (earray_146 = select(queue_145,seq)),
% 24.10/3.55 inference(paramodulation,[],['13','773'])).
% 24.10/3.55 cnf('775', plain, (earray_146 = earray_142),
% 24.10/3.55 inference(simplify,[],['772','774'])).
% 24.10/3.55 cnf('776', plain, (select(earray_146,X) = select(earray_140,X) | index_135 = X),
% 24.10/3.55 inference(simplify,[],['770','775'])).
% 24.10/3.55 cnf('777', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as17'])).
% 24.10/3.55 cnf('778', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','777'])).
% 24.10/3.55 cnf('779', plain, (index_135 = s(index_132)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp76'])).
% 24.10/3.55 cnf('780', plain, (index_135 = s(index_129)),
% 24.10/3.55 inference(paramodulation,[],['751','779'])).
% 24.10/3.55 cnf('781', plain, (index_135 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['778','465','482','508','530','551','574','595','614','628','655','674','696','717','737','759','780','412'])).
% 24.10/3.55 cnf('782', plain, (index_135 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','781'])).
% 24.10/3.55 cnf('783', plain, (select(earray_146,index_168) = e10),
% 24.10/3.55 inference(paramodulation,[then_simplify],['762','776','782'])).
% 24.10/3.55 cnf('784', plain, (queue_169 = store(queue_166,head,index_168)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp170'])).
% 24.10/3.55 cnf('785', plain, (select(queue_169,head) = index_168),
% 24.10/3.55 inference(paramodulation,[],['784','9'])).
% 24.10/3.55 cnf('786', plain, (q30 = queue_169),
% 24.10/3.55 inference(cnf_transformation,[],['hyp239'])).
% 24.10/3.55 cnf('787', plain, (index_213 = select(q30,head)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp110'])).
% 24.10/3.55 cnf('788', plain, (index_213 = select(queue_169,head)),
% 24.10/3.55 inference(paramodulation,[],['786','787'])).
% 24.10/3.55 cnf('789', plain, (index_213 = index_168),
% 24.10/3.55 inference(simplify,[],['785','788'])).
% 24.10/3.55 cnf('790', plain, (elem_214 = select(earray_212,index_213)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp61'])).
% 24.10/3.55 cnf('791', plain, (elem_214 = select(earray_212,index_168)),
% 24.10/3.55 inference(paramodulation,[],['789','790'])).
% 24.10/3.55 cnf('792', plain, (earray_212 = select(q30,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp36'])).
% 24.10/3.55 cnf('793', plain, (earray_212 = select(queue_169,seq)),
% 24.10/3.55 inference(paramodulation,[],['786','792'])).
% 24.10/3.55 cnf('794', plain, (select(queue_169,X) = select(queue_166,X) | head = X),
% 24.10/3.55 inference(paramodulation,[],['784','2'])).
% 24.10/3.55 cnf('795', plain, (earray_212 = select(queue_166,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['793','794','421'])).
% 24.10/3.55 cnf('796', plain, (earray_212 = select(queue_164,seq)),
% 24.10/3.55 inference(paramodulation,[then_simplify],['386','795','419'])).
% 24.10/3.55 cnf('797', plain, (select(queue_164,seq) = earray_163),
% 24.10/3.55 inference(paramodulation,[],['390','9'])).
% 24.10/3.55 cnf('798', plain, (earray_212 = earray_163),
% 24.10/3.55 inference(simplify,[],['796','797'])).
% 24.10/3.55 cnf('799', plain, (select(queue_151,tail) = index_150),
% 24.10/3.55 inference(paramodulation,[],['394','9'])).
% 24.10/3.55 cnf('800', plain, (index_162 = select(q29,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp88'])).
% 24.10/3.55 cnf('801', plain, (index_162 = select(queue_151,tail)),
% 24.10/3.55 inference(paramodulation,[],['389','800'])).
% 24.10/3.55 cnf('802', plain, (index_162 = index_150),
% 24.10/3.55 inference(simplify,[],['799','801'])).
% 24.10/3.55 cnf('803', plain, (earray_163 = store(earray_161,index_162,e29)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp21'])).
% 24.10/3.55 cnf('804', plain, (earray_163 = store(earray_161,index_150,e29)),
% 24.10/3.55 inference(paramodulation,[],['802','803'])).
% 24.10/3.55 cnf('805', plain, (select(earray_163,X) = select(earray_161,X) | index_150 = X),
% 24.10/3.55 inference(paramodulation,[],['804','2'])).
% 24.10/3.55 cnf('806', plain, (select(earray_212,X) = select(earray_161,X) | index_150 = X),
% 24.10/3.55 inference(paramodulation,[],['798','805'])).
% 24.10/3.55 cnf('807', plain, (elem_214 = select(earray_161,index_168) | index_150 = index_168),
% 24.10/3.55 inference(paramodulation,[],['791','806'])).
% 24.10/3.55 cnf('808', plain, (select(queue_149,seq) = earray_148),
% 24.10/3.55 inference(paramodulation,[],['14','9'])).
% 24.10/3.55 cnf('809', plain, (select(queue_151,seq) = earray_148),
% 24.10/3.55 inference(paramodulation,[then_simplify],['395','808','419'])).
% 24.10/3.55 cnf('810', plain, (earray_161 = select(q29,seq)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp20'])).
% 24.10/3.55 cnf('811', plain, (earray_161 = select(queue_151,seq)),
% 24.10/3.55 inference(paramodulation,[],['389','810'])).
% 24.10/3.55 cnf('812', plain, (earray_161 = earray_148),
% 24.10/3.55 inference(simplify,[],['809','811'])).
% 24.10/3.55 cnf('813', plain, (select(queue_145,tail) = index_144),
% 24.10/3.55 inference(paramodulation,[],['1','9'])).
% 24.10/3.55 cnf('814', plain, (index_147 = select(q28,tail)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp81'])).
% 24.10/3.55 cnf('815', plain, (index_147 = select(queue_145,tail)),
% 24.10/3.55 inference(paramodulation,[],['13','814'])).
% 24.10/3.55 cnf('816', plain, (index_147 = index_144),
% 24.10/3.55 inference(simplify,[],['813','815'])).
% 24.10/3.55 cnf('817', plain, (earray_148 = store(earray_146,index_147,e28)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp16'])).
% 24.10/3.55 cnf('818', plain, (earray_148 = store(earray_146,index_144,e28)),
% 24.10/3.55 inference(paramodulation,[],['816','817'])).
% 24.10/3.55 cnf('819', plain, (select(earray_148,X) = select(earray_146,X) | index_144 = X),
% 24.10/3.55 inference(paramodulation,[],['818','2'])).
% 24.10/3.55 cnf('820', plain, (select(earray_161,X) = select(earray_146,X) | index_144 = X),
% 24.10/3.55 inference(paramodulation,[],['812','819'])).
% 24.10/3.55 cnf('821', plain, (elem_214 = select(earray_146,index_168) | index_150 = index_168 | index_144 = index_168),
% 24.10/3.55 inference(paramodulation,[],['807','820'])).
% 24.10/3.55 cnf('822', plain, (elem_214 != e10),
% 24.10/3.55 inference(cnf_transformation,[],['goal'])).
% 24.10/3.55 cnf('823', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as19'])).
% 24.10/3.55 cnf('824', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','823'])).
% 24.10/3.55 cnf('825', plain, (index_144 = s(index_141)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp80'])).
% 24.10/3.55 cnf('826', plain, (index_144 = s(index_135)),
% 24.10/3.55 inference(paramodulation,[],['767','825'])).
% 24.10/3.55 cnf('827', plain, (index_150 = s(index_147)),
% 24.10/3.55 inference(cnf_transformation,[],['hyp83'])).
% 24.10/3.55 cnf('828', plain, (index_150 = s(index_144)),
% 24.10/3.55 inference(paramodulation,[],['816','827'])).
% 24.10/3.55 cnf('829', plain, (index_150 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['824','465','482','508','530','551','574','595','614','628','655','674','696','717','737','759','780','826','828','412'])).
% 24.10/3.55 cnf('830', plain, (index_150 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','829'])).
% 24.10/3.55 cnf('831', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X),
% 24.10/3.55 inference(cnf_transformation,[],['as18'])).
% 24.10/3.55 cnf('832', plain, (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))))) != index_15),
% 24.10/3.55 inference(paramodulation,[],['442','831'])).
% 24.10/3.55 cnf('833', plain, (index_144 != index_12),
% 24.10/3.55 inference(simplify,[then_simplify],['832','465','482','508','530','551','574','595','614','628','655','674','696','717','737','759','780','826','412'])).
% 24.10/3.55 cnf('834', plain, (index_144 != index_168),
% 24.10/3.55 inference(paramodulation,[],['416','833'])).
% 24.10/3.55 cnf('835', plain, ($false),
% 24.10/3.55 inference(paramodulation,[then_simplify],['783','821','822','830','834'])).
% 24.10/3.55
% 24.10/3.55 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.10/3.55
% 24.10/3.55 run 116 fork 3 statistics:
% 24.10/3.55 ----------------------------------
% 24.10/3.55 this run seconds: 0.582678
% 24.10/3.55 total seconds: 2.609174
% 24.10/3.55 stat_given_used: 3120
% 24.10/3.55 stat_given_used_at_endgame: 0
% 24.10/3.55 stat_given_candidates: 7010
% 24.10/3.55 stat_given_candidates_at_endgame: 0
% 24.10/3.55 stat_given_candidates_h: 0
% 24.10/3.55 stat_binres_derived_cl: 0
% 24.10/3.55 stat_binres_derived_cl_h: 0
% 24.10/3.55 stat_factor_derived_cl: 0
% 24.10/3.55 stat_para_derived_cl: 22103
% 24.10/3.55 stat_tautologies_discarded: 0
% 24.10/3.55 stat_forward_subsumed: 3954
% 24.10/3.55 stat_derived_cut: 976
% 24.10/3.55 stat_derived_rewritten: 1914
% 24.10/3.55 stat_weight_discarded_building: 0
% 24.10/3.55 stat_weight_discarded_cl: 225
% 24.10/3.55 stat_internlimit_discarded_cl: 0
% 24.10/3.55 stat_simplified: 1915 simplified 0 derived 0 given
% 24.10/3.55 stat_kept_cl: 12529
% 24.10/3.55 stat_built_cl: 20909
% 24.10/3.55 stat_hyperres_partial_cl: 0
% 24.10/3.55 stat_made_rewriters: 922
% 24.10/3.55 stat_backward_subsumed: 0
% 24.10/3.55 stat_propagated_subsumed: 0
% 24.10/3.55 stat_clsubs_attempted: 180121
% 24.10/3.55 stat_clsubs_fact_groundunit_found: 0
% 24.10/3.55 stat_clsubs_rule_groundunit_found: 517
% 24.10/3.55 stat_clsubs_top_meta_attempted: 1829787
% 24.10/3.55 stat_clsubs_top_meta_failed: 1649666
% 24.10/3.55 stat_clsubs_top_meta_nonpref_attempted: 1829787
% 24.10/3.55 stat_clsubs_top_meta_nonpref_succeeded: 472708
% 24.10/3.55 stat_clsubs_top_meta_pref_attempted: 472708
% 24.10/3.55 stat_clsubs_top_meta_pref1_succeeded: 472398
% 24.10/3.55 stat_clsubs_top_meta_pref2_succeeded: 203373
% 24.10/3.55 stat_clsubs_top_meta_pref3_succeeded: 180121
% 24.10/3.55 stat_clsubs_top_meta_pref_succeeded: 180121
% 24.10/3.55 stat_clsubs_meta_attempted: 355661
% 24.10/3.55 stat_clsubs_meta_failed: 342781
% 24.10/3.55 stat_clsubs_predsymbs_attempted: 0
% 24.10/3.55 stat_clsubs_unit_attempted: 5765
% 24.10/3.55 stat_clsubs_full_attempted: 174356
% 24.10/3.55 stat_forwardsubs_attempted: 16709
% 24.10/3.55 stat_lit_hash_added: 13120
% 24.10/3.55 stat_lit_hash_computed: 63478
% 24.10/3.55 stat_lit_hash_match_found: 6221
% 24.10/3.55 stat_lit_hash_match_miss: 78822
% 24.10/3.55 stat_lit_hash_cut_ok: 1261
% 24.10/3.55 stat_lit_strong_cut_ok: 141
% 24.10/3.55 stat_lit_hash_subsume_ok: 3954
% 24.10/3.55 clqueue els 10000000 used 1
% 24.10/3.55 clactive els 10000000 used 3121
% 24.10/3.55 clactivesubsume els 10000000 used 5809
% 24.10/3.55 queue_termbuf els 200000000 used 1212849
% 24.10/3.55 hyper_termbuf els 100000000 used 1
% 24.10/3.55 active_termbuf els 100000000 used 94258
% 24.10/3.55 varstack els 5000 last used 1
% 24.10/3.55 given_termbuf els 10000000 last used 1
% 24.10/3.55 simplified_termbuf els 10000000 last used 1
% 24.10/3.55 derived_termbuf els 10000000 last used 43
% 24.10/3.55 wr_mallocs: 59071
% 24.10/3.55 wr_callocs: 21
% 24.10/3.55 wr_reallocs: 1459
% 24.10/3.55 wr_frees: 4
% 24.10/3.55 wr_malloc_bytes: 4164644964
% 24.10/3.55 wr_calloc_bytes: 112065536
% 24.10/3.55 wr_realloc_bytes: 476432
% 24.10/3.55 wr_realloc_freebytes: 0
% 24.10/3.55 ----------------------------------
%------------------------------------------------------------------------------