%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : LCL672+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:09:10 PM UTC 2026
% Result : Theorem 86.61s 11.95s
% Output : CNFRefutation 86.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL672+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : gkc %s
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 4 20:26:58 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.14/0.43
% 0.14/0.43 input clause set summed statistics:
% 0.14/0.43 ----------------------------------
% 0.14/0.43 in_clause_count: 197
% 0.14/0.43 in_rule_clause_count: 112
% 0.14/0.43 in_fact_clause_count: 85
% 0.14/0.43 in_answer_clause_count: 0
% 0.14/0.43 in_ground_clause_count: 145
% 0.14/0.43 in_unit_clause_count: 146
% 0.14/0.43 in_horn_clause_count: 152
% 0.14/0.43 in_pos_clause_count: 91
% 0.14/0.43 in_neg_clause_count: 55
% 0.14/0.43 in_poseq_clause_count: 0
% 0.14/0.43 in_negeq_clause_count: 0
% 0.14/0.43 in_unitposeq_clause_count: 0
% 0.14/0.43 in_chain_clause_count: 0
% 0.14/0.43 in_min_length: 1
% 0.14/0.43 in_max_length: 30
% 0.14/0.43 in_min_depth: 1
% 0.14/0.43 in_max_depth: 2
% 0.14/0.43 in_min_size: 2
% 0.14/0.43 in_max_size: 91
% 0.14/0.43 in_min_vars: 0
% 0.14/0.43 in_max_vars: 18
% 0.14/0.43 in_extaxiom_count: 0
% 0.14/0.43 in_axiom_count: 2
% 0.14/0.43 in_assumption_count: 0
% 0.14/0.43 in_goal_count: 195
% 0.14/0.43 in_neg_goal_count: 55
% 0.14/0.43 in_pos_goal_count: 90
% 0.14/0.43 in_posunit_goal_count: 90
% 0.14/0.43
% 0.14/0.43 auto guide:
% 0.14/0.43 -----------
% 0.14/0.43 {
% 0.14/0.43 "print":1,
% 0.14/0.43 "print_level": 15,
% 0.14/0.43 "max_size": 0,
% 0.14/0.43 "max_depth": 0,
% 0.14/0.43 "max_length": 0,
% 0.14/0.43 "max_dseconds": 0,
% 0.14/0.43 "equality":0,
% 0.14/0.43 "runs":[
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "depth_penalty":100},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":1, "reverse_clauselist":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "sine":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":2, "sine":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":1, "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "sine":2, "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "max_ground_weight"], "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "weight_select_ratio":100, "repeat_var_weight":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "unit"], "query_preference":1, "sine":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "double"], "query_preference":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":1},
% 0.14/0.43 {"weight_select_ratio":20, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.14/0.43 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.14/0.43 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":1},
% 0.14/0.43 {"sine":2, "var_weight":70, "repeat_var_weight":70, "max_depth":0, "length_penalty":100, "query_preference":2, "strategy":["unit"], "max_dseconds":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus", "positive_pref"], "query_preference":1},
% 0.14/0.43 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":3},
% 0.14/0.43 {"max_dseconds":1, "strategy":["query_focus"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":1, "var_weight":1, "repeat_var_weight":1},
% 0.14/0.43 {"max_dseconds":1, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":1, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.14/0.43 {"weight_select_ratio":100, "length_penalty":100, "query_preference":1, "strategy":["query_focus"], "max_dseconds":1},
% 0.14/0.43
% 0.14/0.43 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "sine":5, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "sine":5, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "sine":5, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":10, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.14/0.43 {"max_dseconds":10, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.14/0.43 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.14/0.43 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":10},
% 0.14/0.43 {"max_dseconds":10, "strategy":["positive_pref"], "query_preference":0},
% 0.14/0.43 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":10},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":10, "strategy":["query_focus"], "query_preference":3},
% 0.14/0.43 {"max_dseconds":10, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":10, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.14/0.43
% 0.14/0.43 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["hardness_pref"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit"], "weight_select_ratio":100, "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "weight_select_ratio":100, "query_preference":0, "var_weight":70, "repeat_var_weight":70},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":50, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.14/0.43 {"max_dseconds":50, "strategy":["hardness_pref"], "query_preference":0, "weight_select_ratio":20, "depth_penalty":50, "length_penalty":100},
% 0.14/0.43 {"length_penalty":100, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.14/0.43 {"strategy":["hardness_pref", "max_weight"], "length_penalty":100, "depth_penalty":50, "max_depth":3, "var_weight":10, "repeat_var_weight":10, "max_dseconds":50},
% 0.14/0.43 {"max_dseconds":50, "strategy":["positive_pref"], "query_preference":0},
% 0.14/0.43 {"var_weight":70, "repeat_var_weight":70, "max_depth":3, "query_preference":0, "strategy":["negative_pref"], "max_dseconds":50},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit", "posunitpara"], "query_preference":0, "sine":2},
% 0.14/0.43 {"max_dseconds":50, "strategy":["query_focus"], "query_preference":3},
% 0.14/0.43 {"max_dseconds":50, "strategy":["negative_pref"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":50, "strategy":["unit"], "query_preference":0, "var_weight":1, "depth_penalty":100, "repeat_var_weight":1},
% 0.14/0.43
% 0.14/0.43 {"max_dseconds":250, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["unit"], "query_preference":0, "weight_select_ratio":100, "depth_penalty":100, "length_penalty":100},
% 0.14/0.43 {"max_dseconds":250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.14/0.43 {"max_dseconds":250, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0},
% 0.14/0.43
% 0.14/0.43 {"max_dseconds":1250, "strategy":["hardness_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["query_focus", "positive_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0, "sine":1},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["negative_pref"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["hardness_pref", "max_ground_weight"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["query_focus", "unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["unit"], "query_preference":0},
% 0.14/0.43 {"max_dseconds":1250, "strategy":["hardness_pref"], "var_weight":70, "repeat_var_weight":70, "query_preference":0}
% 0.14/0.43
% 0.14/0.43 ]}
% 0.14/0.43
% 0.14/0.43
% 0.14/0.43 **** run 1 fork 0 starts with strategy
% 0.14/0.43 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.14/0.43
% 0.14/0.43 **** run 2 fork 1 starts with strategy
% 0.14/0.43 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.14/0.43
% 0.14/0.43 **** run 3 fork 2 starts with strategy
% 0.14/0.43 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.14/0.43
% 0.14/0.43 **** run 4 fork 3 starts with strategy
% 0.14/0.43 {"max_dseconds":1,"sine":5,"strategy":["unit"],"query_preference":0}
% 0.14/0.43
% 0.14/0.43 **** run 5 fork 4 starts with strategy
% 0.14/0.43 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 6 fork 5 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 7 fork 6 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.14/0.44
% 0.14/0.44 **** run 8 fork 7 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.22/0.56
% 0.22/0.56
% 0.22/0.56 fork 5: search terminated without proof.
% 0.22/0.56
% 0.22/0.56
% 0.22/0.56 fork 0: search terminated without proof.
% 0.22/0.56
% 0.22/0.56
% 0.22/0.56 fork 1: search terminated without proof.
% 0.22/0.56
% 0.22/0.56
% 0.22/0.56 fork 2: search terminated without proof.
% 0.22/0.56
% 0.22/0.56
% 0.22/0.56 fork 4: search terminated without proof.
% 0.22/0.57
% 0.22/0.57
% 0.22/0.57 fork 3: search terminated without proof.
% 0.22/0.58
% 0.22/0.58
% 0.22/0.58 fork 6: search terminated without proof.
% 0.22/0.59
% 0.22/0.59 **** run 14 fork 5 starts with strategy
% 0.22/0.59 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 1.47/0.63
% 1.47/0.63
% 1.47/0.63 fork 7: search terminated without proof.
% 1.47/0.63
% 1.47/0.63 **** run 9 fork 0 starts with strategy
% 1.47/0.63 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 1.47/0.64
% 1.47/0.64 **** run 11 fork 2 starts with strategy
% 1.47/0.64 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 1.47/0.64
% 1.47/0.64 **** run 12 fork 3 starts with strategy
% 1.47/0.64 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 1.47/0.64
% 1.47/0.64 **** run 10 fork 1 starts with strategy
% 1.47/0.64 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 1.47/0.64
% 1.47/0.64 **** run 13 fork 4 starts with strategy
% 1.47/0.64 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 1.91/0.69
% 1.91/0.69 **** run 15 fork 6 starts with strategy
% 1.91/0.69 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 1.91/0.70
% 1.91/0.70 **** run 16 fork 7 starts with strategy
% 1.91/0.70 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 2.24/0.71
% 2.24/0.71
% 2.24/0.71 fork 5: search terminated without proof.
% 2.24/0.75
% 2.24/0.75 **** run 22 fork 5 starts with strategy
% 2.24/0.75 {"max_dseconds":1,"strategy":["unit"],"query_preference":2}
% 2.24/0.77
% 2.24/0.77
% 2.24/0.77 fork 3: search terminated without proof.
% 2.24/0.77
% 2.24/0.77
% 2.24/0.77 fork 4: search terminated without proof.
% 2.24/0.77
% 2.24/0.77
% 2.24/0.77 fork 0: search terminated without proof.
% 2.24/0.77
% 2.24/0.77
% 2.24/0.77 fork 1: search terminated without proof.
% 2.24/0.78
% 2.24/0.78
% 2.24/0.78 fork 2: search terminated without proof.
% 2.99/0.83
% 2.99/0.83
% 2.99/0.83 fork 6: search terminated without proof.
% 2.99/0.83
% 2.99/0.83 **** run 20 fork 3 starts with strategy
% 2.99/0.83 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 2.99/0.84
% 2.99/0.84 **** run 18 fork 1 starts with strategy
% 2.99/0.84 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"reverse_clauselist":1}
% 2.99/0.84
% 2.99/0.84 **** run 21 fork 4 starts with strategy
% 2.99/0.84 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 2.99/0.84
% 2.99/0.84 **** run 19 fork 2 starts with strategy
% 2.99/0.84 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":2}
% 2.99/0.84
% 2.99/0.84 **** run 17 fork 0 starts with strategy
% 2.99/0.84 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"depth_penalty":100}
% 2.99/0.84
% 2.99/0.84 fork 7: search finished without proof.
% 3.80/0.90
% 3.80/0.90
% 3.80/0.90 fork 5: search terminated without proof.
% 3.80/0.92
% 3.80/0.92 **** run 24 fork 7 starts with strategy
% 3.80/0.92 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":1}
% 3.80/0.93
% 3.80/0.93 **** run 30 fork 5 starts with strategy
% 3.80/0.93 {"max_dseconds":1,"strategy":["query_focus","max_ground_weight"],"query_preference":1}
% 3.80/0.93
% 3.80/0.93 **** run 23 fork 6 starts with strategy
% 3.80/0.93 {"max_dseconds":1,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 3.80/1.03
% 3.80/1.03
% 3.80/1.03 fork 1: search terminated without proof.
% 3.80/1.03
% 3.80/1.03
% 3.80/1.03 fork 2: search terminated without proof.
% 3.80/1.03
% 3.80/1.03
% 3.80/1.03 fork 4: search terminated without proof.
% 3.80/1.03
% 3.80/1.03
% 3.80/1.03 fork 0: search terminated without proof.
% 4.81/1.05
% 4.81/1.05
% 4.81/1.05 fork 3: search terminated without proof.
% 4.81/1.06
% 4.81/1.06
% 4.81/1.06 fork 5: search terminated without proof.
% 4.81/1.08
% 4.81/1.08 **** run 26 fork 1 starts with strategy
% 4.81/1.08 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":2,"sine":1}
% 4.81/1.08
% 4.81/1.08 **** run 29 fork 4 starts with strategy
% 4.81/1.08 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1}
% 4.81/1.08
% 4.81/1.08 **** run 27 fork 2 starts with strategy
% 4.81/1.08 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":1,"query_preference":1}
% 4.81/1.08
% 4.81/1.08 **** run 25 fork 0 starts with strategy
% 4.81/1.08 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":2}
% 4.81/1.09
% 4.81/1.09 **** run 38 fork 5 starts with strategy
% 4.81/1.09 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 4.81/1.10
% 4.81/1.10 fork 7: search finished without proof.
% 5.54/1.15
% 5.54/1.15
% 5.54/1.15 fork 6: search terminated without proof.
% 5.54/1.16
% 5.54/1.16 **** run 28 fork 3 starts with strategy
% 5.54/1.16 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":2,"query_preference":1}
% 5.97/1.20
% 5.97/1.20 **** run 31 fork 6 starts with strategy
% 5.97/1.20 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 5.97/1.22
% 5.97/1.22
% 5.97/1.22 fork 5: search terminated without proof.
% 5.97/1.22
% 5.97/1.22
% 5.97/1.22 fork 1: search terminated without proof.
% 5.97/1.22
% 5.97/1.22
% 5.97/1.22 fork 2: search terminated without proof.
% 5.97/1.22
% 5.97/1.22
% 5.97/1.22 fork 0: search terminated without proof.
% 5.97/1.23
% 5.97/1.23
% 5.97/1.23 fork 4: search terminated without proof.
% 5.97/1.24
% 5.97/1.24 **** run 46 fork 5 starts with strategy
% 5.97/1.24 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 5.97/1.26
% 5.97/1.26 **** run 32 fork 7 starts with strategy
% 5.97/1.26 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":2}
% 5.97/1.27
% 5.97/1.27 **** run 34 fork 1 starts with strategy
% 5.97/1.27 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 5.97/1.27
% 5.97/1.27 **** run 35 fork 2 starts with strategy
% 5.97/1.27 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 5.97/1.27
% 5.97/1.27 **** run 33 fork 0 starts with strategy
% 5.97/1.27 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1,"sine":1}
% 5.97/1.28
% 5.97/1.28 **** run 37 fork 4 starts with strategy
% 5.97/1.28 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 6.68/1.34
% 6.68/1.34
% 6.68/1.34 fork 6: search terminated without proof.
% 6.68/1.37
% 6.68/1.37
% 6.68/1.37 fork 5: search terminated without proof.
% 6.68/1.39
% 6.68/1.39 **** run 39 fork 6 starts with strategy
% 6.68/1.39 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":1}
% 7.38/1.40
% 7.38/1.40 **** run 54 fork 5 starts with strategy
% 7.38/1.40 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 7.38/1.41
% 7.38/1.41
% 7.38/1.41 fork 1: search terminated without proof.
% 7.38/1.42
% 7.38/1.42
% 7.38/1.42 fork 2: search terminated without proof.
% 7.38/1.42
% 7.38/1.42
% 7.38/1.42 fork 4: search terminated without proof.
% 7.38/1.42
% 7.38/1.42
% 7.38/1.42 fork 0: search terminated without proof.
% 7.38/1.44
% 7.38/1.44
% 7.38/1.44 fork 3: search terminated without proof.
% 7.38/1.46
% 7.38/1.46 **** run 42 fork 1 starts with strategy
% 7.38/1.46 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":1}
% 7.38/1.47
% 7.38/1.47 **** run 43 fork 2 starts with strategy
% 7.38/1.47 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 7.38/1.47
% 7.38/1.47 **** run 45 fork 4 starts with strategy
% 7.38/1.47 {"max_dseconds":1,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 7.38/1.47
% 7.38/1.47 **** run 41 fork 0 starts with strategy
% 7.38/1.47 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 8.06/1.52
% 8.06/1.52
% 8.06/1.52 fork 7: search terminated without proof.
% 8.06/1.53
% 8.06/1.53
% 8.06/1.53 fork 6: search terminated without proof.
% 8.06/1.55
% 8.06/1.55 **** run 36 fork 3 starts with strategy
% 8.06/1.55 {"weight_select_ratio":20,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 8.06/1.58
% 8.06/1.58 **** run 47 fork 6 starts with strategy
% 8.06/1.58 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 8.06/1.59
% 8.06/1.59 **** run 40 fork 7 starts with strategy
% 8.06/1.59 {"sine":2,"var_weight":70,"repeat_var_weight":70,"max_depth":0,"length_penalty":100,"query_preference":2,"strategy":["unit"],"max_dseconds":1}
% 8.06/1.60
% 8.06/1.60
% 8.06/1.60 fork 1: search terminated without proof.
% 8.78/1.61
% 8.78/1.61
% 8.78/1.61 fork 0: search terminated without proof.
% 8.78/1.61
% 8.78/1.61
% 8.78/1.61 fork 2: search terminated without proof.
% 8.78/1.65
% 8.78/1.65 **** run 50 fork 1 starts with strategy
% 8.78/1.65 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 8.78/1.66
% 8.78/1.66 **** run 49 fork 0 starts with strategy
% 8.78/1.66 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 8.78/1.67
% 8.78/1.67 **** run 51 fork 2 starts with strategy
% 8.78/1.67 {"weight_select_ratio":100,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 9.46/1.70
% 9.46/1.70
% 9.46/1.70 fork 4: search terminated without proof.
% 9.46/1.72
% 9.46/1.72
% 9.46/1.72 fork 6: search terminated without proof.
% 9.46/1.73
% 9.46/1.73
% 9.46/1.73 fork 7: search terminated without proof.
% 9.46/1.79
% 9.46/1.79
% 9.46/1.79 fork 1: search terminated without proof.
% 9.46/1.79
% 9.46/1.79 **** run 55 fork 6 starts with strategy
% 9.46/1.79 {"max_dseconds":10,"sine":5,"strategy":["unit"],"query_preference":0}
% 9.46/1.79
% 9.46/1.79 **** run 48 fork 7 starts with strategy
% 9.46/1.79 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 10.18/1.80
% 10.18/1.80
% 10.18/1.80 fork 0: search terminated without proof.
% 10.18/1.80
% 10.18/1.80 **** run 53 fork 4 starts with strategy
% 10.18/1.80 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 10.18/1.81
% 10.18/1.81
% 10.18/1.81 fork 2: search terminated without proof.
% 10.18/1.83
% 10.18/1.83
% 10.18/1.83 fork 3: search terminated without proof.
% 10.18/1.83
% 10.18/1.83 **** run 58 fork 1 starts with strategy
% 10.18/1.83 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 10.18/1.85
% 10.18/1.85 **** run 57 fork 0 starts with strategy
% 10.18/1.85 {"max_dseconds":10,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 10.18/1.86
% 10.18/1.86 **** run 59 fork 2 starts with strategy
% 10.18/1.86 {"max_dseconds":10,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 10.85/1.93
% 10.85/1.93 **** run 44 fork 3 starts with strategy
% 10.85/1.93 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":2}
% 10.85/2.03
% 10.85/2.03
% 10.85/2.03 fork 7: search terminated without proof.
% 12.49/2.13
% 12.49/2.13 **** run 56 fork 7 starts with strategy
% 12.49/2.13 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 12.96/2.22
% 12.96/2.22
% 12.96/2.22 fork 3: search terminated without proof.
% 13.68/2.32
% 13.68/2.32 **** run 52 fork 3 starts with strategy
% 13.68/2.32 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 14.37/2.42
% 14.37/2.42 fork 5: search finished without proof.
% 14.37/2.45
% 14.37/2.45 **** run 62 fork 5 starts with strategy
% 14.37/2.45 {"max_dseconds":10,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 17.31/2.87
% 17.31/2.87 fork 4: search finished without proof.
% 17.31/2.87
% 17.31/2.87
% 17.31/2.87 fork 1: search terminated without proof.
% 17.31/2.90
% 17.31/2.90 fork 0: search finished without proof.
% 17.31/2.90
% 17.31/2.90
% 17.31/2.90 fork 6: search terminated without proof.
% 18.13/2.91
% 18.13/2.91 **** run 61 fork 4 starts with strategy
% 18.13/2.91 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 18.13/2.92
% 18.13/2.92 **** run 66 fork 1 starts with strategy
% 18.13/2.92 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0}
% 18.13/2.93
% 18.13/2.93
% 18.13/2.93 fork 2: search terminated without proof.
% 18.13/2.94
% 18.13/2.94 **** run 65 fork 0 starts with strategy
% 18.13/2.94 {"max_dseconds":10,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 18.13/2.95
% 18.13/2.95 **** run 63 fork 6 starts with strategy
% 18.13/2.95 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 18.13/2.97
% 18.13/2.97 **** run 67 fork 2 starts with strategy
% 18.13/2.97 {"max_dseconds":10,"strategy":["unit"],"query_preference":0}
% 21.90/3.45
% 21.90/3.45 fork 7: search finished without proof.
% 21.90/3.48
% 21.90/3.48
% 21.90/3.48 fork 5: search terminated without proof.
% 21.90/3.50
% 21.90/3.50 **** run 64 fork 7 starts with strategy
% 21.90/3.50 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0}
% 22.75/3.53
% 22.75/3.53 fork 3: search finished without proof.
% 22.75/3.54
% 22.75/3.54 **** run 70 fork 5 starts with strategy
% 22.75/3.54 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 22.75/3.58
% 22.75/3.58 **** run 60 fork 3 starts with strategy
% 22.75/3.58 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 25.91/3.95
% 25.91/3.95 fork 0: search finished without proof.
% 25.91/3.95
% 25.91/3.95
% 25.91/3.95 fork 4: search terminated without proof.
% 25.91/3.96
% 25.91/3.96
% 25.91/3.96 fork 1: search terminated without proof.
% 25.91/4.00
% 25.91/4.00 **** run 73 fork 0 starts with strategy
% 25.91/4.00 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 25.91/4.00
% 25.91/4.00 **** run 69 fork 4 starts with strategy
% 25.91/4.00 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 25.91/4.01
% 25.91/4.01
% 25.91/4.01 fork 2: search terminated without proof.
% 25.91/4.04
% 25.91/4.04 **** run 74 fork 1 starts with strategy
% 25.91/4.04 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"sine":2}
% 25.91/4.04
% 25.91/4.04 fork 6: search finished without proof.
% 25.91/4.06
% 25.91/4.06 **** run 75 fork 2 starts with strategy
% 25.91/4.06 {"max_dseconds":10,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 27.17/4.07
% 27.17/4.07 **** run 71 fork 6 starts with strategy
% 27.17/4.07 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":10}
% 30.54/4.58
% 30.54/4.58 fork 7: search finished without proof.
% 31.33/4.62
% 31.33/4.62
% 31.33/4.62 fork 3: search terminated without proof.
% 31.33/4.63
% 31.33/4.63 **** run 72 fork 7 starts with strategy
% 31.33/4.63 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 31.33/4.67
% 31.33/4.67 **** run 68 fork 3 starts with strategy
% 31.33/4.67 {"max_dseconds":10,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 31.33/4.68
% 31.33/4.68
% 31.33/4.68 fork 5: search terminated without proof.
% 32.13/4.73
% 32.13/4.73 **** run 78 fork 5 starts with strategy
% 32.13/4.73 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 34.76/5.04
% 34.76/5.04
% 34.76/5.04 fork 0: search terminated without proof.
% 34.76/5.09
% 34.76/5.09
% 34.76/5.09 fork 1: search terminated without proof.
% 34.76/5.09
% 34.76/5.09
% 34.76/5.09 fork 4: search terminated without proof.
% 34.76/5.10
% 34.76/5.10
% 34.76/5.10 fork 2: search terminated without proof.
% 34.76/5.11
% 34.76/5.11
% 34.76/5.11 fork 6: search terminated without proof.
% 34.76/5.11
% 34.76/5.11 **** run 81 fork 0 starts with strategy
% 34.76/5.11 {"max_dseconds":50,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 34.76/5.13
% 34.76/5.13 **** run 82 fork 1 starts with strategy
% 34.76/5.13 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 35.50/5.14
% 35.50/5.14 **** run 79 fork 6 starts with strategy
% 35.50/5.14 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0}
% 35.50/5.15
% 35.50/5.15 **** run 83 fork 2 starts with strategy
% 35.50/5.15 {"max_dseconds":50,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 35.50/5.18
% 35.50/5.18 **** run 77 fork 4 starts with strategy
% 35.50/5.18 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 39.46/5.71
% 39.46/5.71
% 39.46/5.71 fork 3: search terminated without proof.
% 39.46/5.75
% 39.46/5.75 **** run 76 fork 3 starts with strategy
% 39.46/5.75 {"max_dseconds":10,"strategy":["query_focus"],"query_preference":3}
% 40.15/5.80
% 40.15/5.80
% 40.15/5.80 fork 7: search terminated without proof.
% 40.15/5.87
% 40.15/5.87 **** run 80 fork 7 starts with strategy
% 40.15/5.87 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 41.76/6.12
% 41.76/6.12 fork 5: search finished without proof.
% 42.49/6.14
% 42.49/6.14 **** run 86 fork 5 starts with strategy
% 42.49/6.14 {"max_dseconds":50,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 43.74/6.36
% 43.74/6.36
% 43.74/6.36 fork 4: search terminated without proof.
% 44.53/6.41
% 44.53/6.41 **** run 85 fork 4 starts with strategy
% 44.53/6.41 {"max_dseconds":50,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 46.91/6.79
% 46.91/6.79 fork 3: search finished without proof.
% 47.70/6.84
% 47.70/6.84 **** run 84 fork 3 starts with strategy
% 47.70/6.84 {"max_dseconds":50,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 75.51/10.48
% 75.51/10.48
% 75.51/10.48 fork 6: search terminated without proof.
% 76.31/10.50
% 76.31/10.50
% 76.31/10.50 fork 1: search terminated without proof.
% 76.31/10.53
% 76.31/10.53
% 76.31/10.53 fork 0: search terminated without proof.
% 76.31/10.54
% 76.31/10.54 **** run 87 fork 6 starts with strategy
% 76.31/10.54 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 76.31/10.55
% 76.31/10.55 **** run 90 fork 1 starts with strategy
% 76.31/10.55 {"max_dseconds":50,"strategy":["query_focus","unit"],"query_preference":0}
% 76.31/10.59
% 76.31/10.59 **** run 89 fork 0 starts with strategy
% 76.31/10.59 {"max_dseconds":50,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 77.12/10.66
% 77.12/10.66
% 77.12/10.66 fork 2: search terminated without proof.
% 77.91/10.72
% 77.91/10.72 **** run 91 fork 2 starts with strategy
% 77.91/10.72 {"max_dseconds":50,"strategy":["unit"],"query_preference":0}
% 79.51/10.90
% 79.51/10.90
% 79.51/10.90 fork 7: search terminated without proof.
% 79.51/10.95
% 79.51/10.95 **** run 88 fork 7 starts with strategy
% 79.51/10.95 {"max_dseconds":50,"strategy":["negative_pref"],"query_preference":0}
% 81.31/11.19
% 81.31/11.19
% 81.31/11.19 fork 5: search terminated without proof.
% 81.70/11.23
% 81.70/11.23 **** run 94 fork 5 starts with strategy
% 81.70/11.23 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":50}
% 83.10/11.45
% 83.10/11.45
% 83.10/11.45 fork 4: search terminated without proof.
% 83.80/11.50
% 83.80/11.50 **** run 93 fork 4 starts with strategy
% 83.80/11.50 {"max_dseconds":50,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 85.89/11.88
% 85.89/11.88
% 85.89/11.88 fork 3: search terminated without proof.
% 86.61/11.92
% 86.61/11.92 **** run 92 fork 3 starts with strategy
% 86.61/11.92 {"max_dseconds":50,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 86.61/11.95
% 86.61/11.95
% 86.61/11.95 result: proof found
% 86.61/11.95 for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 86.61/11.95 by run 89 fork 0 strategy {"max_dseconds":50,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 86.61/11.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 86.61/11.95
% 86.61/11.95 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 86.61/11.95 fof('main_$sk', plain, ((~p1($sk2) & r1($sk1,$sk2)) & (((~p1($sk4) & r1($sk3,$sk4)) & (((~p1($sk6) & r1($sk5,$sk6)) & (((~p1($sk8) & r1($sk7,$sk8)) & (((~p1($sk10) & r1($sk9,$sk10)) & (((~p1($sk12) & r1($sk11,$sk12)) & (((p1(X1) | ~r1($sk13,X1)) & r1($sk11,$sk13)) & r1($sk9,$sk11))) & ((~p2($sk14) & r1($sk9,$sk14)) & r1($sk7,$sk9)))) & ((~p2($sk15) & r1($sk7,$sk15)) & r1($sk5,$sk7)))) & ((~p2($sk16) & r1($sk5,$sk16)) & r1($sk3,$sk5)))) & ((~p2($sk17) & r1($sk3,$sk17)) & r1($sk1,$sk3)))) & ((~p2($sk18) & r1($sk1,$sk18)) & (((p1(X2) | ~r1($sk1,X2)) | (((~$false & r1(X3,$sk19(X3))) | ~r1($sk1,X3)) | (p2(X4) | ~r1($sk1,X4)))) & (((p1(X5) | ~r1($sk1,X5)) | (((((~p1($sk20(X6,X7)) & r1(X7,$sk20(X6,X7))) | ~r1(X6,X7)) | (((p1(X9) | ~r1($sk21(X6,X8),X9)) & r1(X8,$sk21(X6,X8))) | ~r1(X6,X8))) | ~r1($sk1,X6)) | (p2(X10) | ~r1($sk1,X10)))) & (((p1(X11) | ~r1($sk1,X11)) | (((((p1(X14) | ~r1(X13,X14)) | ((~p1($sk22(X12,X13,X15)) & r1(X15,$sk22(X12,X13,X15))) | ~r1(X13,X15))) | ~r1(X12,X13)) | ~r1($sk1,X12)) | (p2(X16) | ~r1($sk1,X16)))) & (((p1(X17) | ~r1($sk1,X17)) | (((~p1(X18) | ((p1($sk23(X18,X19)) & r1(X19,$sk23(X18,X19))) | ~r1(X18,X19))) | ~r1($sk1,X18)) | (p2(X20) | ~r1($sk1,X20)))) & ((~p1($sk24) & r1($sk1,$sk24)) & (((~p1($sk26) & r1($sk25,$sk26)) & (((~p1($sk28) & r1($sk27,$sk28)) & (((~p1($sk30) & r1($sk29,$sk30)) & (((~p1($sk32) & r1($sk31,$sk32)) & (((~p1($sk34) & r1($sk33,$sk34)) & (((p1(X21) | ~r1($sk35,X21)) & r1($sk33,$sk35)) & r1($sk31,$sk33))) & ((~p2($sk36) & r1($sk31,$sk36)) & r1($sk29,$sk31)))) & ((~p2($sk37) & r1($sk29,$sk37)) & r1($sk27,$sk29)))) & ((~p2($sk38) & r1($sk27,$sk38)) & r1($sk25,$sk27)))) & ((~p2($sk39) & r1($sk25,$sk39)) & r1($sk1,$sk25)))) & ((~p2($sk40) & r1($sk1,$sk40)) & (((p1(X22) | ~r1($sk1,X22)) | ((((p1(X24) | ~r1(X23,X24)) | (((~$false & r1(X25,$sk41(X23,X25))) | ~r1(X23,X25)) | (p2(X26) | ~r1(X23,X26)))) | ~r1($sk1,X23)) | (p2(X27) | ~r1($sk1,X27)))) & (((p1(X28) | ~r1($sk1,X28)) | ((((p1(X30) | ~r1(X29,X30)) | (((((~p1($sk42(X29,X31,X32)) & r1(X32,$sk42(X29,X31,X32))) | ~r1(X31,X32)) | (((p1(X34) | ~r1($sk43(X29,X31,X33),X34)) & r1(X33,$sk43(X29,X31,X33))) | ~r1(X31,X33))) | ~r1(X29,X31)) | (p2(X35) | ~r1(X29,X35)))) | ~r1($sk1,X29)) | (p2(X36) | ~r1($sk1,X36)))) & (((p1(X37) | ~r1($sk1,X37)) | ((((p1(X39) | ~r1(X38,X39)) | (((((p1(X42) | ~r1(X41,X42)) | ((~p1($sk44(X38,X40,X41,X43)) & r1(X43,$sk44(X38,X40,X41,X43))) | ~r1(X41,X43))) | ~r1(X40,X41)) | ~r1(X38,X40)) | (p2(X44) | ~r1(X38,X44)))) | ~r1($sk1,X38)) | (p2(X45) | ~r1($sk1,X45)))) & (((p1(X46) | ~r1($sk1,X46)) | ((((p1(X48) | ~r1(X47,X48)) | (((~p1(X49) | ((p1($sk45(X47,X49,X50)) & r1(X50,$sk45(X47,X49,X50))) | ~r1(X49,X50))) | ~r1(X47,X49)) | (p2(X51) | ~r1(X47,X51)))) | ~r1($sk1,X47)) | (p2(X52) | ~r1($sk1,X52)))) & ((~p1($sk46) & r1($sk1,$sk46)) & (((~p1($sk48) & r1($sk47,$sk48)) & (((~p1($sk50) & r1($sk49,$sk50)) & (((~p1($sk52) & r1($sk51,$sk52)) & (((~p1($sk54) & r1($sk53,$sk54)) & (((~p1($sk56) & r1($sk55,$sk56)) & (((p1(X53) | ~r1($sk57,X53)) & r1($sk55,$sk57)) & r1($sk53,$sk55))) & ((~p2($sk58) & r1($sk53,$sk58)) & r1($sk51,$sk53)))) & ((~p2($sk59) & r1($sk51,$sk59)) & r1($sk49,$sk51)))) & ((~p2($sk60) & r1($sk49,$sk60)) & r1($sk47,$sk49)))) & ((~p2($sk61) & r1($sk47,$sk61)) & r1($sk1,$sk47)))) & ((~p2($sk62) & r1($sk1,$sk62)) & (((p1(X54) | ~r1($sk1,X54)) | ((((p1(X56) | ~r1(X55,X56)) | ((((p1(X58) | ~r1(X57,X58)) | (((~$false & r1(X59,$sk63(X55,X57,X59))) | ~r1(X57,X59)) | (p2(X60) | ~r1(X57,X60)))) | ~r1(X55,X57)) | (p2(X61) | ~r1(X55,X61)))) | ~r1($sk1,X55)) | (p2(X62) | ~r1($sk1,X62)))) & (((p1(X63) | ~r1($sk1,X63)) | ((((p1(X65) | ~r1(X64,X65)) | ((((p1(X67) | ~r1(X66,X67)) | (((((~p1($sk64(X64,X66,X68,X69)) & r1(X69,$sk64(X64,X66,X68,X69))) | ~r1(X68,X69)) | (((p1(X71) | ~r1($sk65(X64,X66,X68,X70),X71)) & r1(X70,$sk65(X64,X66,X68,X70))) | ~r1(X68,X70))) | ~r1(X66,X68)) | (p2(X72) | ~r1(X66,X72)))) | ~r1(X64,X66)) | (p2(X73) | ~r1(X64,X73)))) | ~r1($sk1,X64)) | (p2(X74) | ~r1($sk1,X74)))) & (((p1(X75) | ~r1($sk1,X75)) | ((((p1(X77) | ~r1(X76,X77)) | ((((p1(X79) | ~r1(X78,X79)) | (((((p1(X82) | ~r1(X81,X82)) | ((~p1($sk66(X76,X78,X80,X81,X83)) & r1(X83,$sk66(X76,X78,X80,X81,X83))) | ~r1(X81,X83))) | ~r1(X80,X81)) | ~r1(X78,X80)) | (p2(X84) | ~r1(X78,X84)))) | ~r1(X76,X78)) | (p2(X85) | ~r1(X76,X85)))) | ~r1($sk1,X76)) | (p2(X86) | ~r1($sk1,X86)))) & (((p1(X87) | ~r1($sk1,X87)) | ((((p1(X89) | ~r1(X88,X89)) | ((((p1(X91) | ~r1(X90,X91)) | (((~p1(X92) | ((p1($sk67(X88,X90,X92,X93)) & r1(X93,$sk67(X88,X90,X92,X93))) | ~r1(X92,X93))) | ~r1(X90,X92)) | (p2(X94) | ~r1(X90,X94)))) | ~r1(X88,X90)) | (p2(X95) | ~r1(X88,X95)))) | ~r1($sk1,X88)) | (p2(X96) | ~r1($sk1,X96)))) & ((~p1($sk68) & r1($sk1,$sk68)) & (((~p1($sk70) & r1($sk69,$sk70)) & (((~p1($sk72) & r1($sk71,$sk72)) & (((~p1($sk74) & r1($sk73,$sk74)) & (((~p1($sk76) & r1($sk75,$sk76)) & (((~p1($sk78) & r1($sk77,$sk78)) & (((p1(X97) | ~r1($sk79,X97)) & r1($sk77,$sk79)) & r1($sk75,$sk77))) & ((~p2($sk80) & r1($sk75,$sk80)) & r1($sk73,$sk75)))) & ((~p2($sk81) & r1($sk73,$sk81)) & r1($sk71,$sk73)))) & ((~p2($sk82) & r1($sk71,$sk82)) & r1($sk69,$sk71)))) & ((~p2($sk83) & r1($sk69,$sk83)) & r1($sk1,$sk69)))) & ((~p2($sk84) & r1($sk1,$sk84)) & (((p1(X98) | ~r1($sk1,X98)) | ((((p1(X100) | ~r1(X99,X100)) | ((((p1(X102) | ~r1(X101,X102)) | ((((p1(X104) | ~r1(X103,X104)) | (((~$false & r1(X105,$sk85(X99,X101,X103,X105))) | ~r1(X103,X105)) | (p2(X106) | ~r1(X103,X106)))) | ~r1(X101,X103)) | (p2(X107) | ~r1(X101,X107)))) | ~r1(X99,X101)) | (p2(X108) | ~r1(X99,X108)))) | ~r1($sk1,X99)) | (p2(X109) | ~r1($sk1,X109)))) & (((p1(X110) | ~r1($sk1,X110)) | ((((p1(X112) | ~r1(X111,X112)) | ((((p1(X114) | ~r1(X113,X114)) | ((((p1(X116) | ~r1(X115,X116)) | (((((~p1($sk86(X111,X113,X115,X117,X118)) & r1(X118,$sk86(X111,X113,X115,X117,X118))) | ~r1(X117,X118)) | (((p1(X120) | ~r1($sk87(X111,X113,X115,X117,X119),X120)) & r1(X119,$sk87(X111,X113,X115,X117,X119))) | ~r1(X117,X119))) | ~r1(X115,X117)) | (p2(X121) | ~r1(X115,X121)))) | ~r1(X113,X115)) | (p2(X122) | ~r1(X113,X122)))) | ~r1(X111,X113)) | (p2(X123) | ~r1(X111,X123)))) | ~r1($sk1,X111)) | (p2(X124) | ~r1($sk1,X124)))) & (((p1(X125) | ~r1($sk1,X125)) | ((((p1(X127) | ~r1(X126,X127)) | ((((p1(X129) | ~r1(X128,X129)) | ((((p1(X131) | ~r1(X130,X131)) | (((((p1(X134) | ~r1(X133,X134)) | ((~p1($sk88(X126,X128,X130,X132,X133,X135)) & r1(X135,$sk88(X126,X128,X130,X132,X133,X135))) | ~r1(X133,X135))) | ~r1(X132,X133)) | ~r1(X130,X132)) | (p2(X136) | ~r1(X130,X136)))) | ~r1(X128,X130)) | (p2(X137) | ~r1(X128,X137)))) | ~r1(X126,X128)) | (p2(X138) | ~r1(X126,X138)))) | ~r1($sk1,X126)) | (p2(X139) | ~r1($sk1,X139)))) & (((p1(X140) | ~r1($sk1,X140)) | ((((p1(X142) | ~r1(X141,X142)) | ((((p1(X144) | ~r1(X143,X144)) | ((((p1(X146) | ~r1(X145,X146)) | (((~p1(X147) | ((p1($sk89(X141,X143,X145,X147,X148)) & r1(X148,$sk89(X141,X143,X145,X147,X148))) | ~r1(X147,X148))) | ~r1(X145,X147)) | (p2(X149) | ~r1(X145,X149)))) | ~r1(X143,X145)) | (p2(X150) | ~r1(X143,X150)))) | ~r1(X141,X143)) | (p2(X151) | ~r1(X141,X151)))) | ~r1($sk1,X141)) | (p2(X152) | ~r1($sk1,X152)))) & ((~p1($sk90) & r1($sk1,$sk90)) & (((~p1($sk92) & r1($sk91,$sk92)) & (((~p1($sk94) & r1($sk93,$sk94)) & (((~p1($sk96) & r1($sk95,$sk96)) & (((~p1($sk98) & r1($sk97,$sk98)) & (((~p1($sk100) & r1($sk99,$sk100)) & (((p1(X153) | ~r1($sk101,X153)) & r1($sk99,$sk101)) & r1($sk97,$sk99))) & ((~p2($sk102) & r1($sk97,$sk102)) & r1($sk95,$sk97)))) & ((~p2($sk103) & r1($sk95,$sk103)) & r1($sk93,$sk95)))) & ((~p2($sk104) & r1($sk93,$sk104)) & r1($sk91,$sk93)))) & ((~p2($sk105) & r1($sk91,$sk105)) & r1($sk1,$sk91)))) & ((~p2($sk106) & r1($sk1,$sk106)) & (((p1(X154) | ~r1($sk1,X154)) | ((((p1(X156) | ~r1(X155,X156)) | ((((p1(X158) | ~r1(X157,X158)) | ((((p1(X160) | ~r1(X159,X160)) | ((((p1(X162) | ~r1(X161,X162)) | (((~$false & r1(X163,$sk107(X155,X157,X159,X161,X163))) | ~r1(X161,X163)) | (p2(X164) | ~r1(X161,X164)))) | ~r1(X159,X161)) | (p2(X165) | ~r1(X159,X165)))) | ~r1(X157,X159)) | (p2(X166) | ~r1(X157,X166)))) | ~r1(X155,X157)) | (p2(X167) | ~r1(X155,X167)))) | ~r1($sk1,X155)) | (p2(X168) | ~r1($sk1,X168)))) & (((p1(X169) | ~r1($sk1,X169)) | ((((p1(X171) | ~r1(X170,X171)) | ((((p1(X173) | ~r1(X172,X173)) | ((((p1(X175) | ~r1(X174,X175)) | ((((p1(X177) | ~r1(X176,X177)) | (((((~p1($sk108(X170,X172,X174,X176,X178,X179)) & r1(X179,$sk108(X170,X172,X174,X176,X178,X179))) | ~r1(X178,X179)) | (((p1(X181) | ~r1($sk109(X170,X172,X174,X176,X178,X180),X181)) & r1(X180,$sk109(X170,X172,X174,X176,X178,X180))) | ~r1(X178,X180))) | ~r1(X176,X178)) | (p2(X182) | ~r1(X176,X182)))) | ~r1(X174,X176)) | (p2(X183) | ~r1(X174,X183)))) | ~r1(X172,X174)) | (p2(X184) | ~r1(X172,X184)))) | ~r1(X170,X172)) | (p2(X185) | ~r1(X170,X185)))) | ~r1($sk1,X170)) | (p2(X186) | ~r1($sk1,X186)))) & (((p1(X187) | ~r1($sk1,X187)) | ((((p1(X189) | ~r1(X188,X189)) | ((((p1(X191) | ~r1(X190,X191)) | ((((p1(X193) | ~r1(X192,X193)) | ((((p1(X195) | ~r1(X194,X195)) | (((((p1(X198) | ~r1(X197,X198)) | ((~p1($sk110(X188,X190,X192,X194,X196,X197,X199)) & r1(X199,$sk110(X188,X190,X192,X194,X196,X197,X199))) | ~r1(X197,X199))) | ~r1(X196,X197)) | ~r1(X194,X196)) | (p2(X200) | ~r1(X194,X200)))) | ~r1(X192,X194)) | (p2(X201) | ~r1(X192,X201)))) | ~r1(X190,X192)) | (p2(X202) | ~r1(X190,X202)))) | ~r1(X188,X190)) | (p2(X203) | ~r1(X188,X203)))) | ~r1($sk1,X188)) | (p2(X204) | ~r1($sk1,X204)))) & ((p1(X205) | ~r1($sk1,X205)) | ((((p1(X207) | ~r1(X206,X207)) | ((((p1(X209) | ~r1(X208,X209)) | ((((p1(X211) | ~r1(X210,X211)) | ((((p1(X213) | ~r1(X212,X213)) | (((~p1(X214) | ((p1($sk111(X206,X208,X210,X212,X214,X215)) & r1(X215,$sk111(X206,X208,X210,X212,X214,X215))) | ~r1(X214,X215))) | ~r1(X212,X214)) | (p2(X216) | ~r1(X212,X216)))) | ~r1(X210,X212)) | (p2(X217) | ~r1(X210,X217)))) | ~r1(X208,X210)) | (p2(X218) | ~r1(X208,X218)))) | ~r1(X206,X208)) | (p2(X219) | ~r1(X206,X219)))) | ~r1($sk1,X206)) | (p2(X220) | ~r1($sk1,X220)))))))))))))))))))))))))))))))))))))),
% 86.61/11.95 inference(negpush_and_skolemize,[],['main'])).
% 86.61/11.95 fof('main', conjecture, ~(? [X] : ~((((((((((((((((((((((((((((((((((((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~p1(Y))))) & p1(Y))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y)))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | $false))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : ((~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | ~p1(X))))) & p1(X))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | $false))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : ((~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~p1(Y))))) & p1(Y))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | $false))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : ((~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | ~p1(X))))) & p1(X))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))))) & ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~((~(! [X] : (~r1(Y,X) | p2(X))) & ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | $false))))) & ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : ((~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~p1(Y))))) & p1(Y))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | p1(X))))))) & ~(! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y))))))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | ((~(! [Y] : (~r1(X,Y) | p2(Y))) & ~(! [Y] : (~r1(X,Y) | ~(! [X] : (~r1(Y,X) | $false))))) & ~(! [Y] : (~r1(X,Y) | p1(Y))))) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : (((~r1(X,Y) | (! [X] : (~r1(Y,X) | p2(X)))) | (! [X] : (((~r1(Y,X) | (! [Y] : (~r1(X,Y) | p2(Y)))) | (! [Y] : ((~r1(X,Y) | (! [X] : (~r1(Y,X) | ~(! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y)))))) | (! [X] : (~r1(Y,X) | p1(X)))))) | (! [Y] : (~r1(X,Y) | p1(Y))))),
% 86.61/11.95 input).
% 86.61/11.95 fof('transitivity_$sk', plain, (r1(X3,X2) | (~r1(X1,X2) | ~r1(X3,X1))),
% 86.61/11.95 inference(negpush_and_skolemize,[],['transitivity'])).
% 86.61/11.95 fof('transitivity', axiom, (! [X,Y,Z] : ((r1(X,Y) & r1(Y,Z)) => r1(X,Z))),
% 86.61/11.95 input).
% 86.61/11.95 fof('reflexivity_$sk', plain, r1(X1,X1),
% 86.61/11.95 inference(negpush_and_skolemize,[],['reflexivity'])).
% 86.61/11.95 fof('reflexivity', axiom, (! [X] : r1(X,X)),
% 86.61/11.95 input).
% 86.61/11.95 cnf('1', plain, (r1(X,$sk22(Y,Z,X)) | ~r1($sk1,U) | ~r1($sk1,V) | ~r1($sk1,Y) | ~r1(Z,W) | ~r1(Z,X) | ~r1(Y,Z) | p2(V) | p1(U) | p1(W)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('2', plain, (~r1($sk57,X) | p1(X)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('3', plain, (p1($sk22(X,Y,$sk57)) | ~r1($sk1,X) | ~r1($sk1,Z) | ~r1($sk1,U) | ~r1(Y,$sk57) | ~r1(Y,V) | ~r1(X,Y) | p2(Z) | p1(V) | p1(U)),
% 86.61/11.95 inference(resolution,[],['1','2'])).
% 86.61/11.95 cnf('4', plain, (~p1($sk22(X,Y,Z)) | ~r1($sk1,U) | ~r1($sk1,V) | ~r1($sk1,X) | ~r1(Y,W) | ~r1(Y,Z) | ~r1(X,Y) | p2(V) | p1(U) | p1(W)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('5', plain, (~p1($sk22(X,Y,Z)) | ~r1($sk1,U) | ~r1($sk1,V) | ~r1($sk1,X) | ~r1(Y,V) | ~r1(Y,Z) | ~r1(X,Y) | p2(U) | p1(V)),
% 86.61/11.95 inference(factorization,[],['4'])).
% 86.61/11.95 cnf('6', plain, (~r1($sk1,X) | ~r1($sk1,Y) | ~r1($sk1,Z) | ~r1($sk1,U) | ~r1($sk1,V) | ~r1(W,$sk57) | ~r1(W,X) | ~r1(W,X2006) | ~r1(V,W) | p2(Y) | p2(U) | p1(X) | p1(X2006) | p1(Z)),
% 86.61/11.95 inference(resolution,[],['3','5'])).
% 86.61/11.95 cnf('7', plain, (~r1($sk1,X) | ~r1($sk1,Y) | ~r1($sk1,Z) | ~r1($sk1,U) | ~r1(V,$sk57) | ~r1(V,W) | ~r1(V,Z) | ~r1(X,V) | p2(Y) | p2(U) | p1(W) | p1(Z)),
% 86.61/11.95 inference(factorization,[],['6'])).
% 86.61/11.95 cnf('8', plain, (~r1($sk1,X) | ~r1($sk1,Y) | ~r1($sk1,Z) | ~r1(U,$sk57) | ~r1(U,V) | ~r1(U,Y) | ~r1(Z,U) | p2(X) | p1(V) | p1(Y)),
% 86.61/11.95 inference(factorization,[],['7'])).
% 86.61/11.95 cnf('9', plain, (~r1(X,Y) | ~r1(Z,X) | r1(Z,Y)),
% 86.61/11.95 inference(cnf_transformation,[],['transitivity_$sk'])).
% 86.61/11.95 cnf('10', plain, (r1($sk55,$sk57)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('11', plain, (~r1(X,$sk55) | r1(X,$sk57)),
% 86.61/11.95 inference(resolution,[],['9','10'])).
% 86.61/11.95 cnf('12', plain, (r1($sk53,$sk55)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('13', plain, (r1($sk53,$sk57)),
% 86.61/11.95 inference(resolution,[],['11','12'])).
% 86.61/11.95 cnf('14', plain, (~r1(X,$sk53) | r1(X,$sk57)),
% 86.61/11.95 inference(resolution,[],['13','9'])).
% 86.61/11.95 cnf('15', plain, (r1($sk51,$sk53)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('16', plain, (~r1(X,$sk51) | r1(X,$sk53)),
% 86.61/11.95 inference(resolution,[],['9','15'])).
% 86.61/11.95 cnf('17', plain, (r1($sk49,$sk51)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('18', plain, (r1($sk49,$sk53)),
% 86.61/11.95 inference(resolution,[],['16','17'])).
% 86.61/11.95 cnf('19', plain, (r1($sk49,$sk57)),
% 86.61/11.95 inference(resolution,[],['14','18'])).
% 86.61/11.95 cnf('20', plain, (~r1(X,$sk49) | r1(X,$sk57)),
% 86.61/11.95 inference(resolution,[],['19','9'])).
% 86.61/11.95 cnf('21', plain, (r1($sk47,$sk49)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('22', plain, (~r1(X,$sk47) | r1(X,$sk49)),
% 86.61/11.95 inference(resolution,[],['9','21'])).
% 86.61/11.95 cnf('23', plain, (r1($sk1,$sk47)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('24', plain, (r1($sk1,$sk49)),
% 86.61/11.95 inference(resolution,[],['22','23'])).
% 86.61/11.95 cnf('25', plain, (r1($sk1,$sk57)),
% 86.61/11.95 inference(resolution,[],['20','24'])).
% 86.61/11.95 cnf('26', plain, (~r1($sk1,X) | ~r1($sk1,Y) | ~r1($sk1,Z) | ~r1(Y,$sk1) | p2(Z) | p1(X)),
% 86.61/11.95 inference(factorization,[then_simplify],['8','25'])).
% 86.61/11.95 cnf('27', plain, (r1($sk33,$sk34)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('28', plain, (~r1(X,$sk33) | r1(X,$sk34)),
% 86.61/11.95 inference(resolution,[],['9','27'])).
% 86.61/11.95 cnf('29', plain, (r1($sk31,$sk33)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('30', plain, (r1($sk31,$sk34)),
% 86.61/11.95 inference(resolution,[],['28','29'])).
% 86.61/11.95 cnf('31', plain, (~r1(X,$sk31) | r1(X,$sk34)),
% 86.61/11.95 inference(resolution,[],['30','9'])).
% 86.61/11.95 cnf('32', plain, (r1($sk29,$sk31)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('33', plain, (r1($sk29,$sk34)),
% 86.61/11.95 inference(resolution,[],['31','32'])).
% 86.61/11.95 cnf('34', plain, (~r1(X,$sk29) | r1(X,$sk34)),
% 86.61/11.95 inference(resolution,[],['33','9'])).
% 86.61/11.95 cnf('35', plain, (r1($sk27,$sk29)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('36', plain, (~r1(X,$sk27) | r1(X,$sk29)),
% 86.61/11.95 inference(resolution,[],['9','35'])).
% 86.61/11.95 cnf('37', plain, (r1($sk25,$sk27)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('38', plain, (r1($sk25,$sk29)),
% 86.61/11.95 inference(resolution,[],['36','37'])).
% 86.61/11.95 cnf('39', plain, (~r1(X,$sk25) | r1(X,$sk29)),
% 86.61/11.95 inference(resolution,[],['38','9'])).
% 86.61/11.95 cnf('40', plain, (r1($sk1,$sk25)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('41', plain, (r1($sk1,$sk29)),
% 86.61/11.95 inference(resolution,[],['39','40'])).
% 86.61/11.95 cnf('42', plain, (r1($sk1,$sk34)),
% 86.61/11.95 inference(resolution,[],['34','41'])).
% 86.61/11.95 cnf('43', plain, (~p1($sk34)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('44', plain, (~r1($sk1,X) | ~r1($sk1,Y) | ~r1(Y,$sk1) | p2(X)),
% 86.61/11.95 inference(resolution,[then_simplify],['26','42','43'])).
% 86.61/11.95 cnf('45', plain, (r1($sk97,$sk102)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('46', plain, (~r1(X,$sk97) | r1(X,$sk102)),
% 86.61/11.95 inference(resolution,[],['9','45'])).
% 86.61/11.95 cnf('47', plain, (r1($sk95,$sk97)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('48', plain, (r1($sk95,$sk102)),
% 86.61/11.95 inference(resolution,[],['46','47'])).
% 86.61/11.95 cnf('49', plain, (~r1(X,$sk95) | r1(X,$sk102)),
% 86.61/11.95 inference(resolution,[],['48','9'])).
% 86.61/11.95 cnf('50', plain, (r1($sk93,$sk95)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('51', plain, (r1($sk93,$sk102)),
% 86.61/11.95 inference(resolution,[],['49','50'])).
% 86.61/11.95 cnf('52', plain, (~r1(X,$sk93) | r1(X,$sk102)),
% 86.61/11.95 inference(resolution,[],['51','9'])).
% 86.61/11.95 cnf('53', plain, (r1($sk91,$sk93)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('54', plain, (~r1(X,$sk91) | r1(X,$sk93)),
% 86.61/11.95 inference(resolution,[],['9','53'])).
% 86.61/11.95 cnf('55', plain, (r1($sk1,$sk91)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('56', plain, (r1($sk1,$sk93)),
% 86.61/11.95 inference(resolution,[],['54','55'])).
% 86.61/11.95 cnf('57', plain, (r1($sk1,$sk102)),
% 86.61/11.95 inference(resolution,[],['52','56'])).
% 86.61/11.95 cnf('58', plain, (~p2($sk102)),
% 86.61/11.95 inference(cnf_transformation,[],['main_$sk'])).
% 86.61/11.95 cnf('59', plain, (~r1($sk1,X) | ~r1(X,$sk1)),
% 86.61/11.95 inference(resolution,[then_simplify],['44','57','58'])).
% 86.61/11.95 cnf('60', plain, (~r1($sk1,$sk1)),
% 86.61/11.95 inference(factorization,[],['59'])).
% 86.61/11.95 cnf('61', plain, (r1(X,X)),
% 86.61/11.95 inference(cnf_transformation,[],['reflexivity_$sk'])).
% 86.61/11.95 cnf('62', plain, ($false),
% 86.61/11.95 inference(resolution,[],['60','61'])).
% 86.61/11.95
% 86.61/11.95 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 86.61/11.95
% 86.61/11.95 run 89 fork 0 statistics:
% 86.61/11.95 ----------------------------------
% 86.61/11.95 this run seconds: 0.698820
% 86.61/11.95 total seconds: 10.511846
% 86.61/11.95 stat_given_used: 1762
% 86.61/11.95 stat_given_used_at_endgame: 0
% 86.61/11.95 stat_given_candidates: 2391
% 86.61/11.96 stat_given_candidates_at_endgame: 0
% 86.61/11.96 stat_given_candidates_h: 0
% 86.61/11.96 stat_binres_derived_cl: 14549
% 86.61/11.96 stat_binres_derived_cl_h: 0
% 86.61/11.96 stat_factor_derived_cl: 5613
% 86.61/11.96 stat_para_derived_cl: 0
% 86.61/11.96 stat_tautologies_discarded: 99
% 86.61/11.96 stat_forward_subsumed: 1119
% 86.61/11.96 stat_derived_cut: 1678
% 86.61/11.96 stat_derived_rewritten: 0
% 86.61/11.96 stat_weight_discarded_building: 0
% 86.61/11.96 stat_weight_discarded_cl: 0
% 86.61/11.96 stat_internlimit_discarded_cl: 0
% 86.61/11.96 stat_simplified: 10 simplified 0 derived 0 given
% 86.61/11.96 stat_kept_cl: 18943
% 86.61/11.96 stat_built_cl: 22477
% 86.61/11.96 stat_hyperres_partial_cl: 0
% 86.61/11.96 stat_made_rewriters: 0
% 86.61/11.96 stat_backward_subsumed: 0
% 86.61/11.96 stat_propagated_subsumed: 0
% 86.61/11.96 stat_clsubs_attempted: 127678
% 86.61/11.96 stat_clsubs_fact_groundunit_found: 85
% 86.61/11.96 stat_clsubs_rule_groundunit_found: 55
% 86.61/11.96 stat_clsubs_top_meta_attempted: 1246446
% 86.61/11.96 stat_clsubs_top_meta_failed: 1118768
% 86.61/11.96 stat_clsubs_top_meta_nonpref_attempted: 1246446
% 86.61/11.96 stat_clsubs_top_meta_nonpref_succeeded: 635515
% 86.61/11.96 stat_clsubs_top_meta_pref_attempted: 635515
% 86.61/11.96 stat_clsubs_top_meta_pref1_succeeded: 282729
% 86.61/11.96 stat_clsubs_top_meta_pref2_succeeded: 134137
% 86.61/11.96 stat_clsubs_top_meta_pref3_succeeded: 127678
% 86.61/11.96 stat_clsubs_top_meta_pref_succeeded: 127678
% 86.61/11.96 stat_clsubs_meta_attempted: 330857
% 86.61/11.96 stat_clsubs_meta_failed: 55487
% 86.61/11.96 stat_clsubs_predsymbs_attempted: 0
% 86.61/11.96 stat_clsubs_unit_attempted: 573
% 86.61/11.96 stat_clsubs_full_attempted: 127105
% 86.61/11.96 stat_forwardsubs_attempted: 20062
% 86.61/11.96 stat_lit_hash_added: 1585
% 86.61/11.96 stat_lit_hash_computed: 497598
% 86.61/11.96 stat_lit_hash_match_found: 3005
% 86.61/11.96 stat_lit_hash_match_miss: 788379
% 86.61/11.96 stat_lit_hash_cut_ok: 1740
% 86.61/11.96 stat_lit_strong_cut_ok: 0
% 86.61/11.96 stat_lit_hash_subsume_ok: 1119
% 86.61/11.96 clqueue els 10000000 used 1
% 86.61/11.96 clactive els 10000000 used 1763
% 86.61/11.96 clactivesubsume els 10000000 used 8497
% 86.61/11.96 queue_termbuf els 200000000 used 3044019
% 86.61/11.96 hyper_termbuf els 100000000 used 1
% 86.61/11.96 active_termbuf els 100000000 used 69543
% 86.61/11.96 varstack els 5000 last used 1
% 86.61/11.96 given_termbuf els 10000000 last used 14
% 86.61/11.96 simplified_termbuf els 10000000 last used 1
% 86.61/11.96 derived_termbuf els 10000000 last used 3
% 86.61/11.96 wr_mallocs: 5687
% 86.61/11.96 wr_callocs: 19
% 86.61/11.96 wr_reallocs: 691
% 86.61/11.96 wr_frees: 4
% 86.61/11.96 wr_malloc_bytes: 4162794772
% 86.61/11.96 wr_calloc_bytes: 96065504
% 86.61/11.96 wr_realloc_bytes: 453936
% 86.61/11.96 wr_realloc_freebytes: 0
% 86.61/11.96 ----------------------------------
%------------------------------------------------------------------------------