%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL667+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n004.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 11:12:26 AM UTC 2026
% Result : CounterSatisfiable 26.37s 8.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL667+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.39 % Computer : n004.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Fri Sep 4 12:35:44 UTC 2026
% 0.13/0.40 % CPUTime :
% 26.37/8.91
% 26.37/8.92 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.37/8.92
% 26.37/8.92 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.37/8.93 %$ r1 > p605 > p604 > p603 > p602 > p601 > p505 > p504 > p503 > p502 > p501 > p405 > p404 > p403 > p402 > p401 > p305 > p304 > p303 > p302 > p301 > p205 > p204 > p203 > p202 > p201 > p105 > p104 > p103 > p102 > p101 > #nlpp > #skF_9 > #skF_36 > #skF_25 > #skF_7 > #skF_5 > #skF_44 > #skF_21 > #skF_16 > #skF_2 > #skF_4 > #skF_18 > #skF_24 > #skF_35 > #skF_19 > #skF_31 > #skF_22 > #skF_37 > #skF_40 > #skF_8 > #skF_34 > #skF_29 > #skF_15 > #skF_32 > #skF_28 > #skF_10 > #skF_41 > #skF_38 > #skF_43 > #skF_1 > #skF_39 > #skF_23 > #skF_33 > #skF_26 > #skF_13 > #skF_17 > #skF_3 > #skF_11 > #skF_14 > #skF_48 > #skF_27 > #skF_12 > #skF_49 > #skF_46 > #skF_42 > #skF_50 > #skF_45 > #skF_30 > #skF_6 > #skF_20 > #skF_51 > #skF_47
% 26.37/8.93
% 26.37/8.93 %Foreground sorts:
% 26.37/8.93
% 26.37/8.93
% 26.37/8.93 %Background operators:
% 26.37/8.93
% 26.37/8.93
% 26.37/8.93 %Foreground operators:
% 26.37/8.93 tff('#skF_9', type, '#skF_9': $i > $i).
% 26.37/8.93 tff(p503, type, p503: $i > $o).
% 26.37/8.93 tff('#skF_36', type, '#skF_36': $i > $i).
% 26.37/8.93 tff('#skF_25', type, '#skF_25': $i > $i).
% 26.37/8.93 tff('#skF_7', type, '#skF_7': $i > $i).
% 26.37/8.93 tff('#skF_5', type, '#skF_5': $i > $i).
% 26.37/8.93 tff('#skF_44', type, '#skF_44': $i > $i).
% 26.37/8.93 tff('#skF_21', type, '#skF_21': $i > $i).
% 26.37/8.93 tff('#skF_16', type, '#skF_16': $i > $i).
% 26.37/8.93 tff(p303, type, p303: $i > $o).
% 26.37/8.93 tff('#skF_2', type, '#skF_2': $i > $i).
% 26.37/8.93 tff('#skF_4', type, '#skF_4': $i > $i).
% 26.37/8.93 tff('#skF_18', type, '#skF_18': $i > $i).
% 26.37/8.93 tff(p101, type, p101: $i > $o).
% 26.37/8.93 tff('#skF_24', type, '#skF_24': $i > $i).
% 26.37/8.93 tff('#skF_35', type, '#skF_35': $i > $i).
% 26.37/8.93 tff('#skF_19', type, '#skF_19': $i > $i).
% 26.37/8.93 tff('#skF_31', type, '#skF_31': $i > $i).
% 26.37/8.93 tff(p305, type, p305: $i > $o).
% 26.37/8.93 tff('#skF_22', type, '#skF_22': $i > $i).
% 26.37/8.93 tff('#skF_37', type, '#skF_37': $i > $i).
% 26.37/8.93 tff(p102, type, p102: $i > $o).
% 26.37/8.93 tff(p401, type, p401: $i > $o).
% 26.37/8.93 tff('#skF_40', type, '#skF_40': $i > $i).
% 26.37/8.93 tff('#skF_8', type, '#skF_8': $i > $i).
% 26.37/8.93 tff(p205, type, p205: $i > $o).
% 26.37/8.93 tff(p103, type, p103: $i > $o).
% 26.37/8.93 tff(p304, type, p304: $i > $o).
% 26.37/8.93 tff(p201, type, p201: $i > $o).
% 26.37/8.93 tff(p402, type, p402: $i > $o).
% 26.37/8.93 tff('#skF_34', type, '#skF_34': $i > $i).
% 26.37/8.93 tff('#skF_29', type, '#skF_29': $i > $i).
% 26.37/8.93 tff(p405, type, p405: $i > $o).
% 26.37/8.93 tff('#skF_15', type, '#skF_15': $i > $i).
% 26.37/8.93 tff('#skF_32', type, '#skF_32': $i > $i).
% 26.37/8.93 tff(p403, type, p403: $i > $o).
% 26.37/8.93 tff(p404, type, p404: $i > $o).
% 26.37/8.93 tff(p504, type, p504: $i > $o).
% 26.37/8.93 tff(p601, type, p601: $i > $o).
% 26.37/8.93 tff('#skF_28', type, '#skF_28': $i > $i).
% 26.37/8.93 tff('#skF_10', type, '#skF_10': $i > $i).
% 26.37/8.93 tff('#skF_41', type, '#skF_41': $i > $i).
% 26.37/8.93 tff(p203, type, p203: $i > $o).
% 26.37/8.93 tff('#skF_38', type, '#skF_38': $i > $i).
% 26.37/8.93 tff('#skF_43', type, '#skF_43': $i > $i).
% 26.37/8.93 tff(r1, type, r1: ($i * $i) > $o).
% 26.37/8.93 tff('#skF_1', type, '#skF_1': $i).
% 26.37/8.93 tff(p604, type, p604: $i > $o).
% 26.37/8.93 tff('#skF_39', type, '#skF_39': $i > $i).
% 26.37/8.93 tff('#skF_23', type, '#skF_23': $i > $i).
% 26.37/8.93 tff(p202, type, p202: $i > $o).
% 26.37/8.93 tff('#skF_33', type, '#skF_33': $i > $i).
% 26.37/8.93 tff('#skF_26', type, '#skF_26': $i > $i).
% 26.37/8.93 tff(p105, type, p105: $i > $o).
% 26.37/8.93 tff(p602, type, p602: $i > $o).
% 26.37/8.93 tff('#skF_13', type, '#skF_13': $i > $i).
% 26.37/8.93 tff(p302, type, p302: $i > $o).
% 26.37/8.93 tff('#skF_17', type, '#skF_17': $i > $i).
% 26.37/8.93 tff('#skF_3', type, '#skF_3': $i > $i).
% 26.37/8.93 tff('#skF_11', type, '#skF_11': $i > $i).
% 26.37/8.93 tff('#skF_14', type, '#skF_14': $i > $i).
% 26.37/8.93 tff(p505, type, p505: $i > $o).
% 26.37/8.93 tff('#skF_48', type, '#skF_48': $i > $i).
% 26.37/8.93 tff('#skF_27', type, '#skF_27': $i > $i).
% 26.37/8.93 tff(p104, type, p104: $i > $o).
% 26.37/8.93 tff(p603, type, p603: $i > $o).
% 26.37/8.93 tff('#skF_12', type, '#skF_12': $i > $i).
% 26.37/8.93 tff('#skF_49', type, '#skF_49': $i > $i).
% 26.37/8.93 tff('#skF_46', type, '#skF_46': $i > $i).
% 26.37/8.93 tff('#skF_42', type, '#skF_42': $i > $i).
% 26.37/8.93 tff(p502, type, p502: $i > $o).
% 26.37/8.93 tff('#skF_50', type, '#skF_50': $i > $i).
% 26.37/8.93 tff('#skF_45', type, '#skF_45': $i > $i).
% 26.37/8.93 tff(p204, type, p204: $i > $o).
% 26.37/8.93 tff(p501, type, p501: $i > $o).
% 26.37/8.93 tff('#skF_30', type, '#skF_30': $i > $i).
% 26.37/8.93 tff('#skF_6', type, '#skF_6': $i > $i).
% 26.37/8.93 tff('#skF_20', type, '#skF_20': $i > $i).
% 26.37/8.93 tff('#skF_51', type, '#skF_51': $i > $i).
% 26.37/8.93 tff('#skF_47', type, '#skF_47': $i > $i).
% 26.37/8.93 tff(p605, type, p605: $i > $o).
% 26.37/8.93 tff(p301, type, p301: $i > $o).
% 26.37/8.93
% 26.37/8.93 %Saturated clause set:
% 26.37/8.94 tff(c_48095, plain, (~p302('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_48091, plain, (~p604('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_48087, plain, (~p403('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_48068, plain, (~p605('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_48063, plain, (~p603('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_48048, plain, (~p504('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_48044, plain, (~p403('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_48041, plain, (~p201('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_48027, plain, (~p403('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_48020, plain, (~p402('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47984, plain, (~p302('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47971, plain, (~p504('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47967, plain, (~p301('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47955, plain, (~p602('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47935, plain, (~p602('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47924, plain, (~p302('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47917, plain, (~p401('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47913, plain, (~p502('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47910, plain, (~p605('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47903, plain, (~p503('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47876, plain, (~p605('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47873, plain, (~p402('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47871, plain, (~p201('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47861, plain, (~p601('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47839, plain, (~p502('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47831, plain, (~p301('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47827, plain, (~p504('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47807, plain, (~p501('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47802, plain, (~p604('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47797, plain, (~p501('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47782, plain, (~p503('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47775, plain, (~p603('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47769, plain, (~p301('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47767, plain, (~p601('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47765, plain, (~p604('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47763, plain, (~p201('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47760, plain, (~p601('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47756, plain, (~p401('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47747, plain, (~p602('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47740, plain, (~p402('#skF_46'('#skF_1')))).
% 26.37/8.94 tff(c_47734, plain, (~p502('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47728, plain, (~p401('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47720, plain, (~p503('#skF_29'('#skF_1')))).
% 26.37/8.94 tff(c_47717, plain, (~p603('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47714, plain, (~p501('#skF_34'('#skF_1')))).
% 26.37/8.94 tff(c_47709, plain, (~p402('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47687, plain, (~p403('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47677, plain, (~p602('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47674, plain, (~p605('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47637, plain, (~p504('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47617, plain, (~p201('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47610, plain, (~p502('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47596, plain, (~p301('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47593, plain, (~p402('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47592, plain, (~p403('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47589, plain, (~p502('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47588, plain, (~p403('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47586, plain, (~p601('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47585, plain, (~p502('#skF_12'('#skF_1')))).
% 26.37/8.95 tff(c_47583, plain, (~p403('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47580, plain, (~p201('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47579, plain, (~p504('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47577, plain, (~p401('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47575, plain, (~p603('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47572, plain, (~p604('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47571, plain, (~p605('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47570, plain, (~p504('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47569, plain, (~p302('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47568, plain, (~p402('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47567, plain, (~p504('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47566, plain, (~p604('#skF_12'('#skF_1')))).
% 26.37/8.95 tff(c_47565, plain, (~p504('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47562, plain, (~p302('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47560, plain, (~p302('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47559, plain, (~p301('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47558, plain, (~p504('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47557, plain, (~p201('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47556, plain, (~p605('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47555, plain, (~p604('#skF_3'('#skF_1')))).
% 26.37/8.95 tff(c_47552, plain, (~p403('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47550, plain, (~p602('#skF_35'('#skF_1')))).
% 26.37/8.95 tff(c_47549, plain, (~p604('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47548, plain, (~p605('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47547, plain, (~p302('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47546, plain, (~p402('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47545, plain, (~p603('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47544, plain, (~p402('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47542, plain, (~p301('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47541, plain, (~p403('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47540, plain, (~p401('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47539, plain, (~p402('#skF_19'('#skF_1')))).
% 26.37/8.95 tff(c_47538, plain, (~p503('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47537, plain, (~p302('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47535, plain, (~p503('#skF_6'('#skF_1')))).
% 26.37/8.95 tff(c_47534, plain, (~p602('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47533, plain, (~p503('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47530, plain, (~p403('#skF_20'('#skF_1')))).
% 26.37/8.95 tff(c_47529, plain, (~p503('#skF_11'('#skF_1')))).
% 26.37/8.95 tff(c_47528, plain, (~p502('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47527, plain, (~p604('#skF_17'('#skF_1')))).
% 26.37/8.95 tff(c_47526, plain, (~p502('#skF_35'('#skF_1')))).
% 26.37/8.96 tff(c_47525, plain, (~p502('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47524, plain, (~p604('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47522, plain, (~p402('#skF_35'('#skF_1')))).
% 26.37/8.96 tff(c_47521, plain, (~p603('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47520, plain, (p304('#skF_46'('#skF_1')))).
% 26.37/8.96 tff(c_47519, plain, (~p601('#skF_35'('#skF_1')))).
% 26.37/8.96 tff(c_47518, plain, (~p302('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47516, plain, (~p504('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47515, plain, (~p201('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47514, plain, (~p601('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47512, plain, (~p604('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47513, plain, (p304('#skF_34'('#skF_1')))).
% 26.37/8.96 tff(c_47511, plain, (~p603('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47510, plain, (~p403('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47509, plain, (~p604('#skF_11'('#skF_1')))).
% 26.37/8.96 tff(c_47508, plain, (~p201('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47507, plain, (p304('#skF_29'('#skF_1')))).
% 26.37/8.96 tff(c_47506, plain, (~p602('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47505, plain, (~p201('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47504, plain, (~p501('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47503, plain, (~p502('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47501, plain, (~p302('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47500, plain, (~p501('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47499, plain, (~p605('#skF_35'('#skF_1')))).
% 26.37/8.96 tff(c_47498, plain, (~p201('#skF_11'('#skF_1')))).
% 26.37/8.96 tff(c_47496, plain, (~p602('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47495, plain, (~p602('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47494, plain, (~p602('#skF_17'('#skF_1')))).
% 26.37/8.96 tff(c_47492, plain, (~p402('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47491, plain, (~p503('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47490, plain, (~p602('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47489, plain, (~p401('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47487, plain, (~p601('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47486, plain, (~p504('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47485, plain, (~p502('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47484, plain, (~p605('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47482, plain, (~p603('#skF_11'('#skF_1')))).
% 26.37/8.96 tff(c_47481, plain, (~p603('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47480, plain, (~p501('#skF_17'('#skF_1')))).
% 26.37/8.96 tff(c_47473, plain, (~r1('#skF_1', '#skF_33'('#skF_1')))).
% 26.37/8.96 tff(c_47472, plain, (p203('#skF_34'('#skF_1')))).
% 26.37/8.96 tff(c_47354, plain, (~p503('#skF_19'('#skF_1')))).
% 26.37/8.96 tff(c_47353, plain, (~p301('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47352, plain, (~p503('#skF_35'('#skF_1')))).
% 26.37/8.96 tff(c_47316, plain, (p304('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47315, plain, (p203('#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47203, plain, (r1('#skF_1', '#skF_12'('#skF_1')))).
% 26.37/8.96 tff(c_47202, plain, (~p301('#skF_20'('#skF_1')))).
% 26.37/8.96 tff(c_47195, plain, (~r1('#skF_1', '#skF_45'('#skF_1')))).
% 26.37/8.96 tff(c_47077, plain, (~p401('#skF_6'('#skF_1')))).
% 26.37/8.96 tff(c_47194, plain, (p203('#skF_46'('#skF_1')))).
% 26.37/8.96 tff(c_47076, plain, (~p501('#skF_6'('#skF_1')))).
% 26.37/8.97 tff(c_47039, plain, (p304('#skF_6'('#skF_1')))).
% 26.37/8.97 tff(c_47075, plain, (~p601('#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_47038, plain, (p203('#skF_6'('#skF_1')))).
% 26.37/8.97 tff(c_46926, plain, (r1('#skF_1', '#skF_6'('#skF_1')))).
% 26.37/8.97 tff(c_46925, plain, (~p401('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46924, plain, (~p605('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46923, plain, (~p501('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46887, plain, (p304('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46886, plain, (p203('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46774, plain, (r1('#skF_1', '#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46773, plain, (~p401('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46772, plain, (~p301('#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_46771, plain, (~p601('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46735, plain, (p304('#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_46734, plain, (p203('#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_46622, plain, (r1('#skF_1', '#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_46621, plain, (~p603('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46613, plain, (~r1('#skF_1', '#skF_28'('#skF_1')))).
% 26.37/8.97 tff(c_46614, plain, (~p401('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46494, plain, (~p301('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46612, plain, (p203('#skF_29'('#skF_1')))).
% 26.37/8.97 tff(c_46493, plain, (~p501('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46456, plain, (p304('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46492, plain, (~p201('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46455, plain, (p203('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46343, plain, (r1('#skF_1', '#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46342, plain, (~p301('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46341, plain, (~p501('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46304, plain, (p304('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46340, plain, (~p605('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46303, plain, (p203('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46191, plain, (r1('#skF_1', '#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46190, plain, (~p601('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46154, plain, (p304('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46153, plain, (p203('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46041, plain, (r1('#skF_1', '#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46038, plain, (~p305('#skF_7'('#skF_1')))).
% 26.37/8.97 tff(c_46037, plain, (~p204('#skF_29'('#skF_1')))).
% 26.37/8.97 tff(c_46036, plain, (~p204('#skF_35'('#skF_1')))).
% 26.37/8.97 tff(c_46035, plain, (~p305('#skF_18'('#skF_1')))).
% 26.37/8.97 tff(c_46034, plain, (~p205('#skF_13'('#skF_1')))).
% 26.37/8.97 tff(c_46033, plain, (~p104('#skF_36'('#skF_1')))).
% 26.37/8.97 tff(c_46032, plain, (~p105('#skF_21'('#skF_1')))).
% 26.37/8.97 tff(c_46031, plain, (~p105('#skF_17'('#skF_1')))).
% 26.37/8.97 tff(c_46030, plain, (~p105('#skF_19'('#skF_1')))).
% 26.37/8.97 tff(c_46029, plain, (~p205('#skF_20'('#skF_1')))).
% 26.37/8.97 tff(c_46028, plain, (~p304('#skF_28'('#skF_1')))).
% 26.37/8.97 tff(c_46027, plain, (~p203('#skF_45'('#skF_1')))).
% 26.37/8.97 tff(c_46026, plain, (~p304('#skF_33'('#skF_1')))).
% 26.37/8.97 tff(c_46025, plain, (~p205('#skF_11'('#skF_1')))).
% 26.37/8.97 tff(c_46024, plain, (~p405('#skF_16'('#skF_1')))).
% 26.37/8.97 tff(c_46023, plain, (~p104('#skF_34'('#skF_1')))).
% 26.37/8.97 tff(c_46022, plain, (~p405('#skF_6'('#skF_1')))).
% 26.37/8.97 tff(c_46021, plain, (~p305('#skF_12'('#skF_1')))).
% 26.37/8.97 tff(c_46020, plain, (~p405('#skF_10'('#skF_1')))).
% 26.37/8.97 tff(c_46006, plain, (p203('#skF_15'('#skF_1')))).
% 26.37/8.97 tff(c_46012, plain, (p203('#skF_9'('#skF_1')))).
% 26.37/8.97 tff(c_46018, plain, (p203('#skF_3'('#skF_1')))).
% 26.37/8.97 tff(c_45976, plain, (p203('#skF_5'('#skF_1')))).
% 26.37/8.97 tff(c_45958, plain, (p203('#skF_47'('#skF_1')))).
% 26.37/8.97 tff(c_46019, plain, (p203('#skF_1'))).
% 26.37/8.98 tff(c_45593, plain, (![Y_169]: (p203(Y_169) | ~r1('#skF_1', Y_169)))).
% 26.37/8.98 tff(c_45592, plain, (~p103('#skF_46'('#skF_1')))).
% 26.37/8.98 tff(c_45146, plain, (p304('#skF_9'('#skF_1')))).
% 26.37/8.98 tff(c_45152, plain, (p304('#skF_3'('#skF_1')))).
% 26.37/8.98 tff(c_45591, plain, (p101('#skF_1'))).
% 26.37/8.98 tff(c_45140, plain, (p304('#skF_15'('#skF_1')))).
% 26.37/8.98 tff(c_45110, plain, (p304('#skF_5'('#skF_1')))).
% 26.37/8.98 tff(c_45092, plain, (p304('#skF_47'('#skF_1')))).
% 26.37/8.98 tff(c_45153, plain, (p304('#skF_1'))).
% 26.37/8.98 tff(c_44727, plain, (![Y_166]: (p304(Y_166) | ~r1('#skF_1', Y_166)))).
% 26.37/8.98 tff(c_44285, plain, (~p602('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_44287, plain, (p404('#skF_1'))).
% 26.37/8.98 tff(c_44038, plain, (~p503('#skF_3'('#skF_1')))).
% 26.37/8.98 tff(c_152, plain, (![Y_113]: (r1(Y_113, '#skF_35'(Y_113)) | r1(Y_113, '#skF_36'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_44035, plain, (~p402('#skF_27'('#skF_1')))).
% 26.37/8.98 tff(c_252, plain, (![Y_113]: (r1(Y_113, '#skF_10'(Y_113)) | r1(Y_113, '#skF_11'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_160, plain, (![Y_113]: (r1(Y_113, '#skF_33'(Y_113)) | r1(Y_113, '#skF_34'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_43540, plain, (~p602('#skF_24'('#skF_1')))).
% 26.37/8.98 tff(c_112, plain, (![Y_113]: (r1(Y_113, '#skF_45'(Y_113)) | r1(Y_113, '#skF_46'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_228, plain, (![Y_113]: (r1(Y_113, '#skF_16'(Y_113)) | r1(Y_113, '#skF_17'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_43047, plain, (~p603('#skF_24'('#skF_1')))).
% 26.37/8.98 tff(c_43046, plain, (~p402('#skF_24'('#skF_1')))).
% 26.37/8.98 tff(c_220, plain, (![Y_113]: (r1(Y_113, '#skF_18'(Y_113)) | r1(Y_113, '#skF_19'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_42799, plain, (~p502('#skF_24'('#skF_1')))).
% 26.37/8.98 tff(c_212, plain, (![Y_113]: (r1(Y_113, '#skF_20'(Y_113)) | r1(Y_113, '#skF_21'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_42552, plain, (~p604('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_42551, plain, (~p502('#skF_27'('#skF_1')))).
% 26.37/8.98 tff(c_244, plain, (![Y_113]: (r1(Y_113, '#skF_12'(Y_113)) | r1(Y_113, '#skF_13'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_268, plain, (![Y_113]: (r1(Y_113, '#skF_6'(Y_113)) | r1(Y_113, '#skF_7'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_42058, plain, (~p402('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_180, plain, (![Y_113]: (r1(Y_113, '#skF_28'(Y_113)) | r1(Y_113, '#skF_29'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_240, plain, (![Y_113]: (r1(Y_113, '#skF_12'(Y_113)) | ~p205('#skF_13'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_41565, plain, (~p301('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_41564, plain, (~p503('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_224, plain, (![Y_113]: (r1(Y_113, '#skF_16'(Y_113)) | ~p105('#skF_17'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_41317, plain, (~p501('#skF_24'('#skF_1')))).
% 26.37/8.98 tff(c_41070, plain, (~p501('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_226, plain, (![Y_113]: (~p405('#skF_16'(Y_113)) | r1(Y_113, '#skF_17'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.98 tff(c_41069, plain, (~p603('#skF_32'('#skF_1')))).
% 26.37/8.98 tff(c_250, plain, (![Y_113]: (~p405('#skF_10'(Y_113)) | r1(Y_113, '#skF_11'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_40822, plain, (~p603('#skF_27'('#skF_1')))).
% 26.37/8.99 tff(c_40819, plain, (~p601('#skF_27'('#skF_1')))).
% 26.37/8.99 tff(c_40818, plain, (~p601('#skF_3'('#skF_1')))).
% 26.37/8.99 tff(c_248, plain, (![Y_113]: (r1(Y_113, '#skF_10'(Y_113)) | ~p205('#skF_11'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_40569, plain, (~p601('#skF_32'('#skF_1')))).
% 26.37/8.99 tff(c_158, plain, (![Y_113]: (~p304('#skF_33'(Y_113)) | r1(Y_113, '#skF_34'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_40322, plain, (~p504('#skF_32'('#skF_1')))).
% 26.37/8.99 tff(c_40321, plain, (~p303('#skF_1'))).
% 26.37/8.99 tff(c_266, plain, (![Y_113]: (~p405('#skF_6'(Y_113)) | r1(Y_113, '#skF_7'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_40074, plain, (~p601('#skF_24'('#skF_1')))).
% 26.37/8.99 tff(c_178, plain, (![Y_113]: (~p304('#skF_28'(Y_113)) | r1(Y_113, '#skF_29'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_39825, plain, (~p502('#skF_32'('#skF_1')))).
% 26.37/8.99 tff(c_39824, plain, (~p302('#skF_3'('#skF_1')))).
% 26.37/8.99 tff(c_110, plain, (![Y_113]: (~p203('#skF_45'(Y_113)) | r1(Y_113, '#skF_46'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_39575, plain, (~p302('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_39328, plain, (~p403('#skF_15'('#skF_1')))).
% 26.37/8.99 tff(c_150, plain, (![Y_113]: (~p204('#skF_35'(Y_113)) | r1(Y_113, '#skF_36'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_39327, plain, (~p504('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_210, plain, (![Y_113]: (~p205('#skF_20'(Y_113)) | r1(Y_113, '#skF_21'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_39080, plain, (~p503('#skF_9'('#skF_1')))).
% 26.37/8.99 tff(c_218, plain, (![Y_113]: (~p305('#skF_18'(Y_113)) | r1(Y_113, '#skF_19'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_156, plain, (![Y_113]: (r1(Y_113, '#skF_33'(Y_113)) | ~p104('#skF_34'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_176, plain, (![Y_113]: (r1(Y_113, '#skF_28'(Y_113)) | ~p204('#skF_29'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_148, plain, (![Y_113]: (r1(Y_113, '#skF_35'(Y_113)) | ~p104('#skF_36'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_38093, plain, (~p402('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_264, plain, (![Y_113]: (r1(Y_113, '#skF_6'(Y_113)) | ~p305('#skF_7'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_37846, plain, (~p302('#skF_15'('#skF_1')))).
% 26.37/8.99 tff(c_208, plain, (![Y_113]: (r1(Y_113, '#skF_20'(Y_113)) | ~p105('#skF_21'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_37599, plain, (~p403('#skF_9'('#skF_1')))).
% 26.37/8.99 tff(c_216, plain, (![Y_113]: (r1(Y_113, '#skF_18'(Y_113)) | ~p105('#skF_19'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_108, plain, (![Y_113]: (r1(Y_113, '#skF_45'(Y_113)) | ~p103('#skF_46'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_37106, plain, (~p602('#skF_9'('#skF_1')))).
% 26.37/8.99 tff(c_242, plain, (![Y_113]: (~p305('#skF_12'(Y_113)) | r1(Y_113, '#skF_13'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_192, plain, (![Y_113]: (r1(Y_113, '#skF_25'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_36613, plain, (~p503('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_36611, plain, (~p604('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_214, plain, (![Y_113]: (~p305('#skF_18'(Y_113)) | ~p105('#skF_19'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_36364, plain, (~p502('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_284, plain, (![Y_113]: (r1(Y_113, '#skF_2'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_36363, plain, (~p602('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_36362, plain, (~p403('#skF_5'('#skF_1')))).
% 26.37/8.99 tff(c_236, plain, (![Y_113]: (r1(Y_113, '#skF_14'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_36115, plain, (~p602('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_106, plain, (![Y_113]: (~p203('#skF_45'(Y_113)) | ~p103('#skF_46'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_238, plain, (![Y_113]: (~p305('#skF_12'(Y_113)) | ~p205('#skF_13'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35866, plain, (~p502('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_188, plain, (![Y_113]: (r1(Y_113, '#skF_26'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35865, plain, (~p403('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_196, plain, (![Y_113]: (r1(Y_113, '#skF_24'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35618, plain, (~p504('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_146, plain, (![Y_113]: (~p204('#skF_35'(Y_113)) | ~p104('#skF_36'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35616, plain, (~p402('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_35614, plain, (~p501('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_246, plain, (![Y_113]: (~p405('#skF_10'(Y_113)) | ~p205('#skF_11'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35612, plain, (~p605('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_206, plain, (![Y_113]: (~p205('#skF_20'(Y_113)) | ~p105('#skF_21'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35611, plain, (~p201('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_120, plain, (![Y_113]: (r1(Y_113, '#skF_43'(Y_113)) | ~p403(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35118, plain, (~p503('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_132, plain, (![Y_113]: (r1(Y_113, '#skF_40'(Y_113)) | ~p303(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/8.99 tff(c_35117, plain, (~p604('#skF_47'('#skF_1')))).
% 26.37/8.99 tff(c_35116, plain, (~p302('#skF_47'('#skF_1')))).
% 26.37/9.00 tff(c_140, plain, (![Y_113]: (r1(Y_113, '#skF_38'(Y_113)) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_200, plain, (![Y_113]: (r1(Y_113, '#skF_23'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_34623, plain, (~p301('#skF_47'('#skF_1')))).
% 26.37/9.00 tff(c_34622, plain, (~p401('#skF_47'('#skF_1')))).
% 26.37/9.00 tff(c_34620, plain, (~p603('#skF_47'('#skF_1')))).
% 26.37/9.00 tff(c_222, plain, (![Y_113]: (~p405('#skF_16'(Y_113)) | ~p105('#skF_17'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_34619, plain, (~p601('#skF_47'('#skF_1')))).
% 26.37/9.00 tff(c_104, plain, (![Y_113]: (r1(Y_113, '#skF_47'(Y_113)) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_34372, plain, (~p501('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_34371, plain, (~p603('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_34124, plain, (~p201('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_124, plain, (![Y_113]: (r1(Y_113, '#skF_42'(Y_113)) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_136, plain, (![Y_113]: (r1(Y_113, '#skF_39'(Y_113)) | ~p403(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_33877, plain, (~p401('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_33876, plain, (~p601('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_128, plain, (![Y_113]: (r1(Y_113, '#skF_41'(Y_113)) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_164, plain, (![Y_113]: (r1(Y_113, '#skF_32'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_33383, plain, (~p301('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_33382, plain, (~p605('#skF_5'('#skF_1')))).
% 26.37/9.00 tff(c_33135, plain, (~p201('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_88, plain, (![Y_113]: (r1(Y_113, '#skF_51'(Y_113)) | ~p202(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_32888, plain, (~p201('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_272, plain, (![Y_113]: (r1(Y_113, '#skF_5'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_32887, plain, (~p502('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_32885, plain, (~p602('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_174, plain, (![Y_113]: (~p304('#skF_28'(Y_113)) | ~p204('#skF_29'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_32884, plain, (~p402('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_116, plain, (![Y_113]: (r1(Y_113, '#skF_44'(Y_113)) | ~p303(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_32637, plain, (~p302('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_32636, plain, (~p601('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_32389, plain, (~p301('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_168, plain, (![Y_113]: (r1(Y_113, '#skF_31'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_154, plain, (![Y_113]: (~p304('#skF_33'(Y_113)) | ~p104('#skF_34'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_32387, plain, (~p504('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_32140, plain, (~p504('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_144, plain, (![Y_113]: (r1(Y_113, '#skF_37'(Y_113)) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_31893, plain, (~p604('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_260, plain, (![Y_113]: (r1(Y_113, '#skF_8'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_31892, plain, (~p503('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_92, plain, (![Y_113]: (r1(Y_113, '#skF_50'(Y_113)) | ~p302(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_31645, plain, (~p301('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_204, plain, (![Y_113]: (r1(Y_113, '#skF_22'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_31398, plain, (~p604('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_31397, plain, (~p603('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_31150, plain, (~p601('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_100, plain, (![Y_113]: (r1(Y_113, '#skF_48'(Y_113)) | ~p502(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_96, plain, (![Y_113]: (r1(Y_113, '#skF_49'(Y_113)) | ~p402(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_30903, plain, (~p401('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_30902, plain, (~p605('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_30655, plain, (~p501('#skF_15'('#skF_1')))).
% 26.37/9.00 tff(c_276, plain, (![Y_113]: (r1(Y_113, '#skF_4'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_30408, plain, (~p502('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_232, plain, (![Y_113]: (r1(Y_113, '#skF_15'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_30407, plain, (~p402('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_30160, plain, (~p603('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_172, plain, (![Y_113]: (r1(Y_113, '#skF_30'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_30159, plain, (~p401('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_262, plain, (![Y_113]: (~p405('#skF_6'(Y_113)) | ~p305('#skF_7'(Y_113)) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_30157, plain, (~p501('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_30156, plain, (~p605('#skF_9'('#skF_1')))).
% 26.37/9.00 tff(c_29909, plain, (~p605('#skF_27'('#skF_1')))).
% 26.37/9.00 tff(c_256, plain, (![Y_113]: (r1(Y_113, '#skF_9'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_29908, plain, (~p501('#skF_3'('#skF_1')))).
% 26.37/9.00 tff(c_184, plain, (![Y_113]: (r1(Y_113, '#skF_27'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.00 tff(c_29659, plain, (~p603('#skF_3'('#skF_1')))).
% 26.37/9.00 tff(c_29656, plain, (~p401('#skF_3'('#skF_1')))).
% 26.37/9.00 tff(c_29655, plain, (p505('#skF_1'))).
% 26.37/9.01 tff(c_280, plain, (![Y_113]: (r1(Y_113, '#skF_3'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_282, plain, (![Y_113]: (~p405('#skF_2'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_98, plain, (![Y_113]: (~p102('#skF_48'(Y_113)) | ~p502(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_102, plain, (![Y_113]: (~p102('#skF_47'(Y_113)) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_194, plain, (![Y_113]: (~p304('#skF_24'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_198, plain, (![Y_113]: (~p304('#skF_23'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_94, plain, (![Y_113]: (~p102('#skF_49'(Y_113)) | ~p402(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_274, plain, (![Y_113]: (~p305('#skF_4'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_186, plain, (![Y_113]: (~p204('#skF_26'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_118, plain, (![Y_113]: (~p103('#skF_43'(Y_113)) | ~p403(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_122, plain, (![Y_113]: (~p103('#skF_42'(Y_113)) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_114, plain, (![Y_113]: (~p103('#skF_44'(Y_113)) | ~p303(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_126, plain, (![Y_113]: (~p103('#skF_41'(Y_113)) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_202, plain, (![Y_113]: (~p304('#skF_22'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_234, plain, (![Y_113]: (~p105('#skF_14'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_90, plain, (![Y_113]: (~p102('#skF_50'(Y_113)) | ~p302(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_162, plain, (![Y_113]: (~p104('#skF_32'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_182, plain, (![Y_113]: (~p204('#skF_27'(Y_113)) | p404(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_130, plain, (![Y_113]: (~p203('#skF_40'(Y_113)) | ~p303(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_230, plain, (![Y_113]: (~p105('#skF_15'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_134, plain, (![Y_113]: (~p203('#skF_39'(Y_113)) | ~p403(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_86, plain, (![Y_113]: (~p102('#skF_51'(Y_113)) | ~p202(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_138, plain, (![Y_113]: (~p203('#skF_38'(Y_113)) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_190, plain, (![Y_113]: (~p204('#skF_25'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_254, plain, (![Y_113]: (~p205('#skF_9'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_270, plain, (![Y_113]: (~p305('#skF_5'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_142, plain, (![Y_113]: (~p203('#skF_37'(Y_113)) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_258, plain, (![Y_113]: (~p205('#skF_8'(Y_113)) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_170, plain, (![Y_113]: (~p104('#skF_30'(Y_113)) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_166, plain, (![Y_113]: (~p104('#skF_31'(Y_113)) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_278, plain, (![Y_113]: (~p405('#skF_3'(Y_113)) | ~p505(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_42, plain, (![Y_113]: (~p401(Y_113) | ~p601(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_60, plain, (![Y_113]: (~p402(Y_113) | ~p502(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_62, plain, (![Y_113]: (~p402(Y_113) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_58, plain, (![Y_113]: (~p302(Y_113) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_44, plain, (![Y_113]: (~p501(Y_113) | ~p601(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_50, plain, (![Y_113]: (~p202(Y_113) | ~p502(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_17708, plain, (~p202('#skF_1'))).
% 26.37/9.01 tff(c_52, plain, (![Y_113]: (~p202(Y_113) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_56, plain, (![Y_113]: (~p302(Y_113) | ~p502(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_36, plain, (![Y_113]: (~p301(Y_113) | ~p501(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_17688, plain, (~p403('#skF_1'))).
% 26.37/9.01 tff(c_66, plain, (![Y_113]: (~p303(Y_113) | ~p403(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_17681, plain, (~p402('#skF_1'))).
% 26.37/9.01 tff(c_54, plain, (![Y_113]: (~p302(Y_113) | ~p402(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_48, plain, (![Y_113]: (~p202(Y_113) | ~p402(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_17668, plain, (p602('#skF_1'))).
% 26.37/9.01 tff(c_17667, plain, (~p502('#skF_1'))).
% 26.37/9.01 tff(c_64, plain, (![Y_113]: (~p502(Y_113) | ~p602(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_40, plain, (![Y_113]: (~p401(Y_113) | ~p501(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_70, plain, (![Y_113]: (~p303(Y_113) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_34, plain, (![Y_113]: (~p301(Y_113) | ~p401(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_32, plain, (![Y_113]: (~p201(Y_113) | ~p601(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_398, plain, (~p302('#skF_1'))).
% 26.37/9.01 tff(c_68, plain, (![Y_113]: (~p303(Y_113) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_46, plain, (![Y_113]: (~p202(Y_113) | ~p302(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_385, plain, (~p503('#skF_1'))).
% 26.37/9.01 tff(c_38, plain, (![Y_113]: (~p301(Y_113) | ~p601(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_72, plain, (![Y_113]: (~p403(Y_113) | ~p503(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_378, plain, (~p504('#skF_1'))).
% 26.37/9.01 tff(c_78, plain, (![Y_113]: (p404(Y_113) | ~p504(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_80, plain, (![Y_113]: (p404(Y_113) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_20, plain, (![Y_113]: (~p101(Y_113) | ~p401(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_22, plain, (![Y_113]: (~p101(Y_113) | ~p501(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.01 tff(c_347, plain, (~p604('#skF_1'))).
% 26.37/9.02 tff(c_18, plain, (![Y_113]: (~p101(Y_113) | ~p301(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_82, plain, (![Y_113]: (~p504(Y_113) | ~p604(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_340, plain, (~p201('#skF_1'))).
% 26.37/9.02 tff(c_16, plain, (![Y_113]: (~p101(Y_113) | ~p201(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_76, plain, (![Y_113]: (~p503(Y_113) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_327, plain, (~p601('#skF_1'))).
% 26.37/9.02 tff(c_320, plain, (~p603('#skF_1'))).
% 26.37/9.02 tff(c_24, plain, (![Y_113]: (~p101(Y_113) | ~p601(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_74, plain, (![Y_113]: (~p403(Y_113) | ~p603(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_313, plain, (~p401('#skF_1'))).
% 26.37/9.02 tff(c_306, plain, (~p301('#skF_1'))).
% 26.37/9.02 tff(c_28, plain, (![Y_113]: (~p201(Y_113) | ~p401(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_305, plain, (~p501('#skF_1'))).
% 26.37/9.02 tff(c_26, plain, (![Y_113]: (~p201(Y_113) | ~p301(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_30, plain, (![Y_113]: (~p201(Y_113) | ~p501(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_292, plain, (~p605('#skF_1'))).
% 26.37/9.02 tff(c_84, plain, (![Y_113]: (~p505(Y_113) | ~p605(Y_113) | ~r1('#skF_1', Y_113)))).
% 26.37/9.02 tff(c_2, plain, (![X_1]: (r1(X_1, X_1)))).
% 26.37/9.02 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.37/9.02
%------------------------------------------------------------------------------