%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : NLP009+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Aug 31 09:52:07 EDT 2023
% Result : Theorem 61.64s 8.31s
% Output : CNFRefutation 61.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP009+1 : TPTP v8.1.2. Released v2.4.0.
% 0.00/0.12 % Command : gkc %s
% 0.12/0.33 % Computer : n020.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Aug 24 11:31:45 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.18/0.40
% 0.18/0.40 input clause set summed statistics:
% 0.18/0.40 ----------------------------------
% 0.18/0.40 in_clause_count: 115
% 0.18/0.40 in_rule_clause_count: 115
% 0.18/0.40 in_fact_clause_count: 0
% 0.18/0.40 in_answer_clause_count: 0
% 0.18/0.40 in_ground_clause_count: 0
% 0.18/0.40 in_unit_clause_count: 0
% 0.18/0.40 in_horn_clause_count: 58
% 0.18/0.40 in_pos_clause_count: 1
% 0.18/0.40 in_neg_clause_count: 2
% 0.18/0.40 in_poseq_clause_count: 62
% 0.18/0.40 in_negeq_clause_count: 60
% 0.18/0.40 in_unitposeq_clause_count: 0
% 0.18/0.40 in_chain_clause_count: 0
% 0.18/0.40 in_min_length: 2
% 0.18/0.40 in_max_length: 30
% 0.18/0.40 in_min_depth: 1
% 0.18/0.40 in_max_depth: 1
% 0.18/0.40 in_min_size: 12
% 0.18/0.40 in_max_size: 77
% 0.18/0.40 in_min_vars: 9
% 0.18/0.40 in_max_vars: 18
% 0.18/0.40 in_extaxiom_count: 0
% 0.18/0.40 in_axiom_count: 0
% 0.18/0.40 in_assumption_count: 0
% 0.18/0.40 in_goal_count: 115
% 0.18/0.40 in_neg_goal_count: 2
% 0.18/0.40 in_pos_goal_count: 1
% 0.18/0.40 in_posunit_goal_count: 0
% 0.18/0.40
% 0.18/0.40 auto guide:
% 0.18/0.40 -----------
% 0.18/0.40 {
% 0.18/0.40 "print":1,
% 0.18/0.40 "print_level": 15,
% 0.18/0.40 "max_size": 0,
% 0.18/0.40 "max_depth": 0,
% 0.18/0.40 "max_length": 0,
% 0.18/0.40 "max_dseconds": 0,
% 0.18/0.40 "runs":[
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.18/0.40 {"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.18/0.40 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.18/0.40 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":1},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":1},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.18/0.40 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":1},
% 0.18/0.40 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.18/0.40 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.18/0.40 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":1},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":1},
% 0.18/0.40 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.18/0.40
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.18/0.40 {"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.18/0.40 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.18/0.40 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":10},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":10},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.18/0.40 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":10},
% 0.18/0.40 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.18/0.40 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.18/0.40 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":10},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":10},
% 0.18/0.40 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.18/0.40
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "sine":3, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_unordered_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"], "query_preference":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "sine":3, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref","prohibit_deep_para"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "max_depth":6, "var_weight":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "depth_penalty":50, "sine":3, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.18/0.40 {"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.18/0.40 {"max_depth":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.18/0.40 {"depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref", "posunitpara"], "query_preference":0, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "sine":4, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_dseconds":50},
% 0.18/0.40 {"length_penalty":100, "depth_penalty":100, "query_preference":0, "strategy":["negative_pref", "hornpref", "max_weight"], "max_depth":2, "max_dseconds":50},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "depth_penalty":50, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.18/0.40 {"sine":2, "query_preference":0, "strategy":["unit"], "max_dseconds":50},
% 0.18/0.40 {"weight_select_ratio":100, "rewrite":0, "depth_penalty":100, "query_preference":0, "strategy":["unit", "posunitpara"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "max_size":30, "max_depth":10, "max_weight":300, "weight_select_ratio":1, "rewrite":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":50, "sine":5, "strategy":["negative_pref"], "query_preference":0, "max_depth":4},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref", "prohibit_nested_para"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "depth_penalty":100, "sine":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0, "sine":2},
% 0.18/0.40 {"sine":1, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit", "pure_unit"], "weight_select_ratio":1, "query_preference":0},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "rewrite":0, "query_preference":0, "strategy":["query_focus", "posunitpara"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "max_depth":2},
% 0.18/0.40 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100, "sine":2},
% 0.18/0.40 {"weight_select_ratio":100, "query_preference":0, "strategy":["negative_pref", "max_weight"], "max_dseconds":50},
% 0.18/0.40 {"weight_select_ratio":100, "var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["hardness_pref"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0, "reverse_clauselist":1},
% 0.18/0.40 {"var_weight":70, "repeat_var_weight":70, "query_preference":0, "strategy":["positive_pref"], "max_dseconds":50},
% 0.18/0.40 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "max_depth":4},
% 0.18/0.40
% 0.18/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":250, "strategy":["query_focus"], "query_preference":3},
% 0.18/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.18/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.18/0.40 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "max_depth":1},
% 0.18/0.40
% 0.18/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["query_focus"], "query_preference":3},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0, "sine":1},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0, "depth_penalty":100},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0, "rewrite":0},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":1, "depth_penalty":50, "length_penalty":100},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "max_depth":3},
% 0.18/0.40 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "max_depth":1}
% 0.18/0.40
% 0.18/0.40 ]}
% 0.18/0.40
% 0.18/0.40
% 0.18/0.40 **** run 1 fork 0 starts with strategy
% 0.18/0.40 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.18/0.40
% 0.18/0.40 **** run 2 fork 1 starts with strategy
% 0.18/0.40 {"max_dseconds":1,"sine":3,"strategy":["hardness_pref"],"query_preference":0}
% 0.18/0.40
% 0.18/0.40 **** run 3 fork 2 starts with strategy
% 0.18/0.40 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.18/0.40
% 0.18/0.40 **** run 4 fork 3 starts with strategy
% 0.18/0.40 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.18/0.40
% 0.18/0.40 **** run 5 fork 4 starts with strategy
% 0.18/0.40 {"max_dseconds":1,"strategy":["negative_pref","prohibit_unordered_para"],"query_preference":0}
% 0.18/0.41
% 0.18/0.41 **** run 6 fork 5 starts with strategy
% 0.18/0.41 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para"],"query_preference":0}
% 0.18/0.41
% 0.18/0.41 **** run 7 fork 6 starts with strategy
% 0.18/0.41 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para"],"query_preference":1}
% 0.18/0.41
% 0.18/0.41 **** run 8 fork 7 starts with strategy
% 0.18/0.41 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 0.18/0.49
% 0.18/0.49 fork 6: search finished without proof.
% 0.18/0.49
% 0.18/0.49 fork 5: search finished without proof.
% 0.18/0.51
% 0.18/0.51 **** run 15 fork 6 starts with strategy
% 0.18/0.51 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 0.18/0.52
% 0.18/0.52 **** run 14 fork 5 starts with strategy
% 0.18/0.52 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 0.18/0.54
% 0.18/0.54 fork 0: search finished without proof.
% 0.18/0.54
% 0.18/0.54 fork 2: search finished without proof.
% 0.18/0.54
% 0.18/0.54 fork 1: search finished without proof.
% 0.18/0.54
% 0.18/0.54 fork 7: search finished without proof.
% 0.18/0.54
% 0.18/0.54 fork 4: search finished without proof.
% 0.18/0.54
% 0.18/0.54 fork 3: search finished without proof.
% 0.18/0.55 No candidate clauses found.
% 0.18/0.55
% 0.18/0.55
% 0.18/0.55 fork 5: search terminated without proof.
% 0.18/0.56
% 0.18/0.56 **** run 9 fork 0 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"strategy":["unit","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 0.18/0.56
% 0.18/0.56 **** run 10 fork 1 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"],"query_preference":1}
% 0.18/0.56
% 0.18/0.56 **** run 13 fork 4 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 0.18/0.56
% 0.18/0.56 **** run 16 fork 7 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"sine":3,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 0.18/0.56
% 0.18/0.56 **** run 12 fork 3 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 0.18/0.56
% 0.18/0.56 **** run 11 fork 2 starts with strategy
% 0.18/0.56 {"max_dseconds":1,"strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"],"query_preference":0}
% 0.18/0.57
% 0.18/0.57 **** run 22 fork 5 starts with strategy
% 0.18/0.57 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"depth_penalty":100}
% 0.18/0.61
% 0.18/0.61 fork 0: search finished without proof.
% 0.18/0.62
% 0.18/0.62 fork 5: search finished without proof.
% 0.18/0.63
% 0.18/0.63 **** run 17 fork 0 starts with strategy
% 0.18/0.63 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 0.18/0.63
% 0.18/0.63 fork 6: search finished without proof.
% 0.18/0.63
% 0.18/0.63 fork 2: search finished without proof.
% 0.18/0.64
% 0.18/0.64 **** run 30 fork 5 starts with strategy
% 0.18/0.64 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 0.18/0.65
% 0.18/0.65 **** run 23 fork 6 starts with strategy
% 0.18/0.65 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 0.18/0.66
% 0.18/0.66 **** run 19 fork 2 starts with strategy
% 0.18/0.66 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 0.18/0.68
% 0.18/0.68 fork 1: search finished without proof.
% 0.18/0.68
% 0.18/0.68
% 0.18/0.68 fork 4: search terminated without proof.
% 0.18/0.70
% 0.18/0.70
% 0.18/0.70 fork 3: search terminated without proof.
% 0.18/0.70
% 0.18/0.70 **** run 18 fork 1 starts with strategy
% 0.18/0.70 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"sine":1}
% 0.18/0.70
% 0.18/0.70 **** run 21 fork 4 starts with strategy
% 0.18/0.70 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":1}
% 0.18/0.72
% 0.18/0.72 **** run 20 fork 3 starts with strategy
% 0.18/0.72 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 0.18/0.72
% 0.18/0.72 fork 7: search finished without proof.
% 0.18/0.75
% 0.18/0.75 **** run 24 fork 7 starts with strategy
% 0.18/0.75 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"rewrite":0}
% 0.18/0.76
% 0.18/0.76 fork 0: search finished without proof.
% 0.18/0.76
% 0.18/0.76 fork 2: search finished without proof.
% 0.18/0.77
% 0.18/0.77
% 0.18/0.77 fork 6: search terminated without proof.
% 0.18/0.77
% 0.18/0.77 fork 5: search finished without proof.
% 0.18/0.78
% 0.18/0.78 **** run 25 fork 0 starts with strategy
% 0.18/0.78 {"max_dseconds":1,"strategy":["hardness_pref","prohibit_deep_para"],"query_preference":0,"rewrite":0}
% 0.18/0.79
% 0.18/0.79 fork 4: search finished without proof.
% 0.18/0.79
% 0.18/0.79 **** run 31 fork 6 starts with strategy
% 0.18/0.79 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"sine":3,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 0.18/0.80
% 0.18/0.80 **** run 38 fork 5 starts with strategy
% 0.18/0.80 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_dseconds":1}
% 0.18/0.80
% 0.18/0.80 **** run 27 fork 2 starts with strategy
% 0.18/0.80 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":3}
% 0.18/0.81
% 0.18/0.81 **** run 29 fork 4 starts with strategy
% 0.18/0.81 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"max_depth":6,"var_weight":1}
% 3.01/0.83
% 3.01/0.83 fork 1: search finished without proof.
% 3.01/0.85
% 3.01/0.85 **** run 26 fork 1 starts with strategy
% 3.01/0.85 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 3.01/0.85
% 3.01/0.85
% 3.01/0.85 fork 3: search terminated without proof.
% 3.01/0.87
% 3.01/0.87 **** run 28 fork 3 starts with strategy
% 3.01/0.87 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":1}
% 3.76/0.88
% 3.76/0.88 fork 4: search finished without proof.
% 3.76/0.90
% 3.76/0.90 **** run 37 fork 4 starts with strategy
% 3.76/0.90 {"max_dseconds":1,"sine":4,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 3.76/0.90
% 3.76/0.90 fork 0: search finished without proof.
% 3.98/0.91
% 3.98/0.91 fork 6: search finished without proof.
% 3.98/0.91
% 3.98/0.91 fork 7: search finished without proof.
% 3.98/0.92
% 3.98/0.92 **** run 33 fork 0 starts with strategy
% 3.98/0.92 {"max_depth":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 3.98/0.92
% 3.98/0.92 **** run 39 fork 6 starts with strategy
% 3.98/0.92 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_depth":2,"max_dseconds":1}
% 4.14/0.93
% 4.14/0.93
% 4.14/0.93 fork 5: search terminated without proof.
% 4.14/0.93
% 4.14/0.93 **** run 32 fork 7 starts with strategy
% 4.14/0.93 {"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}
% 4.14/0.93
% 4.14/0.93
% 4.14/0.93 fork 2: search terminated without proof.
% 4.14/0.95
% 4.14/0.95 **** run 46 fork 5 starts with strategy
% 4.14/0.95 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 4.14/0.95
% 4.14/0.95 **** run 35 fork 2 starts with strategy
% 4.14/0.95 {"max_dseconds":1,"strategy":["hardness_pref","posunitpara"],"query_preference":0,"depth_penalty":50,"length_penalty":100}
% 4.14/0.96
% 4.14/0.96 fork 0: search finished without proof.
% 4.14/0.97
% 4.14/0.97
% 4.14/0.97 fork 1: search terminated without proof.
% 4.14/0.98
% 4.14/0.98 **** run 41 fork 0 starts with strategy
% 4.14/0.98 {"sine":2,"query_preference":0,"strategy":["unit"],"max_dseconds":1}
% 4.14/0.99
% 4.14/0.99 **** run 34 fork 1 starts with strategy
% 4.14/0.99 {"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 4.14/1.00
% 4.14/1.00
% 4.14/1.00 fork 3: search terminated without proof.
% 4.14/1.01
% 4.14/1.01 **** run 36 fork 3 starts with strategy
% 4.14/1.01 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 4.88/1.02
% 4.88/1.02 fork 4: search finished without proof.
% 4.88/1.03
% 4.88/1.03 fork 0: search finished without proof.
% 4.88/1.04
% 4.88/1.04 **** run 45 fork 4 starts with strategy
% 4.88/1.04 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 4.88/1.04
% 4.88/1.04 fork 1: search finished without proof.
% 4.88/1.04
% 4.88/1.04
% 4.88/1.04 fork 6: search terminated without proof.
% 4.88/1.05
% 4.88/1.05 **** run 49 fork 0 starts with strategy
% 4.88/1.05 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 4.88/1.06
% 4.88/1.06 **** run 42 fork 1 starts with strategy
% 4.88/1.06 {"weight_select_ratio":100,"rewrite":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":1}
% 4.88/1.06
% 4.88/1.06
% 4.88/1.06 fork 7: search terminated without proof.
% 4.88/1.06
% 4.88/1.06 **** run 47 fork 6 starts with strategy
% 4.88/1.06 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 4.88/1.06
% 4.88/1.06 fork 5: search finished without proof.
% 4.88/1.07
% 4.88/1.07
% 4.88/1.07 fork 2: search terminated without proof.
% 4.88/1.07
% 4.88/1.07 **** run 40 fork 7 starts with strategy
% 4.88/1.07 {"sine":1,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 4.88/1.08
% 4.88/1.08 **** run 54 fork 5 starts with strategy
% 4.88/1.08 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0,"sine":2}
% 5.46/1.09
% 5.46/1.09 **** run 43 fork 2 starts with strategy
% 5.46/1.09 {"max_dseconds":1,"strategy":["unit","pure_unit"],"max_size":30,"max_depth":10,"max_weight":300,"weight_select_ratio":1,"rewrite":0}
% 5.46/1.10
% 5.46/1.10 fork 0: search finished without proof.
% 5.46/1.10
% 5.46/1.10 fork 1: search finished without proof.
% 5.46/1.11
% 5.46/1.11 fork 5: search finished without proof.
% 5.46/1.12 No candidate clauses found.
% 5.46/1.12
% 5.46/1.12
% 5.46/1.12 fork 2: search terminated without proof.
% 5.46/1.12
% 5.46/1.12 **** run 57 fork 0 starts with strategy
% 5.46/1.12 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 5.46/1.12
% 5.46/1.12 **** run 50 fork 1 starts with strategy
% 5.46/1.12 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1,"length_penalty":100}
% 5.46/1.12
% 5.46/1.12 **** run 62 fork 5 starts with strategy
% 5.46/1.12 {"weight_select_ratio":100,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":1}
% 5.46/1.13
% 5.46/1.13 fork 3: search finished without proof.
% 5.46/1.13
% 5.46/1.13 **** run 51 fork 2 starts with strategy
% 5.46/1.13 {"max_dseconds":1,"strategy":["negative_pref","prohibit_nested_para"],"query_preference":0}
% 5.46/1.15
% 5.46/1.15 **** run 44 fork 3 starts with strategy
% 5.46/1.15 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 5.46/1.17
% 5.46/1.17
% 5.46/1.17 fork 4: search terminated without proof.
% 6.14/1.18
% 6.14/1.18
% 6.14/1.18 fork 6: search terminated without proof.
% 6.14/1.18
% 6.14/1.18 fork 3: search finished without proof.
% 6.14/1.19
% 6.14/1.19 **** run 53 fork 4 starts with strategy
% 6.14/1.19 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"depth_penalty":100,"sine":1}
% 6.14/1.20
% 6.14/1.20 fork 7: search finished without proof.
% 6.14/1.20
% 6.14/1.20 **** run 55 fork 6 starts with strategy
% 6.14/1.20 {"sine":1,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":1}
% 6.14/1.20
% 6.14/1.20 **** run 52 fork 3 starts with strategy
% 6.14/1.20 {"max_dseconds":1,"strategy":["unit","pure_unit"],"query_preference":0}
% 6.36/1.21
% 6.36/1.21 **** run 48 fork 7 starts with strategy
% 6.36/1.21 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 6.36/1.23 No candidate clauses found.
% 6.36/1.23
% 6.36/1.23
% 6.36/1.23 fork 3: search terminated without proof.
% 6.55/1.24
% 6.55/1.24 **** run 60 fork 3 starts with strategy
% 6.55/1.24 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"max_depth":2}
% 6.55/1.24
% 6.55/1.24
% 6.55/1.24 fork 0: search terminated without proof.
% 6.55/1.25
% 6.55/1.25
% 6.55/1.25 fork 1: search terminated without proof.
% 6.55/1.25
% 6.55/1.25 fork 5: search finished without proof.
% 6.55/1.26
% 6.55/1.26
% 6.55/1.26 fork 2: search terminated without proof.
% 6.55/1.26
% 6.55/1.26 **** run 65 fork 0 starts with strategy
% 6.55/1.26 {"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["positive_pref"],"max_dseconds":1}
% 6.55/1.26
% 6.55/1.26 **** run 58 fork 1 starts with strategy
% 6.55/1.26 {"max_dseconds":1,"strategy":["unit","pure_unit"],"weight_select_ratio":1,"query_preference":0}
% 6.55/1.27
% 6.55/1.27 **** run 70 fork 5 starts with strategy
% 6.55/1.27 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 6.55/1.28
% 6.55/1.28 **** run 59 fork 2 starts with strategy
% 6.55/1.28 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"query_preference":0,"strategy":["query_focus","posunitpara"],"max_dseconds":1}
% 6.55/1.29 No candidate clauses found.
% 6.55/1.29
% 6.55/1.29
% 6.55/1.29 fork 1: search terminated without proof.
% 6.55/1.31
% 6.55/1.31 **** run 66 fork 1 starts with strategy
% 6.55/1.31 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"max_depth":4}
% 6.55/1.31
% 6.55/1.31
% 6.55/1.31 fork 4: search terminated without proof.
% 6.55/1.32
% 6.55/1.32 fork 6: search finished without proof.
% 7.28/1.33
% 7.28/1.33 **** run 61 fork 4 starts with strategy
% 7.28/1.33 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100,"sine":2}
% 7.28/1.33
% 7.28/1.33 **** run 63 fork 6 starts with strategy
% 7.28/1.33 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":1}
% 7.28/1.34
% 7.28/1.34
% 7.28/1.34 fork 7: search terminated without proof.
% 7.28/1.36
% 7.28/1.36 fork 1: search finished without proof.
% 7.28/1.36
% 7.28/1.36 **** run 56 fork 7 starts with strategy
% 7.28/1.36 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"rewrite":0}
% 7.28/1.37
% 7.28/1.37
% 7.28/1.37 fork 3: search terminated without proof.
% 7.28/1.37
% 7.28/1.37 **** run 74 fork 1 starts with strategy
% 7.28/1.37 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 7.28/1.38
% 7.28/1.38 fork 0: search finished without proof.
% 7.28/1.38
% 7.28/1.38 **** run 68 fork 3 starts with strategy
% 7.28/1.38 {"max_dseconds":10,"sine":3,"strategy":["hardness_pref"],"query_preference":0}
% 7.28/1.40
% 7.28/1.40 **** run 73 fork 0 starts with strategy
% 7.28/1.40 {"max_dseconds":10,"strategy":["unit","prohibit_unordered_para"],"query_preference":1}
% 7.28/1.41
% 7.28/1.41 fork 7: search finished without proof.
% 7.28/1.42
% 7.28/1.42 fork 2: search finished without proof.
% 7.28/1.43
% 7.28/1.43 **** run 64 fork 7 starts with strategy
% 7.28/1.43 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1}
% 7.28/1.45
% 7.28/1.45 **** run 67 fork 2 starts with strategy
% 7.28/1.45 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 7.28/1.45
% 7.28/1.45 fork 0: search finished without proof.
% 7.28/1.45
% 7.28/1.45 fork 6: search finished without proof.
% 7.28/1.46
% 7.28/1.46 fork 4: search finished without proof.
% 7.28/1.47
% 7.28/1.47 **** run 81 fork 0 starts with strategy
% 7.28/1.47 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 7.28/1.47
% 7.28/1.47 **** run 71 fork 6 starts with strategy
% 7.28/1.47 {"max_dseconds":10,"strategy":["negative_pref","prohibit_unordered_para"],"query_preference":0}
% 7.28/1.48
% 7.28/1.48 **** run 69 fork 4 starts with strategy
% 7.28/1.48 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 8.51/1.57
% 8.51/1.57 fork 7: search finished without proof.
% 8.51/1.58
% 8.51/1.58 **** run 72 fork 7 starts with strategy
% 8.51/1.58 {"max_dseconds":10,"strategy":["unit","prohibit_unordered_para"],"query_preference":0}
% 9.47/1.64
% 9.47/1.64 fork 7: search finished without proof.
% 9.47/1.65
% 9.47/1.65 **** run 80 fork 7 starts with strategy
% 9.47/1.65 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":3}
% 9.47/1.68 No candidate clauses found.
% 9.47/1.68
% 9.47/1.68
% 9.47/1.68 fork 7: search terminated without proof.
% 9.47/1.70
% 9.47/1.70 **** run 88 fork 7 starts with strategy
% 9.47/1.70 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"depth_penalty":100}
% 10.25/1.75
% 10.25/1.75 fork 7: search finished without proof.
% 10.25/1.76
% 10.25/1.76 **** run 96 fork 7 starts with strategy
% 10.25/1.76 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":10}
% 13.39/2.29
% 13.39/2.29 fork 5: search finished without proof.
% 14.67/2.31
% 14.67/2.31 **** run 78 fork 5 starts with strategy
% 14.67/2.31 {"max_dseconds":10,"strategy":["negative_pref","prohibit_nested_para","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 15.05/2.39
% 15.05/2.39 fork 1: search finished without proof.
% 15.05/2.39
% 15.05/2.39 fork 3: search finished without proof.
% 15.75/2.41
% 15.75/2.41 **** run 82 fork 1 starts with strategy
% 15.75/2.41 {"max_dseconds":10,"sine":3,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 15.75/2.41
% 15.75/2.41 **** run 76 fork 3 starts with strategy
% 15.75/2.41 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_unordered_para","prohibit_deep_para"],"query_preference":1}
% 15.75/2.43
% 15.75/2.43 fork 6: search finished without proof.
% 15.75/2.45
% 15.75/2.45 **** run 79 fork 6 starts with strategy
% 15.75/2.45 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0}
% 15.75/2.47
% 15.75/2.47 fork 4: search finished without proof.
% 16.41/2.49
% 16.41/2.49 **** run 77 fork 4 starts with strategy
% 16.41/2.49 {"max_dseconds":10,"strategy":["unit","prohibit_nested_para","prohibit_deep_para","prohibit_unordered_para"],"query_preference":0}
% 16.41/2.49
% 16.41/2.49 fork 0: search finished without proof.
% 16.41/2.51
% 16.41/2.51 **** run 89 fork 0 starts with strategy
% 16.41/2.51 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 16.41/2.52
% 16.41/2.52 fork 2: search finished without proof.
% 16.41/2.54
% 16.41/2.54 **** run 75 fork 2 starts with strategy
% 16.41/2.54 {"max_dseconds":10,"strategy":["unit","prohibit_unordered_para","prohibit_deep_para"],"query_preference":0}
% 16.41/2.54
% 16.41/2.54 fork 4: search finished without proof.
% 16.41/2.55
% 16.41/2.55 **** run 85 fork 4 starts with strategy
% 16.41/2.55 {"max_dseconds":10,"strategy":["unit"],"query_preference":0}
% 17.20/2.59
% 17.20/2.59 fork 2: search finished without proof.
% 17.20/2.60
% 17.20/2.60 **** run 83 fork 2 starts with strategy
% 17.20/2.60 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 17.20/2.60
% 17.20/2.60 fork 4: search finished without proof.
% 17.43/2.62
% 17.43/2.62 **** run 93 fork 4 starts with strategy
% 17.43/2.62 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"max_depth":3}
% 18.17/2.79
% 18.17/2.79 fork 7: search finished without proof.
% 18.81/2.80
% 18.81/2.80 **** run 104 fork 7 starts with strategy
% 18.81/2.80 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_dseconds":10}
% 22.65/3.30
% 22.65/3.30 fork 5: search finished without proof.
% 22.84/3.32
% 22.84/3.32 **** run 86 fork 5 starts with strategy
% 22.84/3.32 {"max_dseconds":10,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 23.00/3.40
% 23.00/3.40 fork 3: search finished without proof.
% 23.73/3.42
% 23.73/3.42 **** run 84 fork 3 starts with strategy
% 23.73/3.42 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"sine":1}
% 23.73/3.43
% 23.73/3.43 fork 6: search finished without proof.
% 23.73/3.44
% 23.73/3.44 **** run 87 fork 6 starts with strategy
% 23.73/3.44 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"sine":1}
% 23.73/3.46
% 23.73/3.46 fork 0: search finished without proof.
% 23.73/3.48
% 23.73/3.48 **** run 97 fork 0 starts with strategy
% 23.73/3.48 {"var_weight":70,"repeat_var_weight":70,"depth_penalty":50,"sine":3,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":10}
% 23.73/3.48
% 23.73/3.48
% 23.73/3.48 fork 1: search terminated without proof.
% 24.32/3.49
% 24.32/3.49 fork 6: search finished without proof.
% 24.32/3.50
% 24.32/3.50 **** run 90 fork 1 starts with strategy
% 24.32/3.50 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"rewrite":0}
% 24.32/3.51
% 24.32/3.51 **** run 95 fork 6 starts with strategy
% 24.32/3.51 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"max_depth":6,"var_weight":1}
% 24.32/3.56
% 24.32/3.56 fork 6: search finished without proof.
% 24.32/3.57
% 24.32/3.57 **** run 103 fork 6 starts with strategy
% 24.32/3.57 {"max_dseconds":10,"sine":4,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 24.32/3.59
% 24.32/3.59 fork 4: search finished without proof.
% 24.32/3.61
% 24.32/3.61 **** run 101 fork 4 starts with strategy
% 24.32/3.61 {"max_dseconds":10,"strategy":["hardness_pref","posunitpara"],"query_preference":0,"depth_penalty":50,"length_penalty":100}
% 24.32/3.65
% 24.32/3.65
% 24.32/3.65 fork 2: search terminated without proof.
% 24.32/3.66
% 24.32/3.66 **** run 91 fork 2 starts with strategy
% 24.32/3.66 {"max_dseconds":10,"strategy":["hardness_pref","prohibit_deep_para"],"query_preference":0,"rewrite":0}
% 27.32/3.90
% 27.32/3.90
% 27.32/3.90 fork 7: search terminated without proof.
% 27.32/3.92
% 27.32/3.92 **** run 112 fork 7 starts with strategy
% 27.32/3.92 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 31.28/4.41
% 31.28/4.41
% 31.28/4.41 fork 5: search terminated without proof.
% 31.59/4.43
% 31.59/4.43 **** run 94 fork 5 starts with strategy
% 31.59/4.43 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"max_depth":1}
% 31.59/4.45
% 31.59/4.45 fork 3: search finished without proof.
% 31.59/4.46
% 31.59/4.46 **** run 92 fork 3 starts with strategy
% 31.59/4.46 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 31.59/4.48
% 31.59/4.48 fork 0: search finished without proof.
% 31.59/4.49
% 31.59/4.49 **** run 105 fork 0 starts with strategy
% 31.59/4.49 {"length_penalty":100,"depth_penalty":100,"query_preference":0,"strategy":["negative_pref","hornpref","max_weight"],"max_depth":2,"max_dseconds":10}
% 32.23/4.52
% 32.23/4.52 fork 1: search finished without proof.
% 32.23/4.54
% 32.23/4.54 **** run 98 fork 1 starts with strategy
% 32.23/4.54 {"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}
% 32.23/4.55
% 32.23/4.55 fork 6: search finished without proof.
% 32.23/4.56
% 32.23/4.56 **** run 111 fork 6 starts with strategy
% 32.23/4.56 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 32.82/4.64
% 32.82/4.64 fork 4: search finished without proof.
% 32.82/4.65
% 32.82/4.65 **** run 109 fork 4 starts with strategy
% 32.82/4.65 {"max_dseconds":10,"strategy":["unit","pure_unit"],"max_size":30,"max_depth":10,"max_weight":300,"weight_select_ratio":1,"rewrite":0}
% 33.53/4.68 No candidate clauses found.
% 33.53/4.68
% 33.53/4.68
% 33.53/4.68 fork 4: search terminated without proof.
% 33.67/4.69
% 33.67/4.69 fork 2: search finished without proof.
% 33.67/4.69
% 33.67/4.69 **** run 117 fork 4 starts with strategy
% 33.67/4.69 {"max_dseconds":10,"strategy":["negative_pref","prohibit_nested_para"],"query_preference":0}
% 33.67/4.70
% 33.67/4.70 **** run 99 fork 2 starts with strategy
% 33.67/4.70 {"max_depth":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":10}
% 33.96/4.75
% 33.96/4.75 fork 2: search finished without proof.
% 33.96/4.76
% 33.96/4.76 **** run 107 fork 2 starts with strategy
% 33.96/4.76 {"sine":2,"query_preference":0,"strategy":["unit"],"max_dseconds":10}
% 33.96/4.81
% 33.96/4.81 fork 2: search finished without proof.
% 33.96/4.83
% 33.96/4.83 **** run 115 fork 2 starts with strategy
% 33.96/4.83 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 33.96/4.88
% 33.96/4.88 fork 2: search finished without proof.
% 33.96/4.91
% 33.96/4.91 **** run 123 fork 2 starts with strategy
% 33.96/4.91 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 35.34/4.96
% 35.34/4.96
% 35.34/4.96 fork 7: search terminated without proof.
% 35.34/4.97
% 35.34/4.97 **** run 120 fork 7 starts with strategy
% 35.34/4.97 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0,"sine":2}
% 35.34/5.01
% 35.34/5.01 fork 7: search finished without proof.
% 36.22/5.03
% 36.22/5.03 **** run 128 fork 7 starts with strategy
% 36.22/5.03 {"weight_select_ratio":100,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":10}
% 38.61/5.40
% 38.61/5.40 fork 5: search finished without proof.
% 39.34/5.42
% 39.34/5.42 **** run 102 fork 5 starts with strategy
% 39.34/5.42 {"max_dseconds":10,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 39.34/5.48
% 39.34/5.48 fork 3: search finished without proof.
% 39.98/5.50
% 39.98/5.50 **** run 100 fork 3 starts with strategy
% 39.98/5.50 {"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":10}
% 39.98/5.54
% 39.98/5.54 fork 3: search finished without proof.
% 39.98/5.54
% 39.98/5.54 fork 1: search finished without proof.
% 39.98/5.55
% 39.98/5.55
% 39.98/5.55 fork 0: search terminated without proof.
% 39.98/5.56
% 39.98/5.56 **** run 108 fork 3 starts with strategy
% 39.98/5.56 {"weight_select_ratio":100,"rewrite":0,"depth_penalty":100,"query_preference":0,"strategy":["unit","posunitpara"],"max_dseconds":10}
% 39.98/5.56
% 39.98/5.56 **** run 106 fork 1 starts with strategy
% 39.98/5.56 {"sine":1,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"depth_penalty":50,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":10}
% 39.98/5.56
% 39.98/5.56 **** run 113 fork 0 starts with strategy
% 39.98/5.56 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 39.98/5.57
% 39.98/5.57 fork 6: search finished without proof.
% 40.68/5.59
% 40.68/5.59 **** run 119 fork 6 starts with strategy
% 40.68/5.59 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"depth_penalty":100,"sine":1}
% 40.68/5.60
% 40.68/5.60 fork 3: search finished without proof.
% 40.68/5.62
% 40.68/5.62 **** run 116 fork 3 starts with strategy
% 40.68/5.62 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1,"length_penalty":100}
% 41.35/5.70
% 41.35/5.70 fork 4: search finished without proof.
% 41.35/5.71
% 41.35/5.71 **** run 125 fork 4 starts with strategy
% 41.35/5.71 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"rewrite":0,"query_preference":0,"strategy":["query_focus","posunitpara"],"max_dseconds":10}
% 42.95/5.90
% 42.95/5.90 fork 2: search finished without proof.
% 42.95/5.92
% 42.95/5.92 **** run 131 fork 2 starts with strategy
% 42.95/5.92 {"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["positive_pref"],"max_dseconds":10}
% 43.85/6.01
% 43.85/6.01 fork 7: search finished without proof.
% 44.14/6.03
% 44.14/6.03 **** run 136 fork 7 starts with strategy
% 44.14/6.03 {"max_dseconds":50,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 47.01/6.42
% 47.01/6.42 fork 5: search finished without proof.
% 47.31/6.44
% 47.31/6.44 **** run 110 fork 5 starts with strategy
% 47.31/6.44 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0}
% 47.31/6.48
% 47.31/6.48 fork 5: search finished without proof.
% 47.31/6.49
% 47.31/6.49 **** run 118 fork 5 starts with strategy
% 47.31/6.49 {"max_dseconds":10,"strategy":["unit","pure_unit"],"query_preference":0}
% 47.86/6.52 No candidate clauses found.
% 47.86/6.52
% 47.86/6.52
% 47.86/6.52 fork 5: search terminated without proof.
% 47.86/6.53
% 47.86/6.53 **** run 126 fork 5 starts with strategy
% 47.86/6.53 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"max_depth":2}
% 47.86/6.56
% 47.86/6.56 fork 0: search finished without proof.
% 48.39/6.58
% 48.39/6.58 **** run 121 fork 0 starts with strategy
% 48.39/6.58 {"sine":1,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["negative_pref","max_weight"],"max_dseconds":10}
% 48.39/6.58
% 48.39/6.58 fork 1: search finished without proof.
% 48.39/6.60
% 48.39/6.60 **** run 114 fork 1 starts with strategy
% 48.39/6.60 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0,"max_depth":4}
% 48.39/6.60
% 48.39/6.60 fork 6: search finished without proof.
% 48.39/6.62
% 48.39/6.62 **** run 127 fork 6 starts with strategy
% 48.39/6.62 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100,"sine":2}
% 49.16/6.68
% 49.16/6.68
% 49.16/6.68 fork 3: search terminated without proof.
% 49.43/6.70
% 49.43/6.70 **** run 124 fork 3 starts with strategy
% 49.43/6.70 {"max_dseconds":10,"strategy":["unit","pure_unit"],"weight_select_ratio":1,"query_preference":0}
% 49.43/6.72 No candidate clauses found.
% 49.43/6.72
% 49.43/6.72
% 49.43/6.72 fork 3: search terminated without proof.
% 49.70/6.73
% 49.70/6.73 **** run 132 fork 3 starts with strategy
% 49.70/6.73 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"max_depth":4}
% 49.70/6.74
% 49.70/6.74
% 49.70/6.74 fork 4: search terminated without proof.
% 49.70/6.76
% 49.70/6.76 **** run 133 fork 4 starts with strategy
% 49.70/6.76 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0}
% 49.70/6.79
% 49.70/6.79 fork 3: search finished without proof.
% 50.26/6.80
% 50.26/6.80 **** run 140 fork 3 starts with strategy
% 50.26/6.80 {"max_dseconds":50,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 50.26/6.91
% 50.26/6.91 fork 2: search finished without proof.
% 50.26/6.93
% 50.26/6.93 **** run 139 fork 2 starts with strategy
% 50.26/6.93 {"max_dseconds":50,"strategy":["unit","prohibit_unordered_para"],"query_preference":1}
% 50.26/6.98
% 50.26/6.98 fork 2: search finished without proof.
% 51.35/6.99
% 51.35/6.99 **** run 147 fork 2 starts with strategy
% 51.35/6.99 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":1,"depth_penalty":50,"length_penalty":100}
% 55.76/7.52
% 55.76/7.52 fork 5: search finished without proof.
% 55.76/7.54
% 55.76/7.54 **** run 134 fork 5 starts with strategy
% 55.76/7.54 {"max_dseconds":50,"sine":3,"strategy":["hardness_pref"],"query_preference":0}
% 55.76/7.59
% 55.76/7.59 fork 1: search finished without proof.
% 55.76/7.59
% 55.76/7.59 fork 0: search finished without proof.
% 55.76/7.60
% 55.76/7.60 **** run 122 fork 1 starts with strategy
% 55.76/7.60 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"rewrite":0}
% 55.76/7.61
% 55.76/7.61 **** run 129 fork 0 starts with strategy
% 55.76/7.61 {"weight_select_ratio":100,"var_weight":70,"repeat_var_weight":70,"query_preference":0,"strategy":["hardness_pref"],"max_dseconds":10}
% 55.76/7.65
% 55.76/7.65 fork 1: search finished without proof.
% 55.76/7.66
% 55.76/7.66
% 55.76/7.66 fork 6: search terminated without proof.
% 55.76/7.68
% 55.76/7.68 **** run 130 fork 1 starts with strategy
% 55.76/7.68 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0,"reverse_clauselist":1}
% 55.76/7.68
% 55.76/7.68 **** run 135 fork 6 starts with strategy
% 55.76/7.68 {"max_dseconds":50,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 61.64/8.31
% 61.64/8.31
% 61.64/8.31 result: proof found
% 61.64/8.31 for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.64/8.31 by run 140 fork 3 strategy {"max_dseconds":50,"strategy":["hardness_pref","prohibit_unordered_para"],"query_preference":1}
% 61.64/8.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.64/8.31
% 61.64/8.31 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.64/8.31 fof('co1_$sk', plain, (((~in(X9,X8) | (~(X1 = X9) | (~in(X7,X8) | (~(X2 = X7) | (~young(X1) | (~man(X1) | (~fellow(X1) | (~young(X2) | (~man(X2) | (~fellow(X2) | ((X2 = X1) | (~front(X8) | (~furniture(X8) | (~seat(X8) | (~in(X6,X5) | (~down(X6,X3) | (~barrel(X6,X4) | (~old(X4) | (~dirty(X4) | (~white(X4) | (~car(X4) | (~chevy(X4) | (~lonely(X3) | (~way(X3) | (~street(X3) | (~event(X6) | (~city(X5) | ~hollywood(X5)))))))))))))))))))))))))))) & (in($sk9,$sk8) & (($sk1 = $sk9) & (in($sk7,$sk8) & (($sk2 = $sk7) & (young($sk1) & (man($sk1) & (fellow($sk1) & (young($sk2) & (man($sk2) & (fellow($sk2) & (~($sk2 = $sk1) & (front($sk8) & (furniture($sk8) & (seat($sk8) & (in($sk6,$sk5) & (down($sk6,$sk3) & (barrel($sk6,$sk4) & (lonely($sk3) & (way($sk3) & (street($sk3) & (old($sk4) & (dirty($sk4) & (white($sk4) & (car($sk4) & (chevy($sk4) & (event($sk6) & (city($sk5) & hollywood($sk5))))))))))))))))))))))))))))) | ((~in(X18,X17) | (~(X10 = X18) | (~in(X16,X17) | (~(X11 = X16) | (~young(X10) | (~man(X10) | (~fellow(X10) | (~young(X11) | (~man(X11) | (~fellow(X11) | ((X11 = X10) | (~front(X17) | (~furniture(X17) | (~seat(X17) | (~in(X15,X14) | (~down(X15,X12) | (~barrel(X15,X13) | (~lonely(X12) | (~way(X12) | (~street(X12) | (~old(X13) | (~dirty(X13) | (~white(X13) | (~car(X13) | (~chevy(X13) | (~event(X15) | (~city(X14) | ~hollywood(X14)))))))))))))))))))))))))))) & (in($sk18,$sk17) & (($sk10 = $sk18) & (in($sk16,$sk17) & (($sk11 = $sk16) & (young($sk10) & (man($sk10) & (fellow($sk10) & (young($sk11) & (man($sk11) & (fellow($sk11) & (~($sk11 = $sk10) & (front($sk17) & (furniture($sk17) & (seat($sk17) & (in($sk15,$sk14) & (down($sk15,$sk12) & (barrel($sk15,$sk13) & (old($sk13) & (dirty($sk13) & (white($sk13) & (car($sk13) & (chevy($sk13) & (lonely($sk12) & (way($sk12) & (street($sk12) & (event($sk15) & (city($sk14) & hollywood($sk14)))))))))))))))))))))))))))))),
% 61.64/8.31 inference(negpush_and_skolemize,[],['co1'])).
% 61.64/8.31 fof('co1', conjecture, (((? [U,V,W,X,Y,Z,X1,X2,X3] : (((((((((((((((((((((((((((hollywood(U) & city(U)) & event(V)) & street(W)) & way(W)) & lonely(W)) & chevy(X)) & car(X)) & white(X)) & dirty(X)) & old(X)) & barrel(V,X)) & down(V,W)) & in(V,U)) & seat(X1)) & furniture(X1)) & front(X1)) & ~(Y = Z)) & fellow(Y)) & man(Y)) & young(Y)) & fellow(Z)) & man(Z)) & young(Z)) & (Y = X2)) & in(X2,X1)) & (Z = X3)) & in(X3,X1))) => (? [X4,X5,X6,X7,X8,X9,X10,X11,X12] : (((((((((((((((((((((((((((hollywood(X4) & city(X4)) & event(X5)) & chevy(X6)) & car(X6)) & white(X6)) & dirty(X6)) & old(X6)) & street(X7)) & way(X7)) & lonely(X7)) & barrel(X5,X6)) & down(X5,X7)) & in(X5,X4)) & seat(X10)) & furniture(X10)) & front(X10)) & ~(X8 = X9)) & fellow(X8)) & man(X8)) & young(X8)) & fellow(X9)) & man(X9)) & young(X9)) & (X8 = X11)) & in(X11,X10)) & (X9 = X12)) & in(X12,X10)))) & ((? [X13,X14,X15,X16,X17,X18,X19,X20,X21] : (((((((((((((((((((((((((((hollywood(X13) & city(X13)) & event(X14)) & chevy(X15)) & car(X15)) & white(X15)) & dirty(X15)) & old(X15)) & street(X16)) & way(X16)) & lonely(X16)) & barrel(X14,X15)) & down(X14,X16)) & in(X14,X13)) & seat(X19)) & furniture(X19)) & front(X19)) & ~(X17 = X18)) & fellow(X17)) & man(X17)) & young(X17)) & fellow(X18)) & man(X18)) & young(X18)) & (X17 = X20)) & in(X20,X19)) & (X18 = X21)) & in(X21,X19))) => (? [X22,X23,X24,X25,X26,X27,X28,X29,X30] : (((((((((((((((((((((((((((hollywood(X22) & city(X22)) & event(X23)) & street(X24)) & way(X24)) & lonely(X24)) & chevy(X25)) & car(X25)) & white(X25)) & dirty(X25)) & old(X25)) & barrel(X23,X25)) & down(X23,X24)) & in(X23,X22)) & seat(X28)) & furniture(X28)) & front(X28)) & ~(X26 = X27)) & fellow(X26)) & man(X26)) & young(X26)) & fellow(X27)) & man(X27)) & young(X27)) & (X26 = X29)) & in(X29,X28)) & (X27 = X30)) & in(X30,X28))))),
% 61.64/8.31 input).
% 61.64/8.31 cnf('1', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~barrel(U,X) | ~down(U,Y) | ~in(U,Z) | ~in(W,X2007) | ~in(X2008,X2007) | V != W | X2006 != X2008 | V = X2006 | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2007) | ~furniture(X2007) | ~front(X2007) | ~fellow(V) | ~fellow(X2006) | ~man(V) | ~man(X2006) | ~young(V) | ~young(X2006)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('2', plain, (~$df2(X,Y,Z,U,V,V,W,X2006,X2007) | ~barrel(U,X) | ~down(U,Y) | ~in(X2007,X2006) | ~in(V,X2006) | ~in(U,Z) | W != X2007 | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['1'])).
% 61.64/8.31 cnf('3', plain, (~$df2(X,Y,Z,U,V,V,W,X2006,W) | ~barrel(U,X) | ~down(U,Y) | ~in(W,X2006) | ~in(V,X2006) | ~in(U,Z) | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['2'])).
% 61.64/8.31 cnf('4', plain, ($df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('5', plain, ($df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~barrel(X2009,X2010) | ~down(X2009,X2011) | ~in(X2012,X2013) | ~in(X2014,X2013) | ~in(X2009,X2015) | X2012 = X2014 | ~hollywood(X2015) | ~city(X2015) | ~event(X2009) | ~chevy(X2010) | ~car(X2010) | ~white(X2010) | ~dirty(X2010) | ~old(X2010) | ~street(X2011) | ~way(X2011) | ~lonely(X2011) | ~seat(X2013) | ~furniture(X2013) | ~front(X2013) | ~fellow(X2012) | ~fellow(X2014) | ~man(X2012) | ~man(X2014) | ~young(X2012) | ~young(X2014)),
% 61.64/8.31 inference(resolution,[],['3','4'])).
% 61.64/8.31 cnf('6', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~barrel(U,X) | ~down(U,Y) | ~in(U,Z) | ~in(W,X2007) | ~in(X2008,X2007) | V != W | X2006 != X2008 | V = X2006 | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2007) | ~furniture(X2007) | ~front(X2007) | ~fellow(V) | ~fellow(X2006) | ~man(V) | ~man(X2006) | ~young(V) | ~young(X2006)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('7', plain, (~$df1(X,Y,Z,U,V,V,W,X2006,X2007) | ~barrel(U,X) | ~down(U,Y) | ~in(X2007,X2006) | ~in(V,X2006) | ~in(U,Z) | W != X2007 | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['6'])).
% 61.64/8.31 cnf('8', plain, (~$df1(X,Y,Z,U,V,V,W,X2006,W) | ~barrel(U,X) | ~down(U,Y) | ~in(W,X2006) | ~in(V,X2006) | ~in(U,Z) | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['7'])).
% 61.64/8.31 cnf('9', plain, (~barrel(X,Y) | ~barrel(Z,U) | ~down(X,V) | ~down(Z,W) | ~in(X2006,X2007) | ~in(X2008,X2007) | ~in(X,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | ~in(Z,X2013) | X2006 = X2008 | X2012 = X2010 | ~hollywood(X2009) | ~hollywood(X2013) | ~city(X2009) | ~city(X2013) | ~event(X) | ~event(Z) | ~chevy(Y) | ~chevy(U) | ~car(Y) | ~car(U) | ~white(Y) | ~white(U) | ~dirty(Y) | ~dirty(U) | ~old(Y) | ~old(U) | ~street(V) | ~street(W) | ~way(V) | ~way(W) | ~lonely(V) | ~lonely(W) | ~seat(X2007) | ~seat(X2011) | ~furniture(X2007) | ~furniture(X2011) | ~front(X2007) | ~front(X2011) | ~fellow(X2006) | ~fellow(X2008) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2006) | ~man(X2008) | ~man(X2010) | ~man(X2012) | ~young(X2006) | ~young(X2008) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(resolution,[],['5','8'])).
% 61.64/8.31 cnf('10', plain, (~barrel(X,Y) | ~down(X,Z) | ~down(X,U) | ~in(V,W) | ~in(X2006,W) | ~in(X2007,X2008) | ~in(X2009,X2008) | ~in(X,X2010) | ~in(X,X2011) | V = X2006 | X2009 = X2007 | ~hollywood(X2010) | ~hollywood(X2011) | ~city(X2010) | ~city(X2011) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~street(U) | ~way(Z) | ~way(U) | ~lonely(Z) | ~lonely(U) | ~seat(W) | ~seat(X2008) | ~furniture(W) | ~furniture(X2008) | ~front(W) | ~front(X2008) | ~fellow(V) | ~fellow(X2006) | ~fellow(X2007) | ~fellow(X2009) | ~man(V) | ~man(X2006) | ~man(X2007) | ~man(X2009) | ~young(V) | ~young(X2006) | ~young(X2007) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['9'])).
% 61.64/8.31 cnf('11', plain, (~barrel(X,Y) | ~down(X,Z) | ~down(X,U) | ~in(V,W) | ~in(X2006,W) | ~in(X2007,W) | ~in(X,X2008) | ~in(X,X2009) | V = X2006 | X2006 = X2007 | ~hollywood(X2008) | ~hollywood(X2009) | ~city(X2008) | ~city(X2009) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~street(U) | ~way(Z) | ~way(U) | ~lonely(Z) | ~lonely(U) | ~seat(W) | ~furniture(W) | ~front(W) | ~fellow(V) | ~fellow(X2006) | ~fellow(X2007) | ~man(V) | ~man(X2006) | ~man(X2007) | ~young(V) | ~young(X2006) | ~young(X2007)),
% 61.64/8.31 inference(factorization,[],['10'])).
% 61.64/8.31 cnf('12', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(W,V) | ~in(X2006,V) | ~in(X,X2007) | ~in(X,X2008) | W = U | X2006 = W | ~hollywood(X2007) | ~hollywood(X2008) | ~city(X2007) | ~city(X2008) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~furniture(V) | ~front(V) | ~fellow(U) | ~fellow(W) | ~fellow(X2006) | ~man(U) | ~man(W) | ~man(X2006) | ~young(U) | ~young(W) | ~young(X2006)),
% 61.64/8.31 inference(factorization,[],['11'])).
% 61.64/8.31 cnf('13', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(W,V) | ~in(X,X2006) | ~in(X,X2007) | U = W | W = U | ~hollywood(X2006) | ~hollywood(X2007) | ~city(X2006) | ~city(X2007) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~furniture(V) | ~front(V) | ~fellow(U) | ~fellow(W) | ~man(U) | ~man(W) | ~young(U) | ~young(W)),
% 61.64/8.31 inference(factorization,[],['12'])).
% 61.64/8.31 cnf('14', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(W,V) | ~in(X,X2006) | U = W | W = U | ~hollywood(X2006) | ~city(X2006) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~furniture(V) | ~front(V) | ~fellow(U) | ~fellow(W) | ~man(U) | ~man(W) | ~young(U) | ~young(W)),
% 61.64/8.31 inference(factorization,[],['13'])).
% 61.64/8.31 cnf('15', plain, (barrel($sk6,$sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('16', plain, (~event($sk6) | ~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(resolution,[],['14','15'])).
% 61.64/8.31 cnf('17', plain, (event($sk6) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('18', plain, (~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['16','17'])).
% 61.64/8.31 cnf('19', plain, (~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['18'])).
% 61.64/8.31 cnf('20', plain, (old($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('21', plain, (~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['19','20'])).
% 61.64/8.31 cnf('22', plain, (~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['21'])).
% 61.64/8.31 cnf('23', plain, (car($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('24', plain, (~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['22','23'])).
% 61.64/8.31 cnf('25', plain, (~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['24'])).
% 61.64/8.31 cnf('26', plain, (chevy($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('27', plain, (~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['25','26'])).
% 61.64/8.31 cnf('28', plain, (~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['27'])).
% 61.64/8.31 cnf('29', plain, (white($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('30', plain, (~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['28','29'])).
% 61.64/8.31 cnf('31', plain, (~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['30'])).
% 61.64/8.31 cnf('32', plain, (dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('33', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['31','32'])).
% 61.64/8.31 cnf('34', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['33'])).
% 61.64/8.31 cnf('35', plain, (down($sk6,$sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('36', plain, (~street($sk3) | ~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['34','35'])).
% 61.64/8.31 cnf('37', plain, (~street($sk3) | ~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['36'])).
% 61.64/8.31 cnf('38', plain, (street($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('39', plain, (~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['37','38'])).
% 61.64/8.31 cnf('40', plain, (~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['39'])).
% 61.64/8.31 cnf('41', plain, (lonely($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('42', plain, (~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['40','41'])).
% 61.64/8.31 cnf('43', plain, (~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['42'])).
% 61.64/8.31 cnf('44', plain, (way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('45', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['43','44'])).
% 61.64/8.31 cnf('46', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['45'])).
% 61.64/8.31 cnf('47', plain, (in($sk6,$sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('48', plain, (~hollywood($sk5) | ~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['46','47'])).
% 61.64/8.31 cnf('49', plain, (~hollywood($sk5) | ~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['48'])).
% 61.64/8.31 cnf('50', plain, (hollywood($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('51', plain, (~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['49','50'])).
% 61.64/8.31 cnf('52', plain, (~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['51'])).
% 61.64/8.31 cnf('53', plain, (city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('54', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['52','53'])).
% 61.64/8.31 cnf('55', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['54'])).
% 61.64/8.31 cnf('56', plain, (barrel($sk15,$sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('57', plain, (~car($sk13) | ~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(resolution,[],['14','56'])).
% 61.64/8.31 cnf('58', plain, (car($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('59', plain, (~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['57','58'])).
% 61.64/8.31 cnf('60', plain, (~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['59'])).
% 61.64/8.31 cnf('61', plain, (chevy($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('62', plain, (~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['60','61'])).
% 61.64/8.31 cnf('63', plain, (~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['62'])).
% 61.64/8.31 cnf('64', plain, (white($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('65', plain, (~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['63','64'])).
% 61.64/8.31 cnf('66', plain, (~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['65'])).
% 61.64/8.31 cnf('67', plain, (dirty($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('68', plain, (~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['66','67'])).
% 61.64/8.31 cnf('69', plain, (~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['68'])).
% 61.64/8.31 cnf('70', plain, (event($sk15) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('71', plain, (~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['69','70'])).
% 61.64/8.31 cnf('72', plain, (~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['71'])).
% 61.64/8.31 cnf('73', plain, (old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('74', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | ~in(X2022,X2021) | X2020 = X2022 | X2022 = X2020 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2020) | ~fellow(X2022) | ~man(X2020) | ~man(X2022) | ~young(X2020) | ~young(X2022)),
% 61.64/8.31 inference(resolution,[],['72','73'])).
% 61.64/8.31 cnf('75', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | ~in(X2013,X2012) | X2011 = X2013 | X2013 = X2011 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2011) | ~fellow(X2013) | ~man(X2011) | ~man(X2013) | ~young(X2011) | ~young(X2013)),
% 61.64/8.31 inference(factorization,[],['74'])).
% 61.64/8.31 cnf('76', plain, (down($sk15,$sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('77', plain, (~lonely($sk12) | ~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['75','76'])).
% 61.64/8.31 cnf('78', plain, (~lonely($sk12) | ~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['77'])).
% 61.64/8.31 cnf('79', plain, (lonely($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('80', plain, (~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['78','79'])).
% 61.64/8.31 cnf('81', plain, (~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['80'])).
% 61.64/8.31 cnf('82', plain, (way($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('83', plain, (~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['81','82'])).
% 61.64/8.31 cnf('84', plain, (~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['83'])).
% 61.64/8.31 cnf('85', plain, (street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('86', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | ~in(X2021,X2020) | X2019 = X2021 | X2021 = X2019 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2019) | ~fellow(X2021) | ~man(X2019) | ~man(X2021) | ~young(X2019) | ~young(X2021)),
% 61.64/8.31 inference(resolution,[],['84','85'])).
% 61.64/8.31 cnf('87', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | ~in(X2012,X2011) | X2010 = X2012 | X2012 = X2010 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2010) | ~fellow(X2012) | ~man(X2010) | ~man(X2012) | ~young(X2010) | ~young(X2012)),
% 61.64/8.31 inference(factorization,[],['86'])).
% 61.64/8.31 cnf('88', plain, (in($sk15,$sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('89', plain, (~hollywood($sk14) | ~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['87','88'])).
% 61.64/8.31 cnf('90', plain, (~hollywood($sk14) | ~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['89'])).
% 61.64/8.31 cnf('91', plain, (hollywood($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('92', plain, (~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['90','91'])).
% 61.64/8.31 cnf('93', plain, (~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['92'])).
% 61.64/8.31 cnf('94', plain, (city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('95', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | ~in(X2020,X2019) | X2018 = X2020 | X2020 = X2018 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2018) | ~fellow(X2020) | ~man(X2018) | ~man(X2020) | ~young(X2018) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['93','94'])).
% 61.64/8.31 cnf('96', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['95'])).
% 61.64/8.31 cnf('97', plain, ($df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | ~in(X2011,X2010) | X2009 = X2011 | X2011 = X2009 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2009) | ~fellow(X2011) | ~man(X2009) | ~man(X2011) | ~young(X2009) | ~young(X2011)),
% 61.64/8.31 inference(resolution,[],['96','4'])).
% 61.64/8.31 cnf('98', plain, (~in(X,Y) | ~in(Z,Y) | ~in(U,V) | ~in(W,V) | X = Z | Z = X | U = W | W = U | ~seat(Y) | ~seat(V) | ~furniture(Y) | ~furniture(V) | ~front(Y) | ~front(V) | ~fellow(X) | ~fellow(Z) | ~fellow(U) | ~fellow(W) | ~man(X) | ~man(Z) | ~man(U) | ~man(W) | ~young(X) | ~young(Z) | ~young(U) | ~young(W)),
% 61.64/8.31 inference(resolution,[],['55','97'])).
% 61.64/8.31 cnf('99', plain, (~in(X,Y) | ~in(X,Z) | ~in(U,Y) | ~in(U,Z) | X = U | U = X | ~seat(Y) | ~seat(Z) | ~furniture(Y) | ~furniture(Z) | ~front(Y) | ~front(Z) | ~fellow(X) | ~fellow(U) | ~man(X) | ~man(U) | ~young(X) | ~young(U)),
% 61.64/8.31 inference(factorization,[],['98'])).
% 61.64/8.31 cnf('100', plain, (~in(X,Y) | ~in(Z,Y) | X = Z | Z = X | ~seat(Y) | ~furniture(Y) | ~front(Y) | ~fellow(X) | ~fellow(Z) | ~man(X) | ~man(Z) | ~young(X) | ~young(Z)),
% 61.64/8.31 inference(factorization,[],['99'])).
% 61.64/8.31 cnf('101', plain, ($sk10 = $sk18 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('102', plain, (in($sk18,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('103', plain, (in($sk10,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['101','102'])).
% 61.64/8.31 cnf('104', plain, (in($sk10,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['103'])).
% 61.64/8.31 cnf('105', plain, (~front($sk17) | ~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['100','104'])).
% 61.64/8.31 cnf('106', plain, (front($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('107', plain, (~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['105','106'])).
% 61.64/8.31 cnf('108', plain, (~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['107'])).
% 61.64/8.31 cnf('109', plain, (fellow($sk10) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('110', plain, (~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['108','109'])).
% 61.64/8.31 cnf('111', plain, (~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['110'])).
% 61.64/8.31 cnf('112', plain, (man($sk10) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('113', plain, (~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['111','112'])).
% 61.64/8.31 cnf('114', plain, (~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['113'])).
% 61.64/8.31 cnf('115', plain, (seat($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('116', plain, (~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['114','115'])).
% 61.64/8.31 cnf('117', plain, (~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['116'])).
% 61.64/8.31 cnf('118', plain, (young($sk10) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('119', plain, (~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['117','118'])).
% 61.64/8.31 cnf('120', plain, (~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['119'])).
% 61.64/8.31 cnf('121', plain, (furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('122', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | ~in(X2018,$sk17) | X2018 = $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['120','121'])).
% 61.64/8.31 cnf('123', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | ~in(X2009,$sk17) | X2009 = $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['122'])).
% 61.64/8.31 cnf('124', plain, ($sk11 = $sk16 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('125', plain, (in($sk16,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('126', plain, (in($sk11,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['124','125'])).
% 61.64/8.31 cnf('127', plain, (in($sk11,$sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['126'])).
% 61.64/8.31 cnf('128', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | $sk11 = $sk10 | $sk10 = $sk11 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['123','127'])).
% 61.64/8.31 cnf('129', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | $sk11 = $sk10 | $sk10 = $sk11 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['128'])).
% 61.64/8.31 cnf('130', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,W) | ~barrel(U,X) | ~down(U,Y) | ~in(W,X2007) | ~in(U,Z) | X2006 != W | V != W | V = X2006 | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2007) | ~furniture(X2007) | ~front(X2007) | ~fellow(X2006) | ~fellow(V) | ~man(X2006) | ~man(V) | ~young(X2006) | ~young(V)),
% 61.64/8.31 inference(factorization,[],['1'])).
% 61.64/8.31 cnf('131', plain, (~$df2(X,Y,Z,U,V,V,W,X2006,V) | ~barrel(U,X) | ~down(U,Y) | ~in(V,X2006) | ~in(U,Z) | W != V | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['130'])).
% 61.64/8.31 cnf('132', plain, ($df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~barrel(X2009,X2010) | ~down(X2009,X2011) | ~in(X2012,X2013) | ~in(X2009,X2014) | X2015 != X2012 | X2012 = X2015 | ~hollywood(X2014) | ~city(X2014) | ~event(X2009) | ~chevy(X2010) | ~car(X2010) | ~white(X2010) | ~dirty(X2010) | ~old(X2010) | ~street(X2011) | ~way(X2011) | ~lonely(X2011) | ~seat(X2013) | ~furniture(X2013) | ~front(X2013) | ~fellow(X2015) | ~fellow(X2012) | ~man(X2015) | ~man(X2012) | ~young(X2015) | ~young(X2012)),
% 61.64/8.31 inference(resolution,[],['131','4'])).
% 61.64/8.31 cnf('133', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,W) | ~barrel(U,X) | ~down(U,Y) | ~in(W,X2007) | ~in(U,Z) | X2006 != W | V != W | V = X2006 | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2007) | ~furniture(X2007) | ~front(X2007) | ~fellow(X2006) | ~fellow(V) | ~man(X2006) | ~man(V) | ~young(X2006) | ~young(V)),
% 61.64/8.31 inference(factorization,[],['6'])).
% 61.64/8.31 cnf('134', plain, (~$df1(X,Y,Z,U,V,V,W,X2006,V) | ~barrel(U,X) | ~down(U,Y) | ~in(V,X2006) | ~in(U,Z) | W != V | V = W | ~hollywood(Z) | ~city(Z) | ~event(U) | ~chevy(X) | ~car(X) | ~white(X) | ~dirty(X) | ~old(X) | ~street(Y) | ~way(Y) | ~lonely(Y) | ~seat(X2006) | ~furniture(X2006) | ~front(X2006) | ~fellow(W) | ~fellow(V) | ~man(W) | ~man(V) | ~young(W) | ~young(V)),
% 61.64/8.31 inference(reflexivity,[],['133'])).
% 61.64/8.31 cnf('135', plain, (~barrel(X,Y) | ~barrel(Z,U) | ~down(X,V) | ~down(Z,W) | ~in(X2006,X2007) | ~in(X,X2008) | ~in(X2009,X2010) | ~in(Z,X2011) | X2012 != X2006 | X2013 != X2009 | X2006 = X2012 | X2009 = X2013 | ~hollywood(X2008) | ~hollywood(X2011) | ~city(X2008) | ~city(X2011) | ~event(X) | ~event(Z) | ~chevy(Y) | ~chevy(U) | ~car(Y) | ~car(U) | ~white(Y) | ~white(U) | ~dirty(Y) | ~dirty(U) | ~old(Y) | ~old(U) | ~street(V) | ~street(W) | ~way(V) | ~way(W) | ~lonely(V) | ~lonely(W) | ~seat(X2007) | ~seat(X2010) | ~furniture(X2007) | ~furniture(X2010) | ~front(X2007) | ~front(X2010) | ~fellow(X2012) | ~fellow(X2006) | ~fellow(X2013) | ~fellow(X2009) | ~man(X2012) | ~man(X2006) | ~man(X2013) | ~man(X2009) | ~young(X2012) | ~young(X2006) | ~young(X2013) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['132','134'])).
% 61.64/8.31 cnf('136', plain, (~barrel(X,Y) | ~barrel(Z,U) | ~down(X,V) | ~down(Z,W) | ~in(X2006,X2007) | ~in(X2006,X2008) | ~in(X,X2009) | ~in(Z,X2010) | X2011 != X2006 | X2006 = X2011 | ~hollywood(X2009) | ~hollywood(X2010) | ~city(X2009) | ~city(X2010) | ~event(X) | ~event(Z) | ~chevy(Y) | ~chevy(U) | ~car(Y) | ~car(U) | ~white(Y) | ~white(U) | ~dirty(Y) | ~dirty(U) | ~old(Y) | ~old(U) | ~street(V) | ~street(W) | ~way(V) | ~way(W) | ~lonely(V) | ~lonely(W) | ~seat(X2007) | ~seat(X2008) | ~furniture(X2007) | ~furniture(X2008) | ~front(X2007) | ~front(X2008) | ~fellow(X2011) | ~fellow(X2006) | ~man(X2011) | ~man(X2006) | ~young(X2011) | ~young(X2006)),
% 61.64/8.31 inference(factorization,[],['135'])).
% 61.64/8.31 cnf('137', plain, (~barrel(X,Y) | ~down(X,Z) | ~down(X,U) | ~in(V,W) | ~in(V,X2006) | ~in(X,X2007) | ~in(X,X2008) | X2009 != V | V = X2009 | ~hollywood(X2007) | ~hollywood(X2008) | ~city(X2007) | ~city(X2008) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~street(U) | ~way(Z) | ~way(U) | ~lonely(Z) | ~lonely(U) | ~seat(W) | ~seat(X2006) | ~furniture(W) | ~furniture(X2006) | ~front(W) | ~front(X2006) | ~fellow(X2009) | ~fellow(V) | ~man(X2009) | ~man(V) | ~young(X2009) | ~young(V)),
% 61.64/8.31 inference(factorization,[],['136'])).
% 61.64/8.31 cnf('138', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(U,W) | ~in(X,X2006) | ~in(X,X2007) | X2008 != U | U = X2008 | ~hollywood(X2006) | ~hollywood(X2007) | ~city(X2006) | ~city(X2007) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~seat(W) | ~furniture(V) | ~furniture(W) | ~front(V) | ~front(W) | ~fellow(X2008) | ~fellow(U) | ~man(X2008) | ~man(U) | ~young(X2008) | ~young(U)),
% 61.64/8.31 inference(factorization,[],['137'])).
% 61.64/8.31 cnf('139', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(X,W) | ~in(X,X2006) | X2007 != U | U = X2007 | ~hollywood(W) | ~hollywood(X2006) | ~city(W) | ~city(X2006) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~furniture(V) | ~front(V) | ~fellow(X2007) | ~fellow(U) | ~man(X2007) | ~man(U) | ~young(X2007) | ~young(U)),
% 61.64/8.31 inference(factorization,[],['138'])).
% 61.64/8.31 cnf('140', plain, (~barrel(X,Y) | ~down(X,Z) | ~in(U,V) | ~in(X,W) | X2006 != U | U = X2006 | ~hollywood(W) | ~city(W) | ~event(X) | ~chevy(Y) | ~car(Y) | ~white(Y) | ~dirty(Y) | ~old(Y) | ~street(Z) | ~way(Z) | ~lonely(Z) | ~seat(V) | ~furniture(V) | ~front(V) | ~fellow(X2006) | ~fellow(U) | ~man(X2006) | ~man(U) | ~young(X2006) | ~young(U)),
% 61.64/8.31 inference(factorization,[],['139'])).
% 61.64/8.31 cnf('141', plain, (~event($sk6) | ~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(resolution,[],['140','15'])).
% 61.64/8.31 cnf('142', plain, (~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['141','17'])).
% 61.64/8.31 cnf('143', plain, (~old($sk4) | ~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['142'])).
% 61.64/8.31 cnf('144', plain, (~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['143','20'])).
% 61.64/8.31 cnf('145', plain, (~car($sk4) | ~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['144'])).
% 61.64/8.31 cnf('146', plain, (~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['145','23'])).
% 61.64/8.31 cnf('147', plain, (~chevy($sk4) | ~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['146'])).
% 61.64/8.31 cnf('148', plain, (~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['147','26'])).
% 61.64/8.31 cnf('149', plain, (~white($sk4) | ~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['148'])).
% 61.64/8.31 cnf('150', plain, (~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['149','29'])).
% 61.64/8.31 cnf('151', plain, (~dirty($sk4) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['150'])).
% 61.64/8.31 cnf('152', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk6,X2018) | ~in($sk6,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['151','32'])).
% 61.64/8.31 cnf('153', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk6,X2009) | ~in($sk6,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['152'])).
% 61.64/8.31 cnf('154', plain, (~street($sk3) | ~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['153','35'])).
% 61.64/8.31 cnf('155', plain, (~street($sk3) | ~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['154'])).
% 61.64/8.31 cnf('156', plain, (~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['155','38'])).
% 61.64/8.31 cnf('157', plain, (~lonely($sk3) | ~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['156'])).
% 61.64/8.31 cnf('158', plain, (~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['157','41'])).
% 61.64/8.31 cnf('159', plain, (~way($sk3) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['158'])).
% 61.64/8.31 cnf('160', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk6,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['159','44'])).
% 61.64/8.31 cnf('161', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk6,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['160'])).
% 61.64/8.31 cnf('162', plain, (~hollywood($sk5) | ~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['161','47'])).
% 61.64/8.31 cnf('163', plain, (~hollywood($sk5) | ~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['162'])).
% 61.64/8.31 cnf('164', plain, (~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['163','50'])).
% 61.64/8.31 cnf('165', plain, (~city($sk5) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['164'])).
% 61.64/8.31 cnf('166', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['165','53'])).
% 61.64/8.31 cnf('167', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['166'])).
% 61.64/8.31 cnf('168', plain, (~car($sk13) | ~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(resolution,[],['140','56'])).
% 61.64/8.31 cnf('169', plain, (~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['168','58'])).
% 61.64/8.31 cnf('170', plain, (~chevy($sk13) | ~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['169'])).
% 61.64/8.31 cnf('171', plain, (~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['170','61'])).
% 61.64/8.31 cnf('172', plain, (~white($sk13) | ~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['171'])).
% 61.64/8.31 cnf('173', plain, (~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['172','64'])).
% 61.64/8.31 cnf('174', plain, (~dirty($sk13) | ~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['173'])).
% 61.64/8.31 cnf('175', plain, (~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['174','67'])).
% 61.64/8.31 cnf('176', plain, (~event($sk15) | ~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['175'])).
% 61.64/8.31 cnf('177', plain, (~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['176','70'])).
% 61.64/8.31 cnf('178', plain, (~old($sk13) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['177'])).
% 61.64/8.31 cnf('179', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~down($sk15,X2018) | ~in($sk15,X2019) | ~in(X2020,X2021) | X2022 != X2020 | X2020 = X2022 | ~hollywood(X2019) | ~city(X2019) | ~street(X2018) | ~way(X2018) | ~lonely(X2018) | ~seat(X2021) | ~furniture(X2021) | ~front(X2021) | ~fellow(X2022) | ~fellow(X2020) | ~man(X2022) | ~man(X2020) | ~young(X2022) | ~young(X2020)),
% 61.64/8.31 inference(resolution,[],['178','73'])).
% 61.64/8.31 cnf('180', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~down($sk15,X2009) | ~in($sk15,X2010) | ~in(X2011,X2012) | X2013 != X2011 | X2011 = X2013 | ~hollywood(X2010) | ~city(X2010) | ~street(X2009) | ~way(X2009) | ~lonely(X2009) | ~seat(X2012) | ~furniture(X2012) | ~front(X2012) | ~fellow(X2013) | ~fellow(X2011) | ~man(X2013) | ~man(X2011) | ~young(X2013) | ~young(X2011)),
% 61.64/8.31 inference(factorization,[],['179'])).
% 61.64/8.31 cnf('181', plain, (~lonely($sk12) | ~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['180','76'])).
% 61.64/8.31 cnf('182', plain, (~lonely($sk12) | ~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['181'])).
% 61.64/8.31 cnf('183', plain, (~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['182','79'])).
% 61.64/8.31 cnf('184', plain, (~way($sk12) | ~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['183'])).
% 61.64/8.31 cnf('185', plain, (~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['184','82'])).
% 61.64/8.31 cnf('186', plain, (~street($sk12) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['185'])).
% 61.64/8.31 cnf('187', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in($sk15,X2018) | ~in(X2019,X2020) | X2021 != X2019 | X2019 = X2021 | ~hollywood(X2018) | ~city(X2018) | ~seat(X2020) | ~furniture(X2020) | ~front(X2020) | ~fellow(X2021) | ~fellow(X2019) | ~man(X2021) | ~man(X2019) | ~young(X2021) | ~young(X2019)),
% 61.64/8.31 inference(resolution,[],['186','85'])).
% 61.64/8.31 cnf('188', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in($sk15,X2009) | ~in(X2010,X2011) | X2012 != X2010 | X2010 = X2012 | ~hollywood(X2009) | ~city(X2009) | ~seat(X2011) | ~furniture(X2011) | ~front(X2011) | ~fellow(X2012) | ~fellow(X2010) | ~man(X2012) | ~man(X2010) | ~young(X2012) | ~young(X2010)),
% 61.64/8.31 inference(factorization,[],['187'])).
% 61.64/8.31 cnf('189', plain, (~hollywood($sk14) | ~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['188','88'])).
% 61.64/8.31 cnf('190', plain, (~hollywood($sk14) | ~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['189'])).
% 61.64/8.31 cnf('191', plain, (~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['190','91'])).
% 61.64/8.31 cnf('192', plain, (~city($sk14) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['191'])).
% 61.64/8.31 cnf('193', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | ~in(X2018,X2019) | X2020 != X2018 | X2018 = X2020 | ~seat(X2019) | ~furniture(X2019) | ~front(X2019) | ~fellow(X2020) | ~fellow(X2018) | ~man(X2020) | ~man(X2018) | ~young(X2020) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['192','94'])).
% 61.64/8.31 cnf('194', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['193'])).
% 61.64/8.31 cnf('195', plain, ($df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~in(X2009,X2010) | X2011 != X2009 | X2009 = X2011 | ~seat(X2010) | ~furniture(X2010) | ~front(X2010) | ~fellow(X2011) | ~fellow(X2009) | ~man(X2011) | ~man(X2009) | ~young(X2011) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['194','4'])).
% 61.64/8.31 cnf('196', plain, (~in(X,Y) | ~in(Z,U) | V != X | W != Z | X = V | Z = W | ~seat(Y) | ~seat(U) | ~furniture(Y) | ~furniture(U) | ~front(Y) | ~front(U) | ~fellow(V) | ~fellow(X) | ~fellow(W) | ~fellow(Z) | ~man(V) | ~man(X) | ~man(W) | ~man(Z) | ~young(V) | ~young(X) | ~young(W) | ~young(Z)),
% 61.64/8.31 inference(resolution,[],['167','195'])).
% 61.64/8.31 cnf('197', plain, (~in(X,Y) | ~in(X,Z) | U != X | X = U | ~seat(Y) | ~seat(Z) | ~furniture(Y) | ~furniture(Z) | ~front(Y) | ~front(Z) | ~fellow(U) | ~fellow(X) | ~man(U) | ~man(X) | ~young(U) | ~young(X)),
% 61.64/8.31 inference(factorization,[],['196'])).
% 61.64/8.31 cnf('198', plain, (~in(X,Y) | Z != X | X = Z | ~seat(Y) | ~furniture(Y) | ~front(Y) | ~fellow(Z) | ~fellow(X) | ~man(Z) | ~man(X) | ~young(Z) | ~young(X)),
% 61.64/8.31 inference(factorization,[],['197'])).
% 61.64/8.31 cnf('199', plain, (~front($sk17) | ~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['198','104'])).
% 61.64/8.31 cnf('200', plain, (~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['199','106'])).
% 61.64/8.31 cnf('201', plain, (~fellow($sk10) | ~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['200'])).
% 61.64/8.31 cnf('202', plain, (~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['201','109'])).
% 61.64/8.31 cnf('203', plain, (~man($sk10) | ~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['202'])).
% 61.64/8.31 cnf('204', plain, (~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['203','112'])).
% 61.64/8.31 cnf('205', plain, (~seat($sk17) | ~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['204'])).
% 61.64/8.31 cnf('206', plain, (~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['205','115'])).
% 61.64/8.31 cnf('207', plain, (~young($sk10) | ~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['206'])).
% 61.64/8.31 cnf('208', plain, (~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['207','118'])).
% 61.64/8.31 cnf('209', plain, (~furniture($sk17) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['208'])).
% 61.64/8.31 cnf('210', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk10 = X2018 | X2018 != $sk10 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['209','121'])).
% 61.64/8.31 cnf('211', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk10 = X2009 | X2009 != $sk10 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['210'])).
% 61.64/8.31 cnf('212', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | $sk10 = $sk11 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['129','211'])).
% 61.64/8.31 cnf('213', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | $sk10 = $sk11 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['212'])).
% 61.64/8.31 cnf('214', plain, ($sk11 != $sk10 | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('215', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['213','214'])).
% 61.64/8.31 cnf('216', plain, (~fellow($sk11) | ~man($sk11) | ~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['215'])).
% 61.64/8.31 cnf('217', plain, (fellow($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('218', plain, (~man($sk11) | ~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['216','217'])).
% 61.64/8.31 cnf('219', plain, (~man($sk11) | ~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['218'])).
% 61.64/8.31 cnf('220', plain, (man($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('221', plain, (~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['219','220'])).
% 61.64/8.31 cnf('222', plain, (~young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['221'])).
% 61.64/8.31 cnf('223', plain, (young($sk11) | ~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('224', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df2(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['222','223'])).
% 61.64/8.31 cnf('225', plain, (~$df2(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['224'])).
% 61.64/8.31 cnf('226', plain, ($sk1 = $sk9 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('227', plain, (in($sk9,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('228', plain, (in($sk1,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['226','227'])).
% 61.64/8.31 cnf('229', plain, (in($sk1,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['228'])).
% 61.64/8.31 cnf('230', plain, (~seat($sk8) | ~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['100','229'])).
% 61.64/8.31 cnf('231', plain, (seat($sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('232', plain, (~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['230','231'])).
% 61.64/8.31 cnf('233', plain, (~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['232'])).
% 61.64/8.31 cnf('234', plain, (young($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('235', plain, (~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['233','234'])).
% 61.64/8.31 cnf('236', plain, (~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['235'])).
% 61.64/8.31 cnf('237', plain, (furniture($sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('238', plain, (~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['236','237'])).
% 61.64/8.31 cnf('239', plain, (~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['238'])).
% 61.64/8.31 cnf('240', plain, (front($sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('241', plain, (~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['239','240'])).
% 61.64/8.31 cnf('242', plain, (~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['241'])).
% 61.64/8.31 cnf('243', plain, (fellow($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('244', plain, (~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['242','243'])).
% 61.64/8.31 cnf('245', plain, (~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['244'])).
% 61.64/8.31 cnf('246', plain, (man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('247', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | ~in(X2018,$sk8) | X2018 = $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['245','246'])).
% 61.64/8.31 cnf('248', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | ~in(X2009,$sk8) | X2009 = $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['247'])).
% 61.64/8.31 cnf('249', plain, ($sk2 = $sk7 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('250', plain, (in($sk7,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('251', plain, (in($sk2,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['249','250'])).
% 61.64/8.31 cnf('252', plain, (in($sk2,$sk8) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['251'])).
% 61.64/8.31 cnf('253', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | $sk2 = $sk1 | $sk1 = $sk2 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['248','252'])).
% 61.64/8.31 cnf('254', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | $sk2 = $sk1 | $sk1 = $sk2 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['253'])).
% 61.64/8.31 cnf('255', plain, (~seat($sk8) | ~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(resolution,[],['198','229'])).
% 61.64/8.31 cnf('256', plain, (~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['255','231'])).
% 61.64/8.31 cnf('257', plain, (~young($sk1) | ~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['256'])).
% 61.64/8.31 cnf('258', plain, (~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['257','234'])).
% 61.64/8.31 cnf('259', plain, (~furniture($sk8) | ~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['258'])).
% 61.64/8.31 cnf('260', plain, (~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['259','237'])).
% 61.64/8.31 cnf('261', plain, (~front($sk8) | ~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['260'])).
% 61.64/8.31 cnf('262', plain, (~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['261','240'])).
% 61.64/8.31 cnf('263', plain, (~fellow($sk1) | ~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['262'])).
% 61.64/8.31 cnf('264', plain, (~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['263','243'])).
% 61.64/8.31 cnf('265', plain, (~man($sk1) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['264'])).
% 61.64/8.31 cnf('266', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017) | $sk1 = X2018 | X2018 != $sk1 | ~fellow(X2018) | ~man(X2018) | ~young(X2018)),
% 61.64/8.31 inference(resolution,[],['265','246'])).
% 61.64/8.31 cnf('267', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | $sk1 = X2009 | X2009 != $sk1 | ~fellow(X2009) | ~man(X2009) | ~young(X2009)),
% 61.64/8.31 inference(factorization,[],['266'])).
% 61.64/8.31 cnf('268', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | $sk1 = $sk2 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['254','267'])).
% 61.64/8.31 cnf('269', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | $sk1 = $sk2 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['268'])).
% 61.64/8.31 cnf('270', plain, ($sk2 != $sk1 | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('271', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(paramodulation,[],['269','270'])).
% 61.64/8.31 cnf('272', plain, (~young($sk2) | ~fellow($sk2) | ~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['271'])).
% 61.64/8.31 cnf('273', plain, (young($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('274', plain, (~fellow($sk2) | ~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['272','273'])).
% 61.64/8.31 cnf('275', plain, (~fellow($sk2) | ~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['274'])).
% 61.64/8.31 cnf('276', plain, (fellow($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('277', plain, (~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['275','276'])).
% 61.64/8.31 cnf('278', plain, (~man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(factorization,[],['277'])).
% 61.64/8.31 cnf('279', plain, (man($sk2) | ~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008)),
% 61.64/8.31 inference(cnf_transformation,[],['co1_$sk'])).
% 61.64/8.31 cnf('280', plain, (~$df1(X,Y,Z,U,V,W,X2006,X2007,X2008) | ~$df1(X2009,X2010,X2011,X2012,X2013,X2014,X2015,X2016,X2017)),
% 61.64/8.31 inference(resolution,[],['278','279'])).
% 61.64/8.31 cnf('281', plain, (~$df1(X3,Y3,Z3,U3,V3,W3,X3006,X3007,X3008)),
% 61.64/8.31 inference(factorization,[],['280'])).
% 61.64/8.31 cnf('282', plain, ($false),
% 61.64/8.31 inference(resolution,[then_simplify],['225','4','281'])).
% 61.64/8.31
% 61.64/8.31 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.64/8.31
% 61.64/8.31 run 140 fork 3 statistics:
% 61.64/8.31 ----------------------------------
% 61.64/8.31 this run seconds: 1.101849
% 61.64/8.31 total seconds: 7.434417
% 61.64/8.31 stat_given_used: 1814
% 61.64/8.31 stat_given_used_at_endgame: 0
% 61.64/8.31 stat_given_candidates: 6847
% 61.64/8.31 stat_given_candidates_at_endgame: 0
% 61.64/8.31 stat_given_candidates_h: 0
% 61.64/8.31 stat_binres_derived_cl: 2947
% 61.64/8.31 stat_binres_derived_cl_h: 0
% 61.64/8.31 stat_factor_derived_cl: 12125
% 61.64/8.31 stat_para_derived_cl: 5757
% 61.64/8.31 stat_tautologies_discarded: 705
% 61.64/8.31 stat_forward_subsumed: 59
% 61.64/8.31 stat_derived_cut: 142
% 61.64/8.31 stat_derived_rewritten: 0
% 61.64/8.31 stat_weight_discarded_building: 0
% 61.64/8.31 stat_weight_discarded_cl: 0
% 61.64/8.31 stat_internlimit_discarded_cl: 0
% 61.64/8.31 stat_simplified: 141 simplified 0 derived 0 given
% 61.64/8.31 stat_kept_cl: 15133
% 61.64/8.31 stat_built_cl: 18902
% 61.64/8.31 stat_hyperres_partial_cl: 0
% 61.64/8.31 stat_made_rewriters: 0
% 61.64/8.31 stat_backward_subsumed: 0
% 61.64/8.31 stat_propagated_subsumed: 0
% 61.64/8.31 stat_clsubs_attempted: 234118
% 61.64/8.31 stat_clsubs_fact_groundunit_found: 0
% 61.64/8.31 stat_clsubs_rule_groundunit_found: 0
% 61.64/8.31 stat_clsubs_top_meta_attempted: 5629211
% 61.64/8.31 stat_clsubs_top_meta_failed: 5395093
% 61.64/8.31 stat_clsubs_top_meta_nonpref_attempted: 5629211
% 61.64/8.31 stat_clsubs_top_meta_nonpref_succeeded: 1316153
% 61.64/8.31 stat_clsubs_top_meta_pref_attempted: 1316153
% 61.64/8.31 stat_clsubs_top_meta_pref1_succeeded: 500516
% 61.64/8.31 stat_clsubs_top_meta_pref2_succeeded: 245638
% 61.64/8.31 stat_clsubs_top_meta_pref3_succeeded: 234118
% 61.64/8.31 stat_clsubs_top_meta_pref_succeeded: 234118
% 61.64/8.31 stat_clsubs_meta_attempted: 15581911
% 61.64/8.31 stat_clsubs_meta_failed: 8839706
% 61.64/8.31 stat_clsubs_predsymbs_attempted: 0
% 61.64/8.31 stat_clsubs_unit_attempted: 12
% 61.64/8.31 stat_clsubs_full_attempted: 234106
% 61.64/8.31 stat_forwardsubs_attempted: 15193
% 61.64/8.31 stat_lit_hash_added: 136
% 61.64/8.31 stat_lit_hash_computed: 968544
% 61.64/8.31 stat_lit_hash_match_found: 141
% 61.64/8.31 stat_lit_hash_match_miss: 1566908
% 61.64/8.31 stat_lit_hash_cut_ok: 144
% 61.64/8.31 stat_lit_strong_cut_ok: 0
% 61.64/8.31 stat_lit_hash_subsume_ok: 59
% 61.64/8.31 clqueue els 10000000 used 1
% 61.64/8.31 clactive els 10000000 used 1815
% 61.64/8.31 clactivesubsume els 10000000 used 10885
% 61.64/8.31 queue_termbuf els 200000000 used 4658170
% 61.64/8.31 hyper_termbuf els 100000000 used 1
% 61.64/8.31 active_termbuf els 100000000 used 355715
% 61.64/8.31 varstack els 5000 last used 1
% 61.64/8.31 given_termbuf els 10000000 last used 1
% 61.64/8.31 simplified_termbuf els 10000000 last used 1
% 61.64/8.31 derived_termbuf els 10000000 last used 29
% 61.64/8.31 wr_mallocs: 7175
% 61.64/8.31 wr_callocs: 19
% 61.64/8.31 wr_reallocs: 848
% 61.64/8.31 wr_frees: 4
% 61.64/8.31 wr_malloc_bytes: 4162846772
% 61.64/8.31 wr_calloc_bytes: 96065504
% 61.64/8.31 wr_realloc_bytes: 261736
% 61.64/8.31 wr_realloc_freebytes: 0
% 61.64/8.31 ----------------------------------
%------------------------------------------------------------------------------