%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL675+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/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 : n014.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:29 AM UTC 2026
% Result : CounterSatisfiable 6.39s 3.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL675+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % 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.11/0.37 % Computer : n014.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 21:27:12 UTC 2026
% 0.11/0.37 % CPUTime :
% 6.39/3.10
% 6.39/3.10 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.39/3.10
% 6.39/3.10 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.39/3.11 %$ r1 > p2 > p102 > p101 > p100 > p1 > #nlpp > #skF_2 > #skF_1 > #skF_3
% 6.39/3.11
% 6.39/3.11 %Foreground sorts:
% 6.39/3.11
% 6.39/3.11
% 6.39/3.11 %Background operators:
% 6.39/3.11
% 6.39/3.11
% 6.39/3.11 %Foreground operators:
% 6.39/3.11 tff('#skF_2', type, '#skF_2': $i > $i).
% 6.39/3.11 tff(p101, type, p101: $i > $o).
% 6.39/3.11 tff(p102, type, p102: $i > $o).
% 6.39/3.11 tff(p100, type, p100: $i > $o).
% 6.39/3.11 tff(r1, type, r1: ($i * $i) > $o).
% 6.39/3.11 tff('#skF_1', type, '#skF_1': $i).
% 6.39/3.11 tff(p2, type, p2: $i > $o).
% 6.39/3.11 tff('#skF_3', type, '#skF_3': $i > $i).
% 6.39/3.11 tff(p1, type, p1: $i > $o).
% 6.39/3.11
% 6.39/3.11 %Saturated clause set:
% 6.39/3.12 tff(c_634, plain, (![Y_43, Y_101]: (~p1('#skF_3'(Y_43)) | p1('#skF_3'(Y_101)) | ~p100('#skF_3'(Y_43)) | ~r1('#skF_3'(Y_43), Y_101) | ~p100(Y_101) | p101(Y_101) | ~r1('#skF_1', Y_101) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.39/3.12 tff(c_633, plain, (![Y_41, Y_101]: (~p1('#skF_2'(Y_41)) | p1('#skF_3'(Y_101)) | ~p100('#skF_2'(Y_41)) | ~r1('#skF_2'(Y_41), Y_101) | ~p100(Y_101) | p101(Y_101) | ~r1('#skF_1', Y_101) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.12 tff(c_663, plain, (![Y_43, Y_103]: (~p1('#skF_3'(Y_43)) | p1('#skF_2'(Y_103)) | ~p100('#skF_3'(Y_43)) | ~r1('#skF_3'(Y_43), Y_103) | ~p100(Y_103) | p101(Y_103) | ~r1('#skF_1', Y_103) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.39/3.12 tff(c_662, plain, (![Y_41, Y_103]: (~p1('#skF_2'(Y_41)) | p1('#skF_2'(Y_103)) | ~p100('#skF_2'(Y_41)) | ~r1('#skF_2'(Y_41), Y_103) | ~p100(Y_103) | p101(Y_103) | ~r1('#skF_1', Y_103) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.12 tff(c_737, plain, (![Y_43, Y_110]: (~p2('#skF_3'(Y_43)) | ~p101('#skF_2'(Y_110)) | p2('#skF_2'(Y_110)) | ~p101('#skF_3'(Y_43)) | ~r1('#skF_3'(Y_43), Y_110) | ~p100(Y_110) | p101(Y_110) | ~r1('#skF_1', Y_110) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.39/3.12 tff(c_394, plain, (![X_2, Y_74, Y_43]: (r1(X_2, '#skF_2'(Y_74)) | ~r1('#skF_3'(Y_43), Y_74) | ~p100(Y_74) | p101(Y_74) | ~r1('#skF_1', Y_74) | ~r1(X_2, Y_43) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.39/3.12 tff(c_393, plain, (![X_2, Y_74, Y_41]: (r1(X_2, '#skF_2'(Y_74)) | ~r1('#skF_2'(Y_41), Y_74) | ~p100(Y_74) | p101(Y_74) | ~r1('#skF_1', Y_74) | ~r1(X_2, Y_41) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.12 tff(c_351, plain, (![X_2, Y_69, Y_41]: (r1(X_2, '#skF_3'(Y_69)) | ~r1('#skF_2'(Y_41), Y_69) | ~p100(Y_69) | p101(Y_69) | ~r1('#skF_1', Y_69) | ~r1(X_2, Y_41) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.12 tff(c_352, plain, (![X_2, Y_69, Y_43]: (r1(X_2, '#skF_3'(Y_69)) | ~r1('#skF_3'(Y_43), Y_69) | ~p100(Y_69) | p101(Y_69) | ~r1('#skF_1', Y_69) | ~r1(X_2, Y_43) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.39/3.12 tff(c_763, plain, (![Y_41, Y_112]: (p2('#skF_2'(Y_41)) | ~p101('#skF_2'(Y_41)) | ~r1('#skF_2'(Y_41), Y_112) | ~p100(Y_112) | p101(Y_112) | ~r1('#skF_1', Y_112) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.13 tff(c_705, plain, (![Y_41]: (p2('#skF_2'(Y_41)) | ~p101('#skF_2'(Y_41)) | ~r1('#skF_2'(Y_41), '#skF_1') | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.39/3.13 tff(c_819, plain, (![Y_110]: (~p101('#skF_2'(Y_110)) | p2('#skF_2'(Y_110)) | ~r1('#skF_3'('#skF_1'), Y_110) | ~p100(Y_110) | p101(Y_110) | ~r1('#skF_1', Y_110)))).
% 6.39/3.13 tff(c_784, plain, (![Y_112]: (~r1('#skF_2'('#skF_1'), Y_112) | ~p100(Y_112) | p101(Y_112) | ~r1('#skF_1', Y_112)))).
% 6.39/3.13 tff(c_774, plain, (p2('#skF_3'('#skF_1')))).
% 6.39/3.13 tff(c_785, plain, (~p2('#skF_2'('#skF_1')))).
% 6.39/3.13 tff(c_688, plain, (![X_106, Y_18]: (p2(X_106) | ~p101(X_106) | ~r1('#skF_1', X_106) | ~r1(X_106, Y_18) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.39/3.13 tff(c_719, plain, (~r1('#skF_2'('#skF_1'), '#skF_1'))).
% 6.39/3.13 tff(c_247, plain, (![X_56, Y_57]: (~p2(X_56) | ~p101('#skF_2'(Y_57)) | p2('#skF_2'(Y_57)) | ~p101(X_56) | ~r1('#skF_1', X_56) | ~r1(X_56, Y_57) | ~p100(Y_57) | p101(Y_57) | ~r1('#skF_1', Y_57)))).
% 6.82/3.13 tff(c_718, plain, (~r1('#skF_3'('#skF_1'), '#skF_1'))).
% 6.82/3.13 tff(c_687, plain, (![X_106]: (p2(X_106) | ~p101(X_106) | ~r1('#skF_1', X_106) | ~r1(X_106, '#skF_1')))).
% 6.82/3.13 tff(c_611, plain, (![X_97, Y_18]: (~p1(X_97) | p1('#skF_2'(Y_18)) | ~p100(X_97) | ~r1('#skF_1', X_97) | ~r1(X_97, Y_18) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_571, plain, (![X_93, Y_18]: (~p1(X_93) | p1('#skF_3'(Y_18)) | ~p100(X_93) | ~r1('#skF_1', X_93) | ~r1(X_93, Y_18) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_593, plain, (![Y_43]: (~p1('#skF_3'(Y_43)) | ~p100('#skF_3'(Y_43)) | ~r1('#skF_3'(Y_43), '#skF_1') | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.82/3.13 tff(c_592, plain, (![Y_41]: (~p1('#skF_2'(Y_41)) | ~p100('#skF_2'(Y_41)) | ~r1('#skF_2'(Y_41), '#skF_1') | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.82/3.13 tff(c_575, plain, (![X_93]: (~p1(X_93) | ~p100(X_93) | ~r1('#skF_1', X_93) | ~r1(X_93, '#skF_1')))).
% 6.82/3.13 tff(c_491, plain, (![X_84, Y_18]: (p1(X_84) | ~p1('#skF_2'(Y_18)) | ~p100(X_84) | ~r1('#skF_1', X_84) | ~r1(X_84, Y_18) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_529, plain, (![Y_89]: (~p1(Y_89) | ~p100(Y_89) | p101(Y_89) | ~r1('#skF_1', Y_89)))).
% 6.82/3.13 tff(c_481, plain, (![X_82, Y_18]: (p1(X_82) | ~p1('#skF_3'(Y_18)) | ~p100(X_82) | ~r1('#skF_1', X_82) | ~r1(X_82, Y_18) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_396, plain, (![Y_18, Y_74]: (r1(Y_18, '#skF_2'(Y_74)) | ~r1('#skF_2'(Y_18), Y_74) | ~p100(Y_74) | p101(Y_74) | ~r1('#skF_1', Y_74) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_395, plain, (![Y_18, Y_74]: (r1(Y_18, '#skF_2'(Y_74)) | ~r1('#skF_3'(Y_18), Y_74) | ~p100(Y_74) | p101(Y_74) | ~r1('#skF_1', Y_74) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_354, plain, (![Y_18, Y_69]: (r1(Y_18, '#skF_3'(Y_69)) | ~r1('#skF_2'(Y_18), Y_69) | ~p100(Y_69) | p101(Y_69) | ~r1('#skF_1', Y_69) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_249, plain, (![X_2, Y_57, X_56]: (r1(X_2, '#skF_2'(Y_57)) | ~r1(X_2, X_56) | ~r1(X_56, Y_57) | ~p100(Y_57) | p101(Y_57) | ~r1('#skF_1', Y_57)))).
% 6.82/3.13 tff(c_353, plain, (![Y_18, Y_69]: (r1(Y_18, '#skF_3'(Y_69)) | ~r1('#skF_3'(Y_18), Y_69) | ~p100(Y_69) | p101(Y_69) | ~r1('#skF_1', Y_69) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.13 tff(c_210, plain, (![X_2, Y_53, X_52]: (r1(X_2, '#skF_3'(Y_53)) | ~r1(X_2, X_52) | ~r1(X_52, Y_53) | ~p100(Y_53) | p101(Y_53) | ~r1('#skF_1', Y_53)))).
% 6.82/3.13 tff(c_299, plain, (![Y_18]: (p1(Y_18) | ~p1('#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_303, plain, (~p1('#skF_2'('#skF_1')))).
% 6.82/3.14 tff(c_285, plain, (![Y_18]: (p1(Y_18) | ~p1('#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_289, plain, (~p1('#skF_3'('#skF_1')))).
% 6.82/3.14 tff(c_263, plain, (![Y_18]: (p100('#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_272, plain, (~p1('#skF_1'))).
% 6.82/3.14 tff(c_74, plain, (![X_2, Y_41]: (r1(X_2, '#skF_2'(Y_41)) | ~r1(X_2, Y_41) | ~p100(Y_41) | p101(Y_41) | ~r1('#skF_1', Y_41)))).
% 6.82/3.14 tff(c_224, plain, (![Y_18]: (p100('#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_125, plain, (![X_2, Y_43]: (r1(X_2, '#skF_3'(Y_43)) | ~r1(X_2, Y_43) | ~p100(Y_43) | p101(Y_43) | ~r1('#skF_1', Y_43)))).
% 6.82/3.14 tff(c_14, plain, (![Y_18, X_28]: (~p1(Y_18) | ~p100(X_28) | p1(X_28) | ~r1(Y_18, X_28) | ~p100(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_20, plain, (![Y_18, X_25]: (p2(Y_18) | ~p101(X_25) | ~p2(X_25) | ~r1(Y_18, X_25) | ~p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_18, plain, (![Y_18, X_26]: (~p2(Y_18) | ~p101(X_26) | p2(X_26) | ~r1(Y_18, X_26) | ~p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_16, plain, (![Y_18, X_27]: (p1(Y_18) | ~p100(X_27) | ~p1(X_27) | ~r1(Y_18, X_27) | ~p100(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_145, plain, (p101('#skF_3'('#skF_1')))).
% 6.82/3.14 tff(c_144, plain, (p100('#skF_3'('#skF_1')))).
% 6.82/3.14 tff(c_28, plain, (![Y_18]: (r1(Y_18, '#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_113, plain, (p101('#skF_2'('#skF_1')))).
% 6.82/3.14 tff(c_112, plain, (p100('#skF_2'('#skF_1')))).
% 6.82/3.14 tff(c_36, plain, (![Y_18]: (r1(Y_18, '#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_34, plain, (![Y_18]: (~p2('#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_22, plain, (![Y_18]: (p101('#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_26, plain, (![Y_18]: (p2('#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_30, plain, (![Y_18]: (p101('#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_24, plain, (![Y_18]: (~p102('#skF_3'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_32, plain, (![Y_18]: (~p102('#skF_2'(Y_18)) | ~p100(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_4, plain, (![X_2, Z_4, Y_3]: (r1(X_2, Z_4) | ~r1(Y_3, Z_4) | ~r1(X_2, Y_3)))).
% 6.82/3.14 tff(c_10, plain, (![Y_18]: (~p101(Y_18) | p100(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_45, plain, (~p102('#skF_1'))).
% 6.82/3.14 tff(c_12, plain, (![Y_18]: (~p102(Y_18) | p101(Y_18) | ~r1('#skF_1', Y_18)))).
% 6.82/3.14 tff(c_2, plain, (![X_1]: (r1(X_1, X_1)))).
% 6.82/3.14 tff(c_6, plain, (p100('#skF_1'))).
% 6.82/3.14 tff(c_8, plain, (~p101('#skF_1'))).
% 6.82/3.14 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.82/3.14
%------------------------------------------------------------------------------