%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL665+1.001 : 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 : n028.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:25 AM UTC 2026
% Result : CounterSatisfiable 6.38s 3.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL665+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % 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.11/0.38 % Computer : n028.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 5 03:05:14 UTC 2026
% 0.11/0.38 % CPUTime :
% 6.38/3.12
% 6.38/3.12 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.38/3.13
% 6.38/3.13 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.75/3.14 %$ r1 > p26 > p25 > p24 > p23 > p22 > p21 > p16 > p15 > p14 > p13 > p12 > p11 > #nlpp > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_17 > #skF_15 > #skF_8 > #skF_16 > #skF_14 > #skF_10 > #skF_1 > #skF_13 > #skF_3 > #skF_11 > #skF_12 > #skF_6
% 6.75/3.14
% 6.75/3.14 %Foreground sorts:
% 6.75/3.14
% 6.75/3.14
% 6.75/3.14 %Background operators:
% 6.75/3.14
% 6.75/3.14
% 6.75/3.14 %Foreground operators:
% 6.75/3.14 tff('#skF_9', type, '#skF_9': $i > $i).
% 6.75/3.14 tff(p12, type, p12: $i > $o).
% 6.75/3.14 tff('#skF_7', type, '#skF_7': $i > $i).
% 6.75/3.14 tff('#skF_5', type, '#skF_5': $i > $i).
% 6.75/3.14 tff(p15, type, p15: $i > $o).
% 6.75/3.14 tff(p11, type, p11: $i > $o).
% 6.75/3.14 tff('#skF_2', type, '#skF_2': $i > $i).
% 6.75/3.14 tff('#skF_4', type, '#skF_4': $i > $i).
% 6.75/3.14 tff('#skF_17', type, '#skF_17': $i).
% 6.75/3.14 tff(p14, type, p14: $i > $o).
% 6.75/3.14 tff('#skF_15', type, '#skF_15': $i).
% 6.75/3.14 tff(p23, type, p23: $i > $o).
% 6.75/3.14 tff('#skF_8', type, '#skF_8': $i > $i).
% 6.75/3.14 tff('#skF_16', type, '#skF_16': $i).
% 6.75/3.14 tff('#skF_14', type, '#skF_14': $i).
% 6.75/3.14 tff('#skF_10', type, '#skF_10': $i > $i).
% 6.75/3.14 tff(p22, type, p22: $i > $o).
% 6.75/3.14 tff(r1, type, r1: ($i * $i) > $o).
% 6.75/3.14 tff('#skF_1', type, '#skF_1': $i).
% 6.75/3.14 tff(p13, type, p13: $i > $o).
% 6.75/3.14 tff(p25, type, p25: $i > $o).
% 6.75/3.14 tff('#skF_13', type, '#skF_13': $i > $i).
% 6.75/3.14 tff(p16, type, p16: $i > $o).
% 6.75/3.14 tff('#skF_3', type, '#skF_3': $i > $i).
% 6.75/3.14 tff('#skF_11', type, '#skF_11': $i > $i).
% 6.75/3.14 tff(p26, type, p26: $i > $o).
% 6.75/3.14 tff(p21, type, p21: $i > $o).
% 6.75/3.14 tff('#skF_12', type, '#skF_12': $i > $i).
% 6.75/3.14 tff('#skF_6', type, '#skF_6': $i > $i).
% 6.75/3.14 tff(p24, type, p24: $i > $o).
% 6.75/3.14
% 6.75/3.14 %Saturated clause set:
% 6.75/3.14 tff(c_842, plain, (![Y_132]: (p26('#skF_9'(Y_132)) | p15(Y_132) | ~r1('#skF_1', Y_132)))).
% 6.75/3.14 tff(c_630, plain, (![Y_122]: (p24('#skF_13'(Y_122)) | p11(Y_122) | ~r1('#skF_1', Y_122)))).
% 6.75/3.14 tff(c_625, plain, (![Y_122]: (p26('#skF_13'(Y_122)) | p11(Y_122) | ~r1('#skF_1', Y_122)))).
% 6.75/3.14 tff(c_405, plain, (![Y_117]: (p22('#skF_11'(Y_117)) | p13(Y_117) | ~r1('#skF_1', Y_117)))).
% 6.75/3.14 tff(c_634, plain, (![Y_122]: (p25('#skF_13'(Y_122)) | p11(Y_122) | ~r1('#skF_1', Y_122)))).
% 6.75/3.14 tff(c_544, plain, (![Y_120]: (p25('#skF_10'(Y_120)) | p13(Y_120) | ~r1('#skF_1', Y_120)))).
% 6.75/3.14 tff(c_404, plain, (![Y_117]: (p26('#skF_11'(Y_117)) | p13(Y_117) | ~r1('#skF_1', Y_117)))).
% 6.75/3.14 tff(c_851, plain, (![Y_132]: (p25('#skF_9'(Y_132)) | p15(Y_132) | ~r1('#skF_1', Y_132)))).
% 6.75/3.14 tff(c_493, plain, (![Y_119]: (p22('#skF_8'(Y_119)) | p15(Y_119) | ~r1('#skF_1', Y_119)))).
% 6.75/3.15 tff(c_449, plain, (![Y_118]: (p22('#skF_12'(Y_118)) | p11(Y_118) | ~r1('#skF_1', Y_118)))).
% 6.75/3.15 tff(c_540, plain, (![Y_120]: (p24('#skF_10'(Y_120)) | p13(Y_120) | ~r1('#skF_1', Y_120)))).
% 6.75/3.15 tff(c_448, plain, (![Y_118]: (p26('#skF_12'(Y_118)) | p11(Y_118) | ~r1('#skF_1', Y_118)))).
% 6.75/3.15 tff(c_492, plain, (![Y_119]: (p26('#skF_8'(Y_119)) | p15(Y_119) | ~r1('#skF_1', Y_119)))).
% 6.75/3.15 tff(c_626, plain, (![Y_122]: (p22('#skF_13'(Y_122)) | p11(Y_122) | ~r1('#skF_1', Y_122)))).
% 6.75/3.15 tff(c_413, plain, (![Y_117]: (p25('#skF_11'(Y_117)) | p13(Y_117) | ~r1('#skF_1', Y_117)))).
% 6.75/3.15 tff(c_847, plain, (![Y_132]: (p24('#skF_9'(Y_132)) | p15(Y_132) | ~r1('#skF_1', Y_132)))).
% 6.75/3.15 tff(c_501, plain, (![Y_119]: (p25('#skF_8'(Y_119)) | p15(Y_119) | ~r1('#skF_1', Y_119)))).
% 6.75/3.15 tff(c_453, plain, (![Y_118]: (p24('#skF_12'(Y_118)) | p11(Y_118) | ~r1('#skF_1', Y_118)))).
% 6.75/3.15 tff(c_535, plain, (![Y_120]: (p26('#skF_10'(Y_120)) | p13(Y_120) | ~r1('#skF_1', Y_120)))).
% 6.75/3.15 tff(c_497, plain, (![Y_119]: (p24('#skF_8'(Y_119)) | p15(Y_119) | ~r1('#skF_1', Y_119)))).
% 6.75/3.15 tff(c_843, plain, (![Y_132]: (p22('#skF_9'(Y_132)) | p15(Y_132) | ~r1('#skF_1', Y_132)))).
% 6.75/3.15 tff(c_409, plain, (![Y_117]: (p24('#skF_11'(Y_117)) | p13(Y_117) | ~r1('#skF_1', Y_117)))).
% 6.75/3.15 tff(c_457, plain, (![Y_118]: (p25('#skF_12'(Y_118)) | p11(Y_118) | ~r1('#skF_1', Y_118)))).
% 6.75/3.15 tff(c_972, plain, (p14('#skF_16'))).
% 6.75/3.15 tff(c_971, plain, (p14('#skF_17'))).
% 6.75/3.15 tff(c_970, plain, (p14('#skF_15'))).
% 6.75/3.15 tff(c_969, plain, (p14('#skF_14'))).
% 6.75/3.15 tff(c_907, plain, (![Y_137]: (p14(Y_137) | ~r1('#skF_1', Y_137)))).
% 6.75/3.15 tff(c_801, plain, (p16('#skF_15'))).
% 6.75/3.15 tff(c_802, plain, (p16('#skF_17'))).
% 6.75/3.15 tff(c_803, plain, (p16('#skF_16'))).
% 6.75/3.15 tff(c_800, plain, (p16('#skF_14'))).
% 6.75/3.15 tff(c_46, plain, (![Y_80]: (r1(Y_80, '#skF_9'(Y_80)) | p15(Y_80) | ~r1('#skF_1', Y_80)))).
% 6.75/3.15 tff(c_731, plain, (![Y_130]: (p16(Y_130) | ~r1('#skF_1', Y_130)))).
% 6.75/3.15 tff(c_536, plain, (![Y_120]: (p22('#skF_10'(Y_120)) | p13(Y_120) | ~r1('#skF_1', Y_120)))).
% 6.75/3.15 tff(c_593, plain, (p14('#skF_1'))).
% 6.75/3.15 tff(c_30, plain, (![Y_88]: (r1(Y_88, '#skF_13'(Y_88)) | p11(Y_88) | ~r1('#skF_1', Y_88)))).
% 6.75/3.15 tff(c_42, plain, (![Y_82]: (r1(Y_82, '#skF_10'(Y_82)) | p13(Y_82) | ~r1('#skF_1', Y_82)))).
% 6.75/3.15 tff(c_503, plain, (p15('#skF_1'))).
% 6.75/3.15 tff(c_50, plain, (![Y_78]: (r1(Y_78, '#skF_8'(Y_78)) | p15(Y_78) | ~r1('#skF_1', Y_78)))).
% 6.75/3.15 tff(c_460, plain, (p11('#skF_1'))).
% 6.75/3.15 tff(c_459, plain, (p13('#skF_1'))).
% 6.75/3.15 tff(c_34, plain, (![Y_86]: (r1(Y_86, '#skF_12'(Y_86)) | p11(Y_86) | ~r1('#skF_1', Y_86)))).
% 6.75/3.15 tff(c_38, plain, (![Y_84]: (r1(Y_84, '#skF_11'(Y_84)) | p13(Y_84) | ~r1('#skF_1', Y_84)))).
% 6.75/3.16 tff(c_370, plain, (p16('#skF_1'))).
% 6.75/3.16 tff(c_320, plain, (p26('#skF_1'))).
% 6.75/3.16 tff(c_223, plain, (![X_1]: (p26(X_1) | ~r1('#skF_1', X_1)))).
% 6.75/3.16 tff(c_287, plain, (p22('#skF_1'))).
% 6.75/3.16 tff(c_199, plain, (![X_1]: (p22(X_1) | ~r1('#skF_1', X_1)))).
% 6.75/3.16 tff(c_232, plain, (p26('#skF_17'))).
% 6.75/3.16 tff(c_229, plain, (p26('#skF_15'))).
% 6.75/3.16 tff(c_226, plain, (p26('#skF_14'))).
% 6.75/3.16 tff(c_235, plain, (p26('#skF_16'))).
% 6.75/3.16 tff(c_211, plain, (p22('#skF_16'))).
% 6.75/3.16 tff(c_26, plain, (![X_56, Y_54]: (p26(X_56) | ~r1(Y_54, X_56) | ~r1('#skF_1', Y_54)))).
% 6.75/3.16 tff(c_208, plain, (p22('#skF_17'))).
% 6.75/3.16 tff(c_205, plain, (p22('#skF_15'))).
% 6.75/3.16 tff(c_202, plain, (p22('#skF_14'))).
% 6.75/3.16 tff(c_20, plain, (![X_65, Y_63]: (p22(X_65) | ~r1(Y_63, X_65) | ~r1('#skF_1', Y_63)))).
% 6.75/3.16 tff(c_40, plain, (![Y_82]: (~p23('#skF_10'(Y_82)) | p13(Y_82) | ~r1('#skF_1', Y_82)))).
% 6.75/3.16 tff(c_32, plain, (![Y_86]: (~p23('#skF_12'(Y_86)) | p11(Y_86) | ~r1('#skF_1', Y_86)))).
% 6.75/3.16 tff(c_36, plain, (![Y_84]: (~p21('#skF_11'(Y_84)) | p13(Y_84) | ~r1('#skF_1', Y_84)))).
% 6.75/3.16 tff(c_44, plain, (![Y_80]: (~p21('#skF_9'(Y_80)) | p15(Y_80) | ~r1('#skF_1', Y_80)))).
% 6.75/3.16 tff(c_48, plain, (![Y_78]: (~p23('#skF_8'(Y_78)) | p15(Y_78) | ~r1('#skF_1', Y_78)))).
% 6.75/3.16 tff(c_170, plain, (p24('#skF_1'))).
% 6.75/3.16 tff(c_140, plain, (![X_1]: (p24(X_1) | ~r1('#skF_1', X_1)))).
% 6.75/3.16 tff(c_152, plain, (p24('#skF_16'))).
% 6.75/3.16 tff(c_149, plain, (p24('#skF_17'))).
% 6.75/3.16 tff(c_146, plain, (p24('#skF_15'))).
% 6.75/3.16 tff(c_143, plain, (p24('#skF_14'))).
% 6.75/3.16 tff(c_22, plain, (![X_62, Y_60]: (p24(X_62) | ~r1(Y_60, X_62) | ~r1('#skF_1', Y_60)))).
% 6.75/3.16 tff(c_117, plain, (p25('#skF_1'))).
% 6.75/3.16 tff(c_28, plain, (![Y_88]: (~p21('#skF_13'(Y_88)) | p11(Y_88) | ~r1('#skF_1', Y_88)))).
% 6.75/3.16 tff(c_87, plain, (![X_1]: (p25(X_1) | ~r1('#skF_1', X_1)))).
% 6.75/3.16 tff(c_96, plain, (p25('#skF_17'))).
% 6.75/3.16 tff(c_93, plain, (p25('#skF_15'))).
% 6.75/3.16 tff(c_99, plain, (p25('#skF_16'))).
% 6.75/3.16 tff(c_90, plain, (p25('#skF_14'))).
% 6.75/3.16 tff(c_24, plain, (![X_59, Y_57]: (p25(X_59) | ~r1(Y_57, X_59) | ~r1('#skF_1', Y_57)))).
% 6.75/3.16 tff(c_2, plain, (![X_1]: (r1(X_1, X_1)))).
% 6.75/3.16 tff(c_18, plain, (r1('#skF_1', '#skF_14'))).
% 6.75/3.16 tff(c_14, plain, (r1('#skF_1', '#skF_15'))).
% 6.75/3.16 tff(c_6, plain, (r1('#skF_1', '#skF_17'))).
% 6.75/3.16 tff(c_10, plain, (r1('#skF_1', '#skF_16'))).
% 6.75/3.16 tff(c_4, plain, (~p11('#skF_17'))).
% 6.75/3.16 tff(c_8, plain, (~p12('#skF_16'))).
% 6.75/3.16 tff(c_12, plain, (~p13('#skF_15'))).
% 6.75/3.16 tff(c_16, plain, (~p15('#skF_14'))).
% 6.75/3.16 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.75/3.16
%------------------------------------------------------------------------------