%------------------------------------------------------------------------------
% File : GKC---0.8
% Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : gkc %s
% Computer : n031.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:09:14 PM UTC 2026
% Result : Theorem 29.19s 4.27s
% Output : CNFRefutation 29.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : gkc %s
% 0.10/0.36 % Computer : n031.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 13:49:24 UTC 2026
% 0.10/0.36 % 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: 146
% 0.14/0.43 in_rule_clause_count: 138
% 0.14/0.43 in_fact_clause_count: 8
% 0.14/0.43 in_answer_clause_count: 0
% 0.14/0.43 in_ground_clause_count: 12
% 0.14/0.43 in_unit_clause_count: 13
% 0.14/0.43 in_horn_clause_count: 82
% 0.14/0.43 in_pos_clause_count: 9
% 0.14/0.43 in_neg_clause_count: 4
% 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: 6
% 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: 21
% 0.14/0.43 in_min_vars: 0
% 0.14/0.43 in_max_vars: 4
% 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: 144
% 0.14/0.43 in_neg_goal_count: 4
% 0.14/0.43 in_pos_goal_count: 8
% 0.14/0.43 in_posunit_goal_count: 8
% 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.44
% 0.14/0.44 **** run 1 fork 0 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 2 fork 1 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 3 fork 2 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 4 fork 3 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"sine":5,"strategy":["unit"],"query_preference":0}
% 0.14/0.44
% 0.14/0.44 **** run 5 fork 4 starts with strategy
% 0.14/0.44 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.14/0.45
% 0.14/0.45 **** run 6 fork 5 starts with strategy
% 0.14/0.45 {"max_dseconds":1,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 0.14/0.45
% 0.14/0.45 **** run 7 fork 6 starts with strategy
% 0.14/0.45 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 0.14/0.45
% 0.14/0.45 **** run 8 fork 7 starts with strategy
% 0.14/0.45 {"max_dseconds":1,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 0.22/0.57
% 0.22/0.57
% 0.22/0.57 fork 5: search terminated without proof.
% 0.22/0.57
% 0.22/0.57
% 0.22/0.57 fork 0: search terminated without proof.
% 0.22/0.57
% 0.22/0.57
% 0.22/0.57 fork 1: search terminated without proof.
% 0.22/0.57
% 0.22/0.57
% 0.22/0.57 fork 2: 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 4: search terminated without proof.
% 0.22/0.59
% 0.22/0.59
% 0.22/0.59 fork 6: search terminated without proof.
% 0.22/0.60
% 0.22/0.60 **** run 14 fork 5 starts with strategy
% 0.22/0.60 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0}
% 1.40/0.62
% 1.40/0.62
% 1.40/0.62 fork 7: search terminated without proof.
% 1.40/0.63
% 1.40/0.63 **** run 10 fork 1 starts with strategy
% 1.40/0.63
% 1.40/0.63 **** run 9 fork 0 starts with strategy
% 1.40/0.63 {"max_dseconds":1,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 1.40/0.63 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 1.40/0.63
% 1.40/0.63 **** run 12 fork 3 starts with strategy
% 1.40/0.63 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 1.40/0.63
% 1.40/0.63 **** run 11 fork 2 starts with strategy
% 1.40/0.63 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1}
% 1.40/0.64
% 1.40/0.64 **** run 13 fork 4 starts with strategy
% 1.40/0.64 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 1.82/0.69
% 1.82/0.69 **** run 16 fork 7 starts with strategy
% 1.82/0.69 {"max_dseconds":1,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 1.82/0.69
% 1.82/0.69 **** run 15 fork 6 starts with strategy
% 1.82/0.69 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1}
% 2.12/0.72
% 2.12/0.72
% 2.12/0.72 fork 5: search terminated without proof.
% 2.12/0.75
% 2.12/0.75 **** run 22 fork 5 starts with strategy
% 2.12/0.75 {"max_dseconds":1,"strategy":["unit"],"query_preference":2}
% 2.12/0.76
% 2.12/0.76
% 2.12/0.76 fork 0: search terminated without proof.
% 2.12/0.76
% 2.12/0.76
% 2.12/0.76 fork 3: search terminated without proof.
% 2.12/0.76
% 2.12/0.76
% 2.12/0.76 fork 1: search terminated without proof.
% 2.12/0.76
% 2.12/0.76
% 2.12/0.76 fork 2: search terminated without proof.
% 2.12/0.77
% 2.12/0.77
% 2.12/0.77 fork 4: search terminated without proof.
% 2.93/0.82
% 2.93/0.82 **** run 18 fork 1 starts with strategy
% 2.93/0.82 {"max_dseconds":1,"strategy":["unit"],"query_preference":1,"reverse_clauselist":1}
% 2.93/0.82
% 2.93/0.82
% 2.93/0.82 fork 7: search terminated without proof.
% 2.93/0.82
% 2.93/0.82 **** run 17 fork 0 starts with strategy
% 2.93/0.82 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"depth_penalty":100}
% 2.93/0.82 **** run 19 fork 2 starts with strategy
% 2.93/0.82 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":2}
% 2.93/0.82
% 2.93/0.82
% 2.93/0.82 **** run 20 fork 3 starts with strategy
% 2.93/0.82 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":0}
% 2.93/0.83
% 2.93/0.83 **** run 21 fork 4 starts with strategy
% 2.93/0.83 {"max_dseconds":1,"strategy":["unit"],"query_preference":0}
% 2.93/0.83
% 2.93/0.83
% 2.93/0.83 fork 6: search terminated without proof.
% 2.93/0.89
% 2.93/0.89 **** run 24 fork 7 starts with strategy
% 2.93/0.89 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":1}
% 2.93/0.90
% 2.93/0.90
% 2.93/0.90 fork 5: search terminated without proof.
% 3.74/0.93
% 3.74/0.93 **** run 30 fork 5 starts with strategy
% 3.74/0.93
% 3.74/0.93 **** run 23 fork 6 starts with strategy
% 3.74/0.93 {"max_dseconds":1,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 3.74/0.93 {"max_dseconds":1,"strategy":["query_focus","max_ground_weight"],"query_preference":1}
% 3.74/0.95
% 3.74/0.95
% 3.74/0.95 fork 3: search terminated without proof.
% 3.74/1.01
% 3.74/1.01
% 3.74/1.01 fork 1: search terminated without proof.
% 3.74/1.01
% 3.74/1.01
% 3.74/1.01 fork 0: search terminated without proof.
% 3.74/1.01
% 3.74/1.01
% 3.74/1.01 fork 2: search terminated without proof.
% 3.74/1.01
% 3.74/1.01 **** run 28 fork 3 starts with strategy
% 3.74/1.01 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":2,"query_preference":1}
% 3.74/1.02
% 3.74/1.02
% 3.74/1.02 fork 4: search terminated without proof.
% 3.74/1.03
% 3.74/1.03 fork 7: search finished without proof.
% 4.85/1.06
% 4.85/1.06 **** run 25 fork 0 starts with strategy
% 4.85/1.06 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"sine":2}
% 4.85/1.06
% 4.85/1.06 **** run 26 fork 1 starts with strategy
% 4.85/1.06 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":2,"sine":1}
% 4.85/1.06
% 4.85/1.06 **** run 27 fork 2 starts with strategy
% 4.85/1.06 {"max_dseconds":1,"strategy":["hardness_pref"],"sine":1,"query_preference":1}
% 4.85/1.06
% 4.85/1.06 **** run 32 fork 7 starts with strategy
% 4.85/1.06 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":2}
% 4.85/1.07
% 4.85/1.07
% 4.85/1.07 fork 6: search terminated without proof.
% 4.85/1.09
% 4.85/1.09 **** run 29 fork 4 starts with strategy
% 4.85/1.09 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1}
% 4.85/1.09
% 4.85/1.09
% 4.85/1.09 fork 5: search terminated without proof.
% 4.85/1.14
% 4.85/1.14 **** run 38 fork 5 starts with strategy
% 4.85/1.14 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 5.62/1.17
% 5.62/1.17 **** run 31 fork 6 starts with strategy
% 5.62/1.17 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"weight_select_ratio":100,"repeat_var_weight":1}
% 5.62/1.20
% 5.62/1.20
% 5.62/1.20 fork 0: search terminated without proof.
% 5.62/1.20
% 5.62/1.20
% 5.62/1.20 fork 2: search terminated without proof.
% 5.62/1.20
% 5.62/1.20
% 5.62/1.20 fork 1: search terminated without proof.
% 6.02/1.22
% 6.02/1.22
% 6.02/1.22 fork 7: search terminated without proof.
% 6.02/1.23
% 6.02/1.23
% 6.02/1.23 fork 3: search terminated without proof.
% 6.02/1.24
% 6.02/1.24
% 6.02/1.24 fork 4: search terminated without proof.
% 6.02/1.24
% 6.02/1.24 **** run 35 fork 2 starts with strategy
% 6.02/1.24 {"max_dseconds":1,"strategy":["unit"],"query_preference":1}
% 6.02/1.24
% 6.02/1.24 **** run 33 fork 0 starts with strategy
% 6.02/1.24 {"max_dseconds":1,"strategy":["query_focus","unit"],"query_preference":1,"sine":1}
% 6.02/1.25
% 6.02/1.25 **** run 40 fork 7 starts with strategy
% 6.02/1.25 {"sine":2,"var_weight":70,"repeat_var_weight":70,"max_depth":0,"length_penalty":100,"query_preference":2,"strategy":["unit"],"max_dseconds":1}
% 6.02/1.25
% 6.02/1.25 **** run 34 fork 1 starts with strategy
% 6.02/1.25 {"max_dseconds":1,"strategy":["query_focus","double"],"query_preference":1}
% 6.02/1.28
% 6.02/1.28
% 6.02/1.28 fork 5: search terminated without proof.
% 6.02/1.28
% 6.02/1.28 **** run 37 fork 4 starts with strategy
% 6.02/1.28 {"max_dseconds":1,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 6.02/1.29
% 6.02/1.29 **** run 36 fork 3 starts with strategy
% 6.02/1.29 {"weight_select_ratio":20,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 6.77/1.33
% 6.77/1.33
% 6.77/1.33 fork 6: search terminated without proof.
% 6.77/1.35
% 6.77/1.35 **** run 46 fork 5 starts with strategy
% 6.77/1.35 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":3}
% 6.77/1.37
% 6.77/1.37
% 6.77/1.37 fork 7: search terminated without proof.
% 6.77/1.38
% 6.77/1.38
% 6.77/1.38 fork 2: search terminated without proof.
% 6.77/1.38
% 6.77/1.38
% 6.77/1.38 fork 0: search terminated without proof.
% 6.77/1.39
% 6.77/1.39
% 6.77/1.39 fork 1: search terminated without proof.
% 6.77/1.39
% 6.77/1.39 **** run 39 fork 6 starts with strategy
% 6.77/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}
% 6.77/1.40
% 6.77/1.40 **** run 48 fork 7 starts with strategy
% 6.77/1.40 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 7.59/1.42
% 7.59/1.42
% 7.59/1.42 fork 4: search terminated without proof.
% 7.59/1.43
% 7.59/1.43
% 7.59/1.43 fork 3: search terminated without proof.
% 7.59/1.43
% 7.59/1.43 **** run 41 fork 0 starts with strategy
% 7.59/1.43 {"max_dseconds":1,"strategy":["positive_pref"],"query_preference":0}
% 7.59/1.43
% 7.59/1.43 **** run 43 fork 2 starts with strategy
% 7.59/1.43 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":1}
% 7.59/1.43
% 7.59/1.43 **** run 42 fork 1 starts with strategy
% 7.59/1.43 {"max_dseconds":1,"strategy":["query_focus","positive_pref"],"query_preference":1}
% 7.59/1.47
% 7.59/1.47 **** run 45 fork 4 starts with strategy
% 7.59/1.47 {"max_dseconds":1,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 7.59/1.49
% 7.59/1.49 **** run 44 fork 3 starts with strategy
% 7.59/1.49 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"sine":2}
% 7.59/1.50
% 7.59/1.50
% 7.59/1.50 fork 5: search terminated without proof.
% 8.33/1.52
% 8.33/1.52
% 8.33/1.52 fork 6: search terminated without proof.
% 8.33/1.53
% 8.33/1.53
% 8.33/1.53 fork 7: search terminated without proof.
% 8.33/1.55
% 8.33/1.55 **** run 56 fork 7 starts with strategy
% 8.33/1.55 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0}
% 8.33/1.57
% 8.33/1.57 fork 0: search finished without proof.
% 8.33/1.57
% 8.33/1.57
% 8.33/1.57 fork 2: search terminated without proof.
% 8.33/1.57
% 8.33/1.57 **** run 54 fork 5 starts with strategy
% 8.33/1.57 {"max_dseconds":10,"sine":5,"strategy":["hardness_pref"],"query_preference":0}
% 8.33/1.57
% 8.33/1.57
% 8.33/1.57 fork 1: search terminated without proof.
% 8.33/1.58
% 8.33/1.58 **** run 47 fork 6 starts with strategy
% 8.33/1.58 {"max_dseconds":1,"strategy":["query_focus"],"query_preference":1,"var_weight":1,"repeat_var_weight":1}
% 9.16/1.62
% 9.16/1.62
% 9.16/1.62 fork 4: search terminated without proof.
% 9.16/1.62
% 9.16/1.62
% 9.16/1.62 fork 3: search terminated without proof.
% 9.16/1.62
% 9.16/1.62 **** run 51 fork 2 starts with strategy
% 9.16/1.62 {"weight_select_ratio":100,"length_penalty":100,"query_preference":1,"strategy":["query_focus"],"max_dseconds":1}
% 9.16/1.62
% 9.16/1.62 **** run 49 fork 0 starts with strategy
% 9.16/1.62 {"max_dseconds":1,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 9.16/1.62
% 9.16/1.62 **** run 50 fork 1 starts with strategy
% 9.16/1.62 {"max_dseconds":1,"strategy":["unit"],"query_preference":0,"var_weight":1,"depth_penalty":100,"repeat_var_weight":1}
% 9.16/1.66
% 9.16/1.66 **** run 53 fork 4 starts with strategy
% 9.16/1.66 {"max_dseconds":10,"sine":5,"strategy":["negative_pref"],"query_preference":0}
% 9.16/1.67
% 9.16/1.67 **** run 52 fork 3 starts with strategy
% 9.16/1.67 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0}
% 9.97/1.71
% 9.97/1.71
% 9.97/1.71 fork 6: search terminated without proof.
% 9.97/1.76
% 9.97/1.76
% 9.97/1.76 fork 2: search terminated without proof.
% 9.97/1.76
% 9.97/1.76
% 9.97/1.76 fork 0: search terminated without proof.
% 9.97/1.76
% 9.97/1.76
% 9.97/1.76 fork 1: search terminated without proof.
% 9.97/1.78
% 9.97/1.78 **** run 55 fork 6 starts with strategy
% 9.97/1.78 {"max_dseconds":10,"sine":5,"strategy":["unit"],"query_preference":0}
% 10.74/1.81
% 10.74/1.81 **** run 59 fork 2 starts with strategy
% 10.74/1.81 {"max_dseconds":10,"strategy":["unit"],"weight_select_ratio":100,"query_preference":0}
% 10.74/1.81
% 10.74/1.81 **** run 57 fork 0 starts with strategy
% 10.74/1.81 {"max_dseconds":10,"strategy":["hardness_pref"],"weight_select_ratio":100,"query_preference":0}
% 10.74/1.81
% 10.74/1.81 **** run 58 fork 1 starts with strategy
% 10.74/1.81 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 16.30/2.58
% 16.30/2.58
% 16.30/2.58 fork 7: search terminated without proof.
% 17.10/2.61
% 17.10/2.61 **** run 64 fork 7 starts with strategy
% 17.10/2.61 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0}
% 17.10/2.62
% 17.10/2.62
% 17.10/2.62 fork 5: search terminated without proof.
% 17.10/2.69
% 17.10/2.69 **** run 62 fork 5 starts with strategy
% 17.10/2.69 {"max_dseconds":10,"strategy":["query_focus","positive_pref"],"query_preference":0}
% 17.94/2.74
% 17.94/2.74
% 17.94/2.74 fork 4: search terminated without proof.
% 17.94/2.76
% 17.94/2.76
% 17.94/2.76 fork 3: search terminated without proof.
% 17.94/2.79
% 17.94/2.79 **** run 61 fork 4 starts with strategy
% 17.94/2.79 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"weight_select_ratio":100,"depth_penalty":100,"length_penalty":100}
% 18.70/2.80
% 18.70/2.80
% 18.70/2.80 fork 6: search terminated without proof.
% 18.70/2.81
% 18.70/2.81 **** run 60 fork 3 starts with strategy
% 18.70/2.81 {"max_dseconds":10,"strategy":["negative_pref"],"weight_select_ratio":100,"query_preference":0,"var_weight":70,"repeat_var_weight":70}
% 18.70/2.85
% 18.70/2.85
% 18.70/2.85 fork 2: search terminated without proof.
% 18.70/2.85
% 18.70/2.85
% 18.70/2.85 fork 0: search terminated without proof.
% 18.70/2.85
% 18.70/2.85
% 18.70/2.85 fork 1: search terminated without proof.
% 18.70/2.86
% 18.70/2.86 **** run 63 fork 6 starts with strategy
% 18.70/2.86 {"max_dseconds":10,"strategy":["negative_pref"],"query_preference":0,"sine":1}
% 18.70/2.89
% 18.70/2.89 **** run 67 fork 2 starts with strategy
% 18.70/2.89 {"max_dseconds":10,"strategy":["unit"],"query_preference":0}
% 18.70/2.90
% 18.70/2.90 **** run 65 fork 0 starts with strategy
% 18.70/2.90 {"max_dseconds":10,"strategy":["hardness_pref","max_ground_weight"],"query_preference":0}
% 18.70/2.90
% 18.70/2.90 **** run 66 fork 1 starts with strategy
% 18.70/2.90 {"max_dseconds":10,"strategy":["query_focus","unit"],"query_preference":0}
% 24.75/3.63
% 24.75/3.63
% 24.75/3.63 fork 7: search terminated without proof.
% 24.75/3.66
% 24.75/3.66 **** run 72 fork 7 starts with strategy
% 24.75/3.66 {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 25.51/3.75
% 25.51/3.75
% 25.51/3.75 fork 5: search terminated without proof.
% 26.28/3.80
% 26.28/3.80 **** run 70 fork 5 starts with strategy
% 26.28/3.80 {"length_penalty":100,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 26.28/3.87
% 26.28/3.87
% 26.28/3.87 fork 4: search terminated without proof.
% 27.08/3.92
% 27.08/3.92 **** run 69 fork 4 starts with strategy
% 27.08/3.92 {"max_dseconds":10,"strategy":["hardness_pref"],"query_preference":0,"weight_select_ratio":20,"depth_penalty":50,"length_penalty":100}
% 27.08/3.93
% 27.08/3.93
% 27.08/3.93 fork 2: search terminated without proof.
% 27.08/3.94
% 27.08/3.94 fork 3: search finished without proof.
% 27.08/3.95
% 27.08/3.95
% 27.08/3.95 fork 1: search terminated without proof.
% 27.08/3.98
% 27.08/3.98 **** run 75 fork 2 starts with strategy
% 27.08/3.98 {"max_dseconds":10,"strategy":["unit","posunitpara"],"query_preference":0,"sine":2}
% 27.08/3.98
% 27.08/3.98
% 27.08/3.98 fork 6: search terminated without proof.
% 27.08/3.99
% 27.08/3.99 **** run 68 fork 3 starts with strategy
% 27.08/3.99 {"max_dseconds":10,"strategy":["hardness_pref"],"var_weight":70,"repeat_var_weight":70,"query_preference":0}
% 27.08/4.00
% 27.08/4.00 **** run 74 fork 1 starts with strategy
% 27.08/4.00 {"max_dseconds":10,"strategy":["unit"],"query_preference":0,"sine":2}
% 27.08/4.04
% 27.08/4.04 **** run 71 fork 6 starts with strategy
% 27.08/4.04 {"strategy":["hardness_pref","max_weight"],"length_penalty":100,"depth_penalty":50,"max_depth":3,"var_weight":10,"repeat_var_weight":10,"max_dseconds":10}
% 28.18/4.11
% 28.18/4.11
% 28.18/4.11 fork 0: search terminated without proof.
% 28.18/4.15
% 28.18/4.15 **** run 73 fork 0 starts with strategy
% 28.18/4.15 {"var_weight":70,"repeat_var_weight":70,"max_depth":3,"query_preference":0,"strategy":["negative_pref"],"max_dseconds":10}
% 29.19/4.27
% 29.19/4.27
% 29.19/4.27 result: proof found
% 29.19/4.27 for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.19/4.27 by run 72 fork 7 strategy {"max_dseconds":10,"strategy":["positive_pref"],"query_preference":0}
% 29.19/4.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.19/4.27
% 29.19/4.27 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.19/4.27 fof('transitivity_$sk', plain, (r1(X3,X2) | (~r1(X1,X2) | ~r1(X3,X1))),
% 29.19/4.27 inference(negpush_and_skolemize,[],['transitivity'])).
% 29.19/4.27 fof('transitivity', axiom, (! [X,Y,Z] : ((r1(X,Y) & r1(Y,Z)) => r1(X,Z))),
% 29.19/4.27 input).
% 29.19/4.27 fof('main_$sk', plain, (((~p11($sk3) & r1($sk2,$sk3)) & r1($sk1,$sk2)) & (((~p12($sk5) & r1($sk4,$sk5)) & r1($sk1,$sk4)) & (((~p13($sk7) & r1($sk6,$sk7)) & r1($sk1,$sk6)) & (((~p15($sk9) & r1($sk8,$sk9)) & r1($sk1,$sk8)) & (((p11(X1) | (~p23($sk10(X1)) & r1(X1,$sk10(X1)))) | ~r1($sk1,X1)) & (((p11(X2) | (~p25($sk11(X2)) & r1(X2,$sk11(X2)))) | ~r1($sk1,X2)) & (((p12(X3) | (~p21($sk12(X3)) & r1(X3,$sk12(X3)))) | ~r1($sk1,X3)) & (((p13(X4) | (~p23($sk13(X4)) & r1(X4,$sk13(X4)))) | ~r1($sk1,X4)) & (((p13(X5) | (~p25($sk14(X5)) & r1(X5,$sk14(X5)))) | ~r1($sk1,X5)) & (((p15(X6) | (~p23($sk15(X6)) & r1(X6,$sk15(X6)))) | ~r1($sk1,X6)) & (((p15(X7) | (~p25($sk16(X7)) & r1(X7,$sk16(X7)))) | ~r1($sk1,X7)) & ((((p21(X9) | (~p31($sk17(X8,X9)) & r1(X9,$sk17(X8,X9)))) | ~r1(X8,X9)) | ~r1($sk1,X8)) & ((((p21(X11) | (~p33($sk18(X10,X11)) & r1(X11,$sk18(X10,X11)))) | ~r1(X10,X11)) | ~r1($sk1,X10)) & ((((p21(X13) | (~p34($sk19(X12,X13)) & r1(X13,$sk19(X12,X13)))) | ~r1(X12,X13)) | ~r1($sk1,X12)) & ((((p21(X15) | (~p35($sk20(X14,X15)) & r1(X15,$sk20(X14,X15)))) | ~r1(X14,X15)) | ~r1($sk1,X14)) & (((p14(X16) | (~p22($sk21(X16)) & r1(X16,$sk21(X16)))) | ~r1($sk1,X16)) & (((p16(X17) | (~p22($sk22(X17)) & r1(X17,$sk22(X17)))) | ~r1($sk1,X17)) & ((((p23(X19) | (~p31($sk23(X18,X19)) & r1(X19,$sk23(X18,X19)))) | ~r1(X18,X19)) | ~r1($sk1,X18)) & ((((p23(X21) | (~p33($sk24(X20,X21)) & r1(X21,$sk24(X20,X21)))) | ~r1(X20,X21)) | ~r1($sk1,X20)) & ((((p23(X23) | (~p35($sk25(X22,X23)) & r1(X23,$sk25(X22,X23)))) | ~r1(X22,X23)) | ~r1($sk1,X22)) & (((p14(X24) | (~p24($sk26(X24)) & r1(X24,$sk26(X24)))) | ~r1($sk1,X24)) & (((p16(X25) | (~p24($sk27(X25)) & r1(X25,$sk27(X25)))) | ~r1($sk1,X25)) & ((((p25(X27) | (~p31($sk28(X26,X27)) & r1(X27,$sk28(X26,X27)))) | ~r1(X26,X27)) | ~r1($sk1,X26)) & ((((p25(X29) | (~p33($sk29(X28,X29)) & r1(X29,$sk29(X28,X29)))) | ~r1(X28,X29)) | ~r1($sk1,X28)) & ((((p25(X31) | (~p35($sk30(X30,X31)) & r1(X31,$sk30(X30,X31)))) | ~r1(X30,X31)) | ~r1($sk1,X30)) & (((p14(X32) | (~p26($sk31(X32)) & r1(X32,$sk31(X32)))) | ~r1($sk1,X32)) & (((p16(X33) | (~p26($sk32(X33)) & r1(X33,$sk32(X33)))) | ~r1($sk1,X33)) & (((((p31(X36) | (~p43($sk33(X34,X35,X36)) & r1(X36,$sk33(X34,X35,X36)))) | ~r1(X35,X36)) | ~r1(X34,X35)) | ~r1($sk1,X34)) & (((((p31(X39) | (~p45($sk34(X37,X38,X39)) & r1(X39,$sk34(X37,X38,X39)))) | ~r1(X38,X39)) | ~r1(X37,X38)) | ~r1($sk1,X37)) & ((((p22(X41) | (~p32($sk35(X40,X41)) & r1(X41,$sk35(X40,X41)))) | ~r1(X40,X41)) | ~r1($sk1,X40)) & ((((p24(X43) | (~p32($sk36(X42,X43)) & r1(X43,$sk36(X42,X43)))) | ~r1(X42,X43)) | ~r1($sk1,X42)) & ((((p26(X45) | (~p32($sk37(X44,X45)) & r1(X45,$sk37(X44,X45)))) | ~r1(X44,X45)) | ~r1($sk1,X44)) & (((((p33(X48) | (~p43($sk38(X46,X47,X48)) & r1(X48,$sk38(X46,X47,X48)))) | ~r1(X47,X48)) | ~r1(X46,X47)) | ~r1($sk1,X46)) & (((((p33(X51) | (~p45($sk39(X49,X50,X51)) & r1(X51,$sk39(X49,X50,X51)))) | ~r1(X50,X51)) | ~r1(X49,X50)) | ~r1($sk1,X49)) & (((((p34(X54) | (~p41($sk40(X52,X53,X54)) & r1(X54,$sk40(X52,X53,X54)))) | ~r1(X53,X54)) | ~r1(X52,X53)) | ~r1($sk1,X52)) & ((((p22(X56) | (~p34($sk41(X55,X56)) & r1(X56,$sk41(X55,X56)))) | ~r1(X55,X56)) | ~r1($sk1,X55)) & ((((p24(X58) | (~p34($sk42(X57,X58)) & r1(X58,$sk42(X57,X58)))) | ~r1(X57,X58)) | ~r1($sk1,X57)) & ((((p26(X60) | (~p34($sk43(X59,X60)) & r1(X60,$sk43(X59,X60)))) | ~r1(X59,X60)) | ~r1($sk1,X59)) & (((((p35(X63) | (~p43($sk44(X61,X62,X63)) & r1(X63,$sk44(X61,X62,X63)))) | ~r1(X62,X63)) | ~r1(X61,X62)) | ~r1($sk1,X61)) & (((((p35(X66) | (~p45($sk45(X64,X65,X66)) & r1(X66,$sk45(X64,X65,X66)))) | ~r1(X65,X66)) | ~r1(X64,X65)) | ~r1($sk1,X64)) & ((((p22(X68) | (~p36($sk46(X67,X68)) & r1(X68,$sk46(X67,X68)))) | ~r1(X67,X68)) | ~r1($sk1,X67)) & ((((p24(X70) | (~p36($sk47(X69,X70)) & r1(X70,$sk47(X69,X70)))) | ~r1(X69,X70)) | ~r1($sk1,X69)) & ((((p26(X72) | (~p36($sk48(X71,X72)) & r1(X72,$sk48(X71,X72)))) | ~r1(X71,X72)) | ~r1($sk1,X71)) & ((((((p41(X76) | (~p51($sk49(X73,X74,X75,X76)) & r1(X76,$sk49(X73,X74,X75,X76)))) | ~r1(X75,X76)) | ~r1(X74,X75)) | ~r1(X73,X74)) | ~r1($sk1,X73)) & ((((((p41(X80) | (~p53($sk50(X77,X78,X79,X80)) & r1(X80,$sk50(X77,X78,X79,X80)))) | ~r1(X79,X80)) | ~r1(X78,X79)) | ~r1(X77,X78)) | ~r1($sk1,X77)) & ((((((p41(X84) | (~p54($sk51(X81,X82,X83,X84)) & r1(X84,$sk51(X81,X82,X83,X84)))) | ~r1(X83,X84)) | ~r1(X82,X83)) | ~r1(X81,X82)) | ~r1($sk1,X81)) & ((((((p41(X88) | (~p55($sk52(X85,X86,X87,X88)) & r1(X88,$sk52(X85,X86,X87,X88)))) | ~r1(X87,X88)) | ~r1(X86,X87)) | ~r1(X85,X86)) | ~r1($sk1,X85)) & (((((p32(X91) | (~p42($sk53(X89,X90,X91)) & r1(X91,$sk53(X89,X90,X91)))) | ~r1(X90,X91)) | ~r1(X89,X90)) | ~r1($sk1,X89)) & (((((p36(X94) | (~p42($sk54(X92,X93,X94)) & r1(X94,$sk54(X92,X93,X94)))) | ~r1(X93,X94)) | ~r1(X92,X93)) | ~r1($sk1,X92)) & ((((((p43(X98) | (~p51($sk55(X95,X96,X97,X98)) & r1(X98,$sk55(X95,X96,X97,X98)))) | ~r1(X97,X98)) | ~r1(X96,X97)) | ~r1(X95,X96)) | ~r1($sk1,X95)) & ((((((p43(X102) | (~p53($sk56(X99,X100,X101,X102)) & r1(X102,$sk56(X99,X100,X101,X102)))) | ~r1(X101,X102)) | ~r1(X100,X101)) | ~r1(X99,X100)) | ~r1($sk1,X99)) & ((((((p43(X106) | (~p55($sk57(X103,X104,X105,X106)) & r1(X106,$sk57(X103,X104,X105,X106)))) | ~r1(X105,X106)) | ~r1(X104,X105)) | ~r1(X103,X104)) | ~r1($sk1,X103)) & (((((p32(X109) | (~p44($sk58(X107,X108,X109)) & r1(X109,$sk58(X107,X108,X109)))) | ~r1(X108,X109)) | ~r1(X107,X108)) | ~r1($sk1,X107)) & (((((p36(X112) | (~p44($sk59(X110,X111,X112)) & r1(X112,$sk59(X110,X111,X112)))) | ~r1(X111,X112)) | ~r1(X110,X111)) | ~r1($sk1,X110)) & ((((((p45(X116) | (~p51($sk60(X113,X114,X115,X116)) & r1(X116,$sk60(X113,X114,X115,X116)))) | ~r1(X115,X116)) | ~r1(X114,X115)) | ~r1(X113,X114)) | ~r1($sk1,X113)) & ((((((p45(X120) | (~p53($sk61(X117,X118,X119,X120)) & r1(X120,$sk61(X117,X118,X119,X120)))) | ~r1(X119,X120)) | ~r1(X118,X119)) | ~r1(X117,X118)) | ~r1($sk1,X117)) & ((((((p45(X124) | (~p55($sk62(X121,X122,X123,X124)) & r1(X124,$sk62(X121,X122,X123,X124)))) | ~r1(X123,X124)) | ~r1(X122,X123)) | ~r1(X121,X122)) | ~r1($sk1,X121)) & (((((p32(X127) | (~p46($sk63(X125,X126,X127)) & r1(X127,$sk63(X125,X126,X127)))) | ~r1(X126,X127)) | ~r1(X125,X126)) | ~r1($sk1,X125)) & (((((p36(X130) | (~p46($sk64(X128,X129,X130)) & r1(X130,$sk64(X128,X129,X130)))) | ~r1(X129,X130)) | ~r1(X128,X129)) | ~r1($sk1,X128)) & ((((((p42(X134) | (~p52($sk65(X131,X132,X133,X134)) & r1(X134,$sk65(X131,X132,X133,X134)))) | ~r1(X133,X134)) | ~r1(X132,X133)) | ~r1(X131,X132)) | ~r1($sk1,X131)) & ((((((p44(X138) | (~p52($sk66(X135,X136,X137,X138)) & r1(X138,$sk66(X135,X136,X137,X138)))) | ~r1(X137,X138)) | ~r1(X136,X137)) | ~r1(X135,X136)) | ~r1($sk1,X135)) & ((((((p46(X142) | (~p52($sk67(X139,X140,X141,X142)) & r1(X142,$sk67(X139,X140,X141,X142)))) | ~r1(X141,X142)) | ~r1(X140,X141)) | ~r1(X139,X140)) | ~r1($sk1,X139)) & ((((((p42(X146) | (~p54($sk68(X143,X144,X145,X146)) & r1(X146,$sk68(X143,X144,X145,X146)))) | ~r1(X145,X146)) | ~r1(X144,X145)) | ~r1(X143,X144)) | ~r1($sk1,X143)) & ((((((p44(X150) | (~p54($sk69(X147,X148,X149,X150)) & r1(X150,$sk69(X147,X148,X149,X150)))) | ~r1(X149,X150)) | ~r1(X148,X149)) | ~r1(X147,X148)) | ~r1($sk1,X147)) & ((((((p46(X154) | (~p54($sk70(X151,X152,X153,X154)) & r1(X154,$sk70(X151,X152,X153,X154)))) | ~r1(X153,X154)) | ~r1(X152,X153)) | ~r1(X151,X152)) | ~r1($sk1,X151)) & ((((((p42(X158) | (~p56($sk71(X155,X156,X157,X158)) & r1(X158,$sk71(X155,X156,X157,X158)))) | ~r1(X157,X158)) | ~r1(X156,X157)) | ~r1(X155,X156)) | ~r1($sk1,X155)) & ((((((p44(X162) | (~p56($sk72(X159,X160,X161,X162)) & r1(X162,$sk72(X159,X160,X161,X162)))) | ~r1(X161,X162)) | ~r1(X160,X161)) | ~r1(X159,X160)) | ~r1($sk1,X159)) & ((((((p46(X166) | (~p56($sk73(X163,X164,X165,X166)) & r1(X166,$sk73(X163,X164,X165,X166)))) | ~r1(X165,X166)) | ~r1(X164,X165)) | ~r1(X163,X164)) | ~r1($sk1,X163)) & (((p52(X168) | ~r1(X167,X168)) & ((p54(X169) | ~r1(X167,X169)) & ((p54(X170) | ~r1(X167,X170)) & (p56(X171) | ~r1(X167,X171))))) | ~r1($sk1,X167)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),
% 29.19/4.27 inference(negpush_and_skolemize,[],['main'])).
% 29.19/4.27 fof('main', conjecture, ~(? [X] : ~((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~(! [Y] : (~r1(X,Y) | ~(((~(! [X] : (~r1(Y,X) | p56(X))) | ~(! [X] : (~r1(Y,X) | p54(X)))) | ~(! [X] : (~r1(Y,X) | p54(X)))) | ~(! [X] : (~r1(Y,X) | p52(X)))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p56(Y))) & ~p46(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p56(Y))) & ~p44(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p56(Y))) & ~p42(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p54(Y))) & ~p46(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p54(Y))) & ~p44(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p54(Y))) & ~p42(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p52(Y))) & ~p46(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p52(Y))) & ~p44(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p52(Y))) & ~p42(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p46(X))) & ~p36(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p46(X))) & ~p32(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p55(Y))) & ~p45(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p53(Y))) & ~p45(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p51(Y))) & ~p45(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p44(X))) & ~p36(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p44(X))) & ~p32(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p55(Y))) & ~p43(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p53(Y))) & ~p43(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p51(Y))) & ~p43(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p42(X))) & ~p36(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p42(X))) & ~p32(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p55(Y))) & ~p41(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p54(Y))) & ~p41(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p53(Y))) & ~p41(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p51(Y))) & ~p41(X))))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p36(Y))) & ~p26(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p36(Y))) & ~p24(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p36(Y))) & ~p22(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p45(X))) & ~p35(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p43(X))) & ~p35(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p34(Y))) & ~p26(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p34(Y))) & ~p24(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p34(Y))) & ~p22(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p41(X))) & ~p34(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p45(X))) & ~p33(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p43(X))) & ~p33(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p32(Y))) & ~p26(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p32(Y))) & ~p24(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p32(Y))) & ~p22(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p45(X))) & ~p31(Y))))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | (! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p43(X))) & ~p31(Y))))))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p26(X))) & ~p16(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p26(X))) & ~p14(Y))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p35(Y))) & ~p25(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p33(Y))) & ~p25(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p31(Y))) & ~p25(X))))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p24(X))) & ~p16(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p24(X))) & ~p14(Y))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p35(Y))) & ~p23(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p33(Y))) & ~p23(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p31(Y))) & ~p23(X))))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p22(X))) & ~p16(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p22(X))) & ~p14(Y))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p35(Y))) & ~p21(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p34(Y))) & ~p21(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p33(Y))) & ~p21(X))))))) | ~(! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | ~((! [Y] : (~r1(X,Y) | p31(Y))) & ~p21(X))))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p25(X))) & ~p15(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p23(X))) & ~p15(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p25(X))) & ~p13(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p23(X))) & ~p13(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p21(X))) & ~p12(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p25(X))) & ~p11(Y))))) | ~(! [Y] : (~r1(X,Y) | ~((! [X] : (~r1(Y,X) | p23(X))) & ~p11(Y))))) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | p15(X)))))) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | p13(X)))))) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | p12(X)))))) | (! [Y] : (~r1(X,Y) | (! [X] : (~r1(Y,X) | p11(X))))))),
% 29.19/4.27 input).
% 29.19/4.27 fof('reflexivity_$sk', plain, r1(X1,X1),
% 29.19/4.27 inference(negpush_and_skolemize,[],['reflexivity'])).
% 29.19/4.27 fof('reflexivity', axiom, (! [X] : r1(X,X)),
% 29.19/4.27 input).
% 29.19/4.27 cnf('1', plain, (~r1(X,Y) | ~r1(Z,X) | r1(Z,Y)),
% 29.19/4.27 inference(cnf_transformation,[],['transitivity_$sk'])).
% 29.19/4.27 cnf('2', plain, (~p21($sk12(X)) | ~r1($sk1,X) | p12(X)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('3', plain, (~p12($sk5)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('4', plain, (~p21($sk12($sk5)) | ~r1($sk1,$sk5)),
% 29.19/4.27 inference(resolution,[],['2','3'])).
% 29.19/4.27 cnf('5', plain, (~p21($sk12($sk5)) | ~r1($sk1,X) | ~r1(X,$sk5)),
% 29.19/4.27 inference(resolution,[],['1','4'])).
% 29.19/4.27 cnf('6', plain, (r1($sk1,$sk4)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('7', plain, (r1($sk4,$sk5)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('8', plain, (~p21($sk12($sk5))),
% 29.19/4.27 inference(resolution,[then_simplify],['5','6','7'])).
% 29.19/4.27 cnf('9', plain, (~p34($sk19(X,Y)) | ~r1($sk1,X) | ~r1(X,Y) | p21(Y)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('10', plain, (~p34($sk19(X,$sk12($sk5))) | ~r1(X,$sk12($sk5)) | ~r1($sk1,X)),
% 29.19/4.27 inference(resolution,[],['8','9'])).
% 29.19/4.27 cnf('11', plain, (~p41($sk40(X,Y,Z)) | ~r1($sk1,X) | ~r1(Y,Z) | ~r1(X,Y) | p34(Z)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('12', plain, (~p41($sk40(X,Y,$sk19(Z,$sk12($sk5)))) | ~r1(Y,$sk19(Z,$sk12($sk5))) | ~r1(Z,$sk12($sk5)) | ~r1($sk1,X) | ~r1($sk1,Z) | ~r1(X,Y)),
% 29.19/4.27 inference(resolution,[],['10','11'])).
% 29.19/4.27 cnf('13', plain, (r1(X0,X0)),
% 29.19/4.27 inference(cnf_transformation,[],['reflexivity_$sk'])).
% 29.19/4.27 cnf('14', plain, (~p41($sk40($sk1,X,$sk19(X,$sk12($sk5)))) | ~r1(X,$sk19(X,$sk12($sk5))) | ~r1(X,$sk12($sk5)) | ~r1($sk1,X)),
% 29.19/4.27 inference(factorization,[then_simplify],['12','13'])).
% 29.19/4.27 cnf('15', plain, (~p54($sk51(X,Y,Z,U)) | ~r1($sk1,X) | ~r1(Z,U) | ~r1(Y,Z) | ~r1(X,Y) | p41(U)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('16', plain, (~p54($sk51(X,X,X,Y)) | ~r1($sk1,X) | ~r1(X,Y) | p41(Y)),
% 29.19/4.27 inference(factorization,[then_simplify],['15','13'])).
% 29.19/4.27 cnf('17', plain, (~p54($sk51(X,X,X,$sk40($sk1,Y,$sk19(Y,$sk12($sk5))))) | ~r1(X,$sk40($sk1,Y,$sk19(Y,$sk12($sk5)))) | ~r1(Y,$sk19(Y,$sk12($sk5))) | ~r1(Y,$sk12($sk5)) | ~r1($sk1,X) | ~r1($sk1,Y)),
% 29.19/4.27 inference(resolution,[],['14','16'])).
% 29.19/4.27 cnf('18', plain, (~p54($sk51(X,X,X,$sk40($sk1,X,$sk19(X,$sk12($sk5))))) | ~r1(X,$sk40($sk1,X,$sk19(X,$sk12($sk5)))) | ~r1(X,$sk19(X,$sk12($sk5))) | ~r1(X,$sk12($sk5)) | ~r1($sk1,X)),
% 29.19/4.27 inference(factorization,[],['17'])).
% 29.19/4.27 cnf('19', plain, (~r1($sk1,X) | ~r1(X,Y) | p54(Y)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('20', plain, (~r1(X,$sk51(Y,Y,Y,$sk40($sk1,Y,$sk19(Y,$sk12($sk5))))) | ~r1(Y,$sk40($sk1,Y,$sk19(Y,$sk12($sk5)))) | ~r1(Y,$sk19(Y,$sk12($sk5))) | ~r1(Y,$sk12($sk5)) | ~r1($sk1,X) | ~r1($sk1,Y)),
% 29.19/4.27 inference(resolution,[],['18','19'])).
% 29.19/4.27 cnf('21', plain, (r1(X,$sk51(Y,Z,U,X)) | ~r1($sk1,Y) | ~r1(U,X) | ~r1(Z,U) | ~r1(Y,Z) | p41(X)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('22', plain, (r1(X,$sk51(Y,$sk1,Y,X)) | ~r1($sk1,Y) | ~r1(Y,$sk1) | ~r1(Y,X) | p41(X)),
% 29.19/4.27 inference(factorization,[],['21'])).
% 29.19/4.27 cnf('23', plain, (r1(X,$sk51($sk1,$sk1,$sk1,X)) | ~r1($sk1,X) | p41(X)),
% 29.19/4.27 inference(factorization,[then_simplify],['22','13'])).
% 29.19/4.27 cnf('24', plain, (~r1($sk1,$sk40($sk1,$sk1,$sk19($sk1,$sk12($sk5)))) | ~r1($sk1,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,$sk12($sk5)) | p41($sk40($sk1,$sk1,$sk19($sk1,$sk12($sk5))))),
% 29.19/4.27 inference(resolution,[then_simplify],['20','23','13'])).
% 29.19/4.27 cnf('25', plain, (~p41($sk40(X,Y,$sk19(X,$sk12($sk5)))) | ~r1(Y,$sk19(X,$sk12($sk5))) | ~r1(X,$sk12($sk5)) | ~r1($sk1,X) | ~r1(X,Y)),
% 29.19/4.27 inference(factorization,[],['12'])).
% 29.19/4.27 cnf('26', plain, (~r1($sk1,$sk40($sk1,$sk1,$sk19($sk1,$sk12($sk5)))) | ~r1($sk1,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,$sk12($sk5))),
% 29.19/4.27 inference(resolution,[then_simplify],['24','25','13'])).
% 29.19/4.27 cnf('27', plain, (~r1($sk1,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,$sk12($sk5)) | ~r1(X,$sk40($sk1,$sk1,$sk19($sk1,$sk12($sk5)))) | ~r1($sk1,X)),
% 29.19/4.27 inference(resolution,[],['26','1'])).
% 29.19/4.27 cnf('28', plain, (r1(X,$sk40(Y,Z,X)) | ~r1($sk1,Y) | ~r1(Z,X) | ~r1(Y,Z) | p34(X)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('29', plain, (r1(X,$sk40($sk1,$sk1,X)) | ~r1($sk1,X) | p34(X)),
% 29.19/4.27 inference(factorization,[then_simplify],['28','13'])).
% 29.19/4.27 cnf('30', plain, (~r1($sk1,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,$sk12($sk5)) | p34($sk19($sk1,$sk12($sk5)))),
% 29.19/4.27 inference(resolution,[],['27','29'])).
% 29.19/4.27 cnf('31', plain, (~r1($sk1,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,$sk12($sk5))),
% 29.19/4.27 inference(resolution,[then_simplify],['30','10','13'])).
% 29.19/4.27 cnf('32', plain, (~r1($sk1,$sk12($sk5)) | ~r1(X,$sk19($sk1,$sk12($sk5))) | ~r1($sk1,X)),
% 29.19/4.27 inference(resolution,[],['31','1'])).
% 29.19/4.27 cnf('33', plain, (r1(X,$sk19(Y,X)) | ~r1($sk1,Y) | ~r1(Y,X) | p21(X)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('34', plain, (~p21($sk12($sk5))),
% 29.19/4.27 inference(resolution,[then_simplify],['5','6','7'])).
% 29.19/4.27 cnf('35', plain, (~r1($sk1,$sk12($sk5))),
% 29.19/4.27 inference(resolution,[then_simplify],['32','33','34','13'])).
% 29.19/4.27 cnf('36', plain, (~r1(X,$sk12($sk5)) | ~r1($sk1,X)),
% 29.19/4.27 inference(resolution,[],['35','1'])).
% 29.19/4.27 cnf('37', plain, (r1(X,$sk12(X)) | ~r1($sk1,X) | p12(X)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('38', plain, (~p12($sk5)),
% 29.19/4.27 inference(cnf_transformation,[],['main_$sk'])).
% 29.19/4.27 cnf('39', plain, (~r1($sk1,$sk5)),
% 29.19/4.27 inference(resolution,[then_simplify],['36','37','38'])).
% 29.19/4.27 cnf('40', plain, (~r1($sk1,X) | ~r1(X,$sk5)),
% 29.19/4.27 inference(resolution,[],['39','1'])).
% 29.19/4.27 cnf('41', plain, ($false),
% 29.19/4.27 inference(resolution,[then_simplify],['40','6','7'])).
% 29.19/4.27
% 29.19/4.27 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.19/4.27
% 29.19/4.27 run 72 fork 7 statistics:
% 29.19/4.27 ----------------------------------
% 29.19/4.27 this run seconds: 0.260046
% 29.19/4.27 total seconds: 3.430252
% 29.19/4.27 stat_given_used: 2541
% 29.19/4.27 stat_given_used_at_endgame: 0
% 29.19/4.27 stat_given_candidates: 4659
% 29.19/4.27 stat_given_candidates_at_endgame: 0
% 29.19/4.27 stat_given_candidates_h: 0
% 29.19/4.27 stat_binres_derived_cl: 13396
% 29.19/4.27 stat_binres_derived_cl_h: 0
% 29.19/4.27 stat_factor_derived_cl: 2822
% 29.19/4.27 stat_para_derived_cl: 0
% 29.19/4.27 stat_tautologies_discarded: 1
% 29.19/4.27 stat_forward_subsumed: 1728
% 29.19/4.27 stat_derived_cut: 1691
% 29.19/4.27 stat_derived_rewritten: 0
% 29.19/4.27 stat_weight_discarded_building: 0
% 29.19/4.27 stat_weight_discarded_cl: 0
% 29.19/4.27 stat_internlimit_discarded_cl: 0
% 29.19/4.27 stat_simplified: 0 simplified 0 derived 0 given
% 29.19/4.27 stat_kept_cl: 14488
% 29.19/4.27 stat_built_cl: 19570
% 29.19/4.27 stat_hyperres_partial_cl: 0
% 29.19/4.27 stat_made_rewriters: 0
% 29.19/4.27 stat_backward_subsumed: 0
% 29.19/4.27 stat_propagated_subsumed: 0
% 29.19/4.27 stat_clsubs_attempted: 41009
% 29.19/4.27 stat_clsubs_fact_groundunit_found: 11
% 29.19/4.27 stat_clsubs_rule_groundunit_found: 7
% 29.19/4.27 stat_clsubs_top_meta_attempted: 4025805
% 29.19/4.27 stat_clsubs_top_meta_failed: 3984796
% 29.19/4.27 stat_clsubs_top_meta_nonpref_attempted: 4025805
% 29.19/4.27 stat_clsubs_top_meta_nonpref_succeeded: 1956925
% 29.19/4.27 stat_clsubs_top_meta_pref_attempted: 1956925
% 29.19/4.27 stat_clsubs_top_meta_pref1_succeeded: 192428
% 29.19/4.27 stat_clsubs_top_meta_pref2_succeeded: 61803
% 29.19/4.27 stat_clsubs_top_meta_pref3_succeeded: 41009
% 29.19/4.27 stat_clsubs_top_meta_pref_succeeded: 41009
% 29.19/4.27 stat_clsubs_meta_attempted: 95203
% 29.19/4.27 stat_clsubs_meta_failed: 48257
% 29.19/4.27 stat_clsubs_predsymbs_attempted: 0
% 29.19/4.27 stat_clsubs_unit_attempted: 703
% 29.19/4.27 stat_clsubs_full_attempted: 40306
% 29.19/4.27 stat_forwardsubs_attempted: 16217
% 29.19/4.27 stat_lit_hash_added: 1191
% 29.19/4.27 stat_lit_hash_computed: 207290
% 29.19/4.27 stat_lit_hash_match_found: 2589
% 29.19/4.27 stat_lit_hash_match_miss: 311759
% 29.19/4.27 stat_lit_hash_cut_ok: 10
% 29.19/4.27 stat_lit_strong_cut_ok: 1682
% 29.19/4.27 stat_lit_hash_subsume_ok: 1728
% 29.19/4.27 clqueue els 10000000 used 1
% 29.19/4.27 clactive els 10000000 used 2542
% 29.19/4.27 clactivesubsume els 10000000 used 15103
% 29.19/4.27 queue_termbuf els 200000000 used 2331063
% 29.19/4.27 hyper_termbuf els 100000000 used 1
% 29.19/4.27 active_termbuf els 100000000 used 238225
% 29.19/4.27 varstack els 5000 last used 1
% 29.19/4.27 given_termbuf els 10000000 last used 1
% 29.19/4.27 simplified_termbuf els 10000000 last used 1
% 29.19/4.27 derived_termbuf els 10000000 last used 22
% 29.19/4.27 wr_mallocs: 14163
% 29.19/4.27 wr_callocs: 21
% 29.19/4.27 wr_reallocs: 769
% 29.19/4.27 wr_frees: 4
% 29.19/4.27 wr_malloc_bytes: 4163193476
% 29.19/4.27 wr_calloc_bytes: 112065536
% 29.19/4.27 wr_realloc_bytes: 460384
% 29.19/4.27 wr_realloc_freebytes: 0
% 29.19/4.27 ----------------------------------
%------------------------------------------------------------------------------