%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL649+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n027.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:20 AM UTC 2026
% Result : CounterSatisfiable 15.40s 4.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL649+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.10/0.43 % Computer : n027.cluster.edu
% 0.10/0.43 % Model : x86_64 x86_64
% 0.10/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.43 % Memory : 8046.5625MB
% 0.10/0.43 % OS : Linux 6.8.0-71-generic
% 0.10/0.43 % CPULimit : 300
% 0.10/0.43 % WCLimit : 300
% 0.10/0.43 % DateTime : Sat Sep 5 15:03:28 UTC 2026
% 0.10/0.44 % CPUTime :
% 15.40/4.70
% 15.40/4.70 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.40/4.70
% 15.40/4.70 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.40/4.71 %$ 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_52 > #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
% 15.40/4.71
% 15.40/4.71 %Foreground sorts:
% 15.40/4.71
% 15.40/4.71
% 15.40/4.71 %Background operators:
% 15.40/4.71
% 15.40/4.71
% 15.40/4.71 %Foreground operators:
% 15.40/4.71 tff('#skF_9', type, '#skF_9': $i > $i).
% 15.40/4.71 tff(p503, type, p503: $i > $o).
% 15.40/4.71 tff('#skF_36', type, '#skF_36': $i > $i).
% 15.40/4.71 tff('#skF_25', type, '#skF_25': $i > $i).
% 15.40/4.71 tff('#skF_7', type, '#skF_7': $i > $i).
% 15.40/4.71 tff('#skF_5', type, '#skF_5': $i > $i).
% 15.40/4.71 tff('#skF_52', type, '#skF_52': $i).
% 15.40/4.71 tff('#skF_44', type, '#skF_44': $i > $i).
% 15.40/4.71 tff('#skF_21', type, '#skF_21': $i > $i).
% 15.40/4.71 tff('#skF_16', type, '#skF_16': $i > $i).
% 15.40/4.71 tff(p303, type, p303: $i > $o).
% 15.40/4.71 tff('#skF_2', type, '#skF_2': $i > $i).
% 15.40/4.71 tff('#skF_4', type, '#skF_4': $i > $i).
% 15.40/4.71 tff('#skF_18', type, '#skF_18': $i > $i).
% 15.40/4.71 tff(p101, type, p101: $i > $o).
% 15.40/4.71 tff('#skF_24', type, '#skF_24': $i > $i).
% 15.40/4.71 tff('#skF_35', type, '#skF_35': $i > $i).
% 15.40/4.71 tff('#skF_19', type, '#skF_19': $i > $i).
% 15.40/4.71 tff('#skF_31', type, '#skF_31': $i > $i).
% 15.40/4.71 tff(p305, type, p305: $i > $o).
% 15.40/4.71 tff('#skF_22', type, '#skF_22': $i > $i).
% 15.40/4.71 tff('#skF_37', type, '#skF_37': $i > $i).
% 15.40/4.71 tff(p102, type, p102: $i > $o).
% 15.40/4.71 tff(p401, type, p401: $i > $o).
% 15.40/4.71 tff('#skF_40', type, '#skF_40': $i > $i).
% 15.40/4.71 tff('#skF_8', type, '#skF_8': $i > $i).
% 15.40/4.71 tff(p205, type, p205: $i > $o).
% 15.40/4.71 tff(p103, type, p103: $i > $o).
% 15.40/4.71 tff(p304, type, p304: $i > $o).
% 15.40/4.71 tff(p201, type, p201: $i > $o).
% 15.40/4.71 tff(p402, type, p402: $i > $o).
% 15.40/4.71 tff('#skF_34', type, '#skF_34': $i > $i).
% 15.40/4.71 tff('#skF_29', type, '#skF_29': $i > $i).
% 15.40/4.71 tff(p405, type, p405: $i > $o).
% 15.40/4.71 tff('#skF_15', type, '#skF_15': $i > $i).
% 15.40/4.71 tff('#skF_32', type, '#skF_32': $i > $i).
% 15.40/4.71 tff(p403, type, p403: $i > $o).
% 15.40/4.71 tff(p404, type, p404: $i > $o).
% 15.40/4.71 tff(p504, type, p504: $i > $o).
% 15.40/4.71 tff(p601, type, p601: $i > $o).
% 15.40/4.71 tff('#skF_28', type, '#skF_28': $i > $i).
% 15.40/4.71 tff('#skF_10', type, '#skF_10': $i > $i).
% 15.40/4.71 tff('#skF_41', type, '#skF_41': $i > $i).
% 15.40/4.71 tff(p203, type, p203: $i > $o).
% 15.40/4.71 tff('#skF_38', type, '#skF_38': $i > $i).
% 15.40/4.71 tff('#skF_43', type, '#skF_43': $i > $i).
% 15.40/4.71 tff(r1, type, r1: ($i * $i) > $o).
% 15.40/4.71 tff('#skF_1', type, '#skF_1': $i).
% 15.40/4.71 tff(p604, type, p604: $i > $o).
% 15.40/4.71 tff('#skF_39', type, '#skF_39': $i > $i).
% 15.40/4.71 tff('#skF_23', type, '#skF_23': $i > $i).
% 15.40/4.71 tff(p202, type, p202: $i > $o).
% 15.40/4.71 tff('#skF_33', type, '#skF_33': $i > $i).
% 15.40/4.71 tff('#skF_26', type, '#skF_26': $i > $i).
% 15.40/4.71 tff(p105, type, p105: $i > $o).
% 15.40/4.71 tff(p602, type, p602: $i > $o).
% 15.40/4.71 tff('#skF_13', type, '#skF_13': $i > $i).
% 15.40/4.71 tff(p302, type, p302: $i > $o).
% 15.40/4.71 tff('#skF_17', type, '#skF_17': $i > $i).
% 15.40/4.71 tff('#skF_3', type, '#skF_3': $i > $i).
% 15.40/4.71 tff('#skF_11', type, '#skF_11': $i > $i).
% 15.40/4.71 tff('#skF_14', type, '#skF_14': $i > $i).
% 15.40/4.71 tff(p505, type, p505: $i > $o).
% 15.40/4.71 tff('#skF_48', type, '#skF_48': $i > $i).
% 15.40/4.71 tff('#skF_27', type, '#skF_27': $i > $i).
% 15.40/4.71 tff(p104, type, p104: $i > $o).
% 15.40/4.71 tff(p603, type, p603: $i > $o).
% 15.40/4.71 tff('#skF_12', type, '#skF_12': $i > $i).
% 15.40/4.71 tff('#skF_49', type, '#skF_49': $i > $i).
% 15.40/4.71 tff('#skF_46', type, '#skF_46': $i > $i).
% 15.40/4.71 tff('#skF_42', type, '#skF_42': $i > $i).
% 15.40/4.71 tff(p502, type, p502: $i > $o).
% 15.40/4.71 tff('#skF_50', type, '#skF_50': $i > $i).
% 15.40/4.71 tff('#skF_45', type, '#skF_45': $i > $i).
% 15.40/4.71 tff(p204, type, p204: $i > $o).
% 15.40/4.71 tff(p501, type, p501: $i > $o).
% 15.40/4.71 tff('#skF_30', type, '#skF_30': $i > $i).
% 15.40/4.71 tff('#skF_6', type, '#skF_6': $i > $i).
% 15.40/4.71 tff('#skF_20', type, '#skF_20': $i > $i).
% 15.40/4.71 tff('#skF_51', type, '#skF_51': $i > $i).
% 15.40/4.71 tff('#skF_47', type, '#skF_47': $i > $i).
% 15.40/4.71 tff(p605, type, p605: $i > $o).
% 15.40/4.71 tff(p301, type, p301: $i > $o).
% 15.40/4.71
% 15.40/4.71 %Saturated clause set:
% 15.40/4.71 tff(c_18190, plain, (p204('#skF_20'('#skF_52')))).
% 15.40/4.71 tff(c_18186, plain, (r1('#skF_52', '#skF_20'('#skF_52')))).
% 15.40/4.71 tff(c_18185, plain, (p204('#skF_6'('#skF_52')))).
% 15.40/4.71 tff(c_18181, plain, (r1('#skF_52', '#skF_6'('#skF_52')))).
% 15.40/4.71 tff(c_18180, plain, (p204('#skF_45'('#skF_52')))).
% 15.40/4.71 tff(c_18176, plain, (r1('#skF_52', '#skF_45'('#skF_52')))).
% 15.40/4.71 tff(c_18175, plain, (p204('#skF_28'('#skF_52')))).
% 15.40/4.71 tff(c_18171, plain, (r1('#skF_52', '#skF_28'('#skF_52')))).
% 15.40/4.71 tff(c_18170, plain, (p204('#skF_17'('#skF_52')))).
% 15.40/4.71 tff(c_18166, plain, (r1('#skF_52', '#skF_17'('#skF_52')))).
% 15.40/4.71 tff(c_18165, plain, (p204('#skF_33'('#skF_52')))).
% 15.40/4.71 tff(c_18161, plain, (r1('#skF_52', '#skF_33'('#skF_52')))).
% 15.40/4.71 tff(c_18154, plain, (~r1('#skF_52', '#skF_35'('#skF_52')))).
% 15.40/4.71 tff(c_18153, plain, (p204('#skF_36'('#skF_52')))).
% 15.40/4.71 tff(c_18144, plain, (p204('#skF_19'('#skF_52')))).
% 15.40/4.71 tff(c_18140, plain, (r1('#skF_52', '#skF_19'('#skF_52')))).
% 15.40/4.71 tff(c_18139, plain, (p204('#skF_12'('#skF_52')))).
% 15.40/4.71 tff(c_18135, plain, (r1('#skF_52', '#skF_12'('#skF_52')))).
% 15.40/4.71 tff(c_18134, plain, (p204('#skF_11'('#skF_52')))).
% 15.40/4.71 tff(c_18130, plain, (r1('#skF_52', '#skF_11'('#skF_52')))).
% 15.40/4.71 tff(c_18129, plain, (~p204('#skF_35'('#skF_52')))).
% 15.40/4.71 tff(c_18128, plain, (~p205('#skF_20'('#skF_52')))).
% 15.40/4.71 tff(c_18127, plain, (~p205('#skF_11'('#skF_52')))).
% 15.40/4.71 tff(c_18126, plain, (~p305('#skF_18'('#skF_52')))).
% 15.40/4.71 tff(c_18125, plain, (~p203('#skF_45'('#skF_52')))).
% 15.40/4.71 tff(c_18124, plain, (~p105('#skF_19'('#skF_52')))).
% 15.40/4.71 tff(c_18123, plain, (~p304('#skF_28'('#skF_52')))).
% 15.40/4.71 tff(c_18122, plain, (~p104('#skF_36'('#skF_52')))).
% 15.40/4.71 tff(c_18121, plain, (~p405('#skF_6'('#skF_52')))).
% 15.40/4.71 tff(c_18120, plain, (~p105('#skF_21'('#skF_52')))).
% 15.40/4.71 tff(c_18119, plain, (~p405('#skF_16'('#skF_52')))).
% 15.40/4.71 tff(c_18118, plain, (~p104('#skF_34'('#skF_52')))).
% 15.40/4.71 tff(c_18117, plain, (~p103('#skF_46'('#skF_52')))).
% 15.40/4.71 tff(c_18116, plain, (~p304('#skF_33'('#skF_52')))).
% 15.40/4.71 tff(c_18115, plain, (~p305('#skF_12'('#skF_52')))).
% 15.40/4.71 tff(c_18114, plain, (~p105('#skF_17'('#skF_52')))).
% 15.40/4.71 tff(c_18113, plain, (~p405('#skF_10'('#skF_52')))).
% 15.40/4.71 tff(c_18112, plain, (~p305('#skF_7'('#skF_52')))).
% 15.40/4.71 tff(c_18111, plain, (~p205('#skF_13'('#skF_52')))).
% 15.40/4.71 tff(c_18110, plain, (~p204('#skF_29'('#skF_52')))).
% 15.40/4.71 tff(c_18066, plain, (p204('#skF_44'('#skF_52')))).
% 15.40/4.71 tff(c_18057, plain, (p204('#skF_15'('#skF_52')))).
% 15.40/4.71 tff(c_18072, plain, (p204('#skF_9'('#skF_52')))).
% 15.40/4.71 tff(c_18075, plain, (p204('#skF_3'('#skF_52')))).
% 15.40/4.71 tff(c_18081, plain, (p204('#skF_5'('#skF_52')))).
% 15.40/4.71 tff(c_18084, plain, (p204('#skF_47'('#skF_52')))).
% 15.40/4.71 tff(c_18021, plain, (p204('#skF_40'('#skF_52')))).
% 15.40/4.71 tff(c_18109, plain, (p101('#skF_52'))).
% 15.40/4.72 tff(c_17687, plain, (![X_188]: (p204(X_188) | ~r1('#skF_52', X_188)))).
% 15.40/4.72 tff(c_16825, plain, (p303('#skF_52'))).
% 15.40/4.72 tff(c_16823, plain, (p404('#skF_52'))).
% 15.40/4.72 tff(c_16821, plain, (~r1('#skF_1', '#skF_1'))).
% 15.40/4.72 tff(c_252, plain, (![Y_123]: (r1(Y_123, '#skF_10'(Y_123)) | r1(Y_123, '#skF_11'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_112, plain, (![Y_123]: (r1(Y_123, '#skF_45'(Y_123)) | r1(Y_123, '#skF_46'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_212, plain, (![Y_123]: (r1(Y_123, '#skF_20'(Y_123)) | r1(Y_123, '#skF_21'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_268, plain, (![Y_123]: (r1(Y_123, '#skF_6'(Y_123)) | r1(Y_123, '#skF_7'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_180, plain, (![Y_123]: (r1(Y_123, '#skF_28'(Y_123)) | r1(Y_123, '#skF_29'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_152, plain, (![Y_123]: (r1(Y_123, '#skF_35'(Y_123)) | r1(Y_123, '#skF_36'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_220, plain, (![Y_123]: (r1(Y_123, '#skF_18'(Y_123)) | r1(Y_123, '#skF_19'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_228, plain, (![Y_123]: (r1(Y_123, '#skF_16'(Y_123)) | r1(Y_123, '#skF_17'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_160, plain, (![Y_123]: (r1(Y_123, '#skF_33'(Y_123)) | r1(Y_123, '#skF_34'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_244, plain, (![Y_123]: (r1(Y_123, '#skF_12'(Y_123)) | r1(Y_123, '#skF_13'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_158, plain, (![Y_123]: (~p304('#skF_33'(Y_123)) | r1(Y_123, '#skF_34'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_156, plain, (![Y_123]: (r1(Y_123, '#skF_33'(Y_123)) | ~p104('#skF_34'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_216, plain, (![Y_123]: (r1(Y_123, '#skF_18'(Y_123)) | ~p105('#skF_19'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_14532, plain, (p505('#skF_52'))).
% 15.40/4.72 tff(c_110, plain, (![Y_123]: (~p203('#skF_45'(Y_123)) | r1(Y_123, '#skF_46'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_264, plain, (![Y_123]: (r1(Y_123, '#skF_6'(Y_123)) | ~p305('#skF_7'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_240, plain, (![Y_123]: (r1(Y_123, '#skF_12'(Y_123)) | ~p205('#skF_13'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_226, plain, (![Y_123]: (~p405('#skF_16'(Y_123)) | r1(Y_123, '#skF_17'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_250, plain, (![Y_123]: (~p405('#skF_10'(Y_123)) | r1(Y_123, '#skF_11'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_224, plain, (![Y_123]: (r1(Y_123, '#skF_16'(Y_123)) | ~p105('#skF_17'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_242, plain, (![Y_123]: (~p305('#skF_12'(Y_123)) | r1(Y_123, '#skF_13'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_248, plain, (![Y_123]: (r1(Y_123, '#skF_10'(Y_123)) | ~p205('#skF_11'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_266, plain, (![Y_123]: (~p405('#skF_6'(Y_123)) | r1(Y_123, '#skF_7'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_108, plain, (![Y_123]: (r1(Y_123, '#skF_45'(Y_123)) | ~p103('#skF_46'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_208, plain, (![Y_123]: (r1(Y_123, '#skF_20'(Y_123)) | ~p105('#skF_21'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_178, plain, (![Y_123]: (~p304('#skF_28'(Y_123)) | r1(Y_123, '#skF_29'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_210, plain, (![Y_123]: (~p205('#skF_20'(Y_123)) | r1(Y_123, '#skF_21'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_150, plain, (![Y_123]: (~p204('#skF_35'(Y_123)) | r1(Y_123, '#skF_36'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_218, plain, (![Y_123]: (~p305('#skF_18'(Y_123)) | r1(Y_123, '#skF_19'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_148, plain, (![Y_123]: (r1(Y_123, '#skF_35'(Y_123)) | ~p104('#skF_36'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_176, plain, (![Y_123]: (r1(Y_123, '#skF_28'(Y_123)) | ~p204('#skF_29'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_132, plain, (![Y_123]: (r1(Y_123, '#skF_40'(Y_123)) | ~p303(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_196, plain, (![Y_123]: (r1(Y_123, '#skF_24'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_276, plain, (![Y_123]: (r1(Y_123, '#skF_4'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_260, plain, (![Y_123]: (r1(Y_123, '#skF_8'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_192, plain, (![Y_123]: (r1(Y_123, '#skF_25'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_100, plain, (![Y_123]: (r1(Y_123, '#skF_48'(Y_123)) | ~p502(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_222, plain, (![Y_123]: (~p405('#skF_16'(Y_123)) | ~p105('#skF_17'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_184, plain, (![Y_123]: (r1(Y_123, '#skF_27'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_238, plain, (![Y_123]: (~p305('#skF_12'(Y_123)) | ~p205('#skF_13'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_262, plain, (![Y_123]: (~p405('#skF_6'(Y_123)) | ~p305('#skF_7'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_206, plain, (![Y_123]: (~p205('#skF_20'(Y_123)) | ~p105('#skF_21'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_92, plain, (![Y_123]: (r1(Y_123, '#skF_50'(Y_123)) | ~p302(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_164, plain, (![Y_123]: (r1(Y_123, '#skF_32'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_172, plain, (![Y_123]: (r1(Y_123, '#skF_30'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_204, plain, (![Y_123]: (r1(Y_123, '#skF_22'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_124, plain, (![Y_123]: (r1(Y_123, '#skF_42'(Y_123)) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_232, plain, (![Y_123]: (r1(Y_123, '#skF_15'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_236, plain, (![Y_123]: (r1(Y_123, '#skF_14'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_174, plain, (![Y_123]: (~p304('#skF_28'(Y_123)) | ~p204('#skF_29'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_144, plain, (![Y_123]: (r1(Y_123, '#skF_37'(Y_123)) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_116, plain, (![Y_123]: (r1(Y_123, '#skF_44'(Y_123)) | ~p303(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_120, plain, (![Y_123]: (r1(Y_123, '#skF_43'(Y_123)) | ~p403(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_256, plain, (![Y_123]: (r1(Y_123, '#skF_9'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_280, plain, (![Y_123]: (r1(Y_123, '#skF_3'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_246, plain, (![Y_123]: (~p405('#skF_10'(Y_123)) | ~p205('#skF_11'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_214, plain, (![Y_123]: (~p305('#skF_18'(Y_123)) | ~p105('#skF_19'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_140, plain, (![Y_123]: (r1(Y_123, '#skF_38'(Y_123)) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.72 tff(c_272, plain, (![Y_123]: (r1(Y_123, '#skF_5'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_154, plain, (![Y_123]: (~p304('#skF_33'(Y_123)) | ~p104('#skF_34'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_146, plain, (![Y_123]: (~p204('#skF_35'(Y_123)) | ~p104('#skF_36'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_104, plain, (![Y_123]: (r1(Y_123, '#skF_47'(Y_123)) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_106, plain, (![Y_123]: (~p203('#skF_45'(Y_123)) | ~p103('#skF_46'(Y_123)) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_88, plain, (![Y_123]: (r1(Y_123, '#skF_51'(Y_123)) | ~p202(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_136, plain, (![Y_123]: (r1(Y_123, '#skF_39'(Y_123)) | ~p403(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_96, plain, (![Y_123]: (r1(Y_123, '#skF_49'(Y_123)) | ~p402(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_200, plain, (![Y_123]: (r1(Y_123, '#skF_23'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_284, plain, (![Y_123]: (r1(Y_123, '#skF_2'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_168, plain, (![Y_123]: (r1(Y_123, '#skF_31'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_128, plain, (![Y_123]: (r1(Y_123, '#skF_41'(Y_123)) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_188, plain, (![Y_123]: (r1(Y_123, '#skF_26'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_90, plain, (![Y_123]: (~p102('#skF_50'(Y_123)) | ~p302(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_114, plain, (![Y_123]: (~p103('#skF_44'(Y_123)) | ~p303(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_122, plain, (![Y_123]: (~p103('#skF_42'(Y_123)) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_282, plain, (![Y_123]: (~p405('#skF_2'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_98, plain, (![Y_123]: (~p102('#skF_48'(Y_123)) | ~p502(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_102, plain, (![Y_123]: (~p102('#skF_47'(Y_123)) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_194, plain, (![Y_123]: (~p304('#skF_24'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_118, plain, (![Y_123]: (~p103('#skF_43'(Y_123)) | ~p403(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_186, plain, (![Y_123]: (~p204('#skF_26'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_198, plain, (![Y_123]: (~p304('#skF_23'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_234, plain, (![Y_123]: (~p105('#skF_14'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_202, plain, (![Y_123]: (~p304('#skF_22'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_126, plain, (![Y_123]: (~p103('#skF_41'(Y_123)) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_274, plain, (![Y_123]: (~p305('#skF_4'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_94, plain, (![Y_123]: (~p102('#skF_49'(Y_123)) | ~p402(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_130, plain, (![Y_123]: (~p203('#skF_40'(Y_123)) | ~p303(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_134, plain, (![Y_123]: (~p203('#skF_39'(Y_123)) | ~p403(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_86, plain, (![Y_123]: (~p102('#skF_51'(Y_123)) | ~p202(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_162, plain, (![Y_123]: (~p104('#skF_32'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_182, plain, (![Y_123]: (~p204('#skF_27'(Y_123)) | p404(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_142, plain, (![Y_123]: (~p203('#skF_37'(Y_123)) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_258, plain, (![Y_123]: (~p205('#skF_8'(Y_123)) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_138, plain, (![Y_123]: (~p203('#skF_38'(Y_123)) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_190, plain, (![Y_123]: (~p204('#skF_25'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_254, plain, (![Y_123]: (~p205('#skF_9'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_230, plain, (![Y_123]: (~p105('#skF_15'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_270, plain, (![Y_123]: (~p305('#skF_5'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_278, plain, (![Y_123]: (~p405('#skF_3'(Y_123)) | ~p505(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_170, plain, (![Y_123]: (~p104('#skF_30'(Y_123)) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_166, plain, (![Y_123]: (~p104('#skF_31'(Y_123)) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_50, plain, (![Y_123]: (~p202(Y_123) | ~p502(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_42, plain, (![Y_123]: (~p401(Y_123) | ~p601(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_58, plain, (![Y_123]: (~p302(Y_123) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_60, plain, (![Y_123]: (~p402(Y_123) | ~p502(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_54, plain, (![Y_123]: (~p302(Y_123) | ~p402(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_62, plain, (![Y_123]: (~p402(Y_123) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_6183, plain, (~p202('#skF_52'))).
% 15.40/4.73 tff(c_52, plain, (![Y_123]: (~p202(Y_123) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_36, plain, (![Y_123]: (~p301(Y_123) | ~p501(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_56, plain, (![Y_123]: (~p302(Y_123) | ~p502(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_6166, plain, (~p403('#skF_52'))).
% 15.40/4.73 tff(c_44, plain, (![Y_123]: (~p501(Y_123) | ~p601(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_66, plain, (![Y_123]: (~p303(Y_123) | ~p403(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_6155, plain, (~p402('#skF_52'))).
% 15.40/4.73 tff(c_6149, plain, (p602('#skF_52'))).
% 15.40/4.73 tff(c_6148, plain, (~p502('#skF_52'))).
% 15.40/4.73 tff(c_48, plain, (![Y_123]: (~p202(Y_123) | ~p402(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_64, plain, (![Y_123]: (~p502(Y_123) | ~p602(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_40, plain, (![Y_123]: (~p401(Y_123) | ~p501(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_70, plain, (![Y_123]: (~p303(Y_123) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_34, plain, (![Y_123]: (~p301(Y_123) | ~p401(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_32, plain, (![Y_123]: (~p201(Y_123) | ~p601(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_380, plain, (~p302('#skF_52'))).
% 15.40/4.73 tff(c_68, plain, (![Y_123]: (~p303(Y_123) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_46, plain, (![Y_123]: (~p202(Y_123) | ~p302(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_369, plain, (~p503('#skF_52'))).
% 15.40/4.73 tff(c_38, plain, (![Y_123]: (~p301(Y_123) | ~p601(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_72, plain, (![Y_123]: (~p403(Y_123) | ~p503(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_363, plain, (~p504('#skF_52'))).
% 15.40/4.73 tff(c_78, plain, (![Y_123]: (p404(Y_123) | ~p504(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_80, plain, (![Y_123]: (p404(Y_123) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_20, plain, (![Y_123]: (~p101(Y_123) | ~p401(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_22, plain, (![Y_123]: (~p101(Y_123) | ~p501(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_337, plain, (~p604('#skF_52'))).
% 15.40/4.73 tff(c_18, plain, (![Y_123]: (~p101(Y_123) | ~p301(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_82, plain, (![Y_123]: (~p504(Y_123) | ~p604(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_331, plain, (~p201('#skF_52'))).
% 15.40/4.73 tff(c_16, plain, (![Y_123]: (~p101(Y_123) | ~p201(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_76, plain, (![Y_123]: (~p503(Y_123) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_320, plain, (~p601('#skF_52'))).
% 15.40/4.73 tff(c_314, plain, (~p603('#skF_52'))).
% 15.40/4.73 tff(c_24, plain, (![Y_123]: (~p101(Y_123) | ~p601(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_74, plain, (![Y_123]: (~p403(Y_123) | ~p603(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_308, plain, (~p401('#skF_52'))).
% 15.40/4.73 tff(c_302, plain, (~p301('#skF_52'))).
% 15.40/4.73 tff(c_28, plain, (![Y_123]: (~p201(Y_123) | ~p401(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_301, plain, (~p501('#skF_52'))).
% 15.40/4.73 tff(c_26, plain, (![Y_123]: (~p201(Y_123) | ~p301(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_30, plain, (![Y_123]: (~p201(Y_123) | ~p501(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_290, plain, (~p605('#skF_52'))).
% 15.40/4.73 tff(c_84, plain, (![Y_123]: (~p505(Y_123) | ~p605(Y_123) | ~r1('#skF_1', Y_123)))).
% 15.40/4.73 tff(c_14, plain, (r1('#skF_1', '#skF_52'))).
% 15.40/4.74 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.40/4.74
%------------------------------------------------------------------------------