%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS028+1 : TPTP v9.0.0. Released v3.1.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 : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:07:11 PM UTC 2025
% Result : Satisfiable 3.71s 1.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : KRS028+1 : TPTP v9.0.0. Released v3.1.0.
% 0.10/0.13 % 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.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 02:54:50 EDT 2025
% 0.12/0.34 % CPUTime :
% 3.71/1.80
% 3.71/1.80 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.71/1.80
% 3.71/1.80 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.71/1.80 %$ rrxa > rrx4a > rrx4 > rrx3a > rrx3 > rrx2a > rrx2 > rrx1a > rrx1 > rrx > xsd_string > xsd_integer > cowlThing > cowlNothing > cc2 > cc1 > cSatisfiable > #nlpp > i2003_11_14_17_15_19316 > #skF_2 > #skF_1 > #skF_3
% 3.71/1.80
% 3.71/1.80 %Foreground sorts:
% 3.71/1.80
% 3.71/1.80
% 3.71/1.80 %Background operators:
% 3.71/1.80
% 3.71/1.80
% 3.71/1.80 %Foreground operators:
% 3.71/1.80 tff(i2003_11_14_17_15_19316, type, i2003_11_14_17_15_19316: $i).
% 3.71/1.80 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.71/1.80 tff(rrxa, type, rrxa: ($i * $i) > $o).
% 3.71/1.80 tff(cowlThing, type, cowlThing: $i > $o).
% 3.71/1.80 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.71/1.80 tff(rrx2, type, rrx2: ($i * $i) > $o).
% 3.71/1.80 tff(rrx1a, type, rrx1a: ($i * $i) > $o).
% 3.71/1.80 tff(rrx, type, rrx: ($i * $i) > $o).
% 3.71/1.80 tff(cc1, type, cc1: $i > $o).
% 3.71/1.80 tff(rrx2a, type, rrx2a: ($i * $i) > $o).
% 3.71/1.80 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.71/1.80 tff(rrx4, type, rrx4: ($i * $i) > $o).
% 3.71/1.80 tff(rrx3a, type, rrx3a: ($i * $i) > $o).
% 3.71/1.80 tff(rrx4a, type, rrx4a: ($i * $i) > $o).
% 3.71/1.80 tff(rrx1, type, rrx1: ($i * $i) > $o).
% 3.71/1.80 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.71/1.80 tff(rrx3, type, rrx3: ($i * $i) > $o).
% 3.71/1.80 tff(xsd_string, type, xsd_string: $i > $o).
% 3.71/1.80 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.71/1.80 tff(cc2, type, cc2: $i > $o).
% 3.71/1.80 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.71/1.80
% 3.71/1.80 %Saturated clause set:
% 3.71/1.81 tff(c_78, plain, (![X_77, Y_85, Y_84]: (rrx3a(X_77, '#skF_1'(X_77)) | cSatisfiable(X_77) | ~cc1(Y_85) | ~rrx3a(X_77, Y_85) | ~cc2(Y_84) | ~rrx4a(X_77, Y_84)))).
% 3.71/1.81 tff(c_74, plain, (![X_77, Y_85, Y_84]: (cc2('#skF_1'(X_77)) | cSatisfiable(X_77) | ~cc1(Y_85) | ~rrx3a(X_77, Y_85) | ~cc2(Y_84) | ~rrx4a(X_77, Y_84)))).
% 3.71/1.81 tff(c_76, plain, (![X_77, Y_85, Y_84]: (cc1('#skF_1'(X_77)) | cSatisfiable(X_77) | ~cc1(Y_85) | ~rrx3a(X_77, Y_85) | ~cc2(Y_84) | ~rrx4a(X_77, Y_84)))).
% 3.71/1.81 tff(c_158, plain, (![X_77]: (~cc2('#skF_3'(X_77)) | ~cc1('#skF_3'(X_77)) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_147, plain, (![Y_157, X_77]: (Y_157='#skF_3'(X_77) | ~rrx3a(X_77, Y_157) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_64, plain, (![Y_86, X_77]: (~cc2(Y_86) | ~cc1(Y_86) | ~rrx3a(X_77, Y_86) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_143, plain, (![Y_154, X_77]: (Y_154='#skF_2'(X_77) | ~rrx4a(X_77, Y_154) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_84, plain, (![Z_95, Y_94, X_93]: (Z_95=Y_94 | ~rrx3a(X_93, Z_95) | ~rrx3a(X_93, Y_94)))).
% 3.71/1.81 tff(c_88, plain, (![Z_101, Y_100, X_99]: (Z_101=Y_100 | ~rrx4a(X_99, Z_101) | ~rrx4a(X_99, Y_100)))).
% 3.71/1.81 tff(c_86, plain, (![Z_98, Y_97, X_96]: (Z_98=Y_97 | ~rrx4(X_96, Z_98) | ~rrx4(X_96, Y_97)))).
% 3.71/1.81 tff(c_80, plain, (![Z_89, Y_88, X_87]: (Z_89=Y_88 | ~rrx(X_87, Z_89) | ~rrx(X_87, Y_88)))).
% 3.71/1.81 tff(c_82, plain, (![Z_92, Y_91, X_90]: (Z_92=Y_91 | ~rrx3(X_90, Z_92) | ~rrx3(X_90, Y_91)))).
% 3.71/1.81 tff(c_134, plain, (![X_141]: (rrx2a(X_141, '#skF_2'(X_141)) | ~cSatisfiable(X_141)))).
% 3.71/1.81 tff(c_127, plain, (![X_136]: (rrx1a(X_136, '#skF_3'(X_136)) | ~cSatisfiable(X_136)))).
% 3.71/1.81 tff(c_72, plain, (![X_77]: (rrx4a(X_77, '#skF_2'(X_77)) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_102, plain, (![X_112, Y_113]: (rrx2a(X_112, Y_113) | ~rrx4a(X_112, Y_113)))).
% 3.71/1.81 tff(c_96, plain, (![X_106, Y_107]: (rrxa(X_106, Y_107) | ~rrx4a(X_106, Y_107)))).
% 3.71/1.81 tff(c_68, plain, (![X_77]: (rrx3a(X_77, '#skF_3'(X_77)) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_94, plain, (![X_104, Y_105]: (rrx1(X_104, Y_105) | ~rrx3(X_104, Y_105)))).
% 3.71/1.81 tff(c_98, plain, (![X_108, Y_109]: (rrx(X_108, Y_109) | ~rrx3(X_108, Y_109)))).
% 3.71/1.81 tff(c_106, plain, (![X_116, Y_117]: (rrx1a(X_116, Y_117) | ~rrx3a(X_116, Y_117)))).
% 3.71/1.81 tff(c_100, plain, (![X_110, Y_111]: (rrx2(X_110, Y_111) | ~rrx4(X_110, Y_111)))).
% 3.71/1.81 tff(c_92, plain, (![X_102, Y_103]: (rrxa(X_102, Y_103) | ~rrx3a(X_102, Y_103)))).
% 3.71/1.81 tff(c_104, plain, (![X_114, Y_115]: (rrx(X_114, Y_115) | ~rrx4(X_114, Y_115)))).
% 3.71/1.81 tff(c_66, plain, (![X_77]: (cc1('#skF_3'(X_77)) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_70, plain, (![X_77]: (cc2('#skF_2'(X_77)) | ~cSatisfiable(X_77)))).
% 3.71/1.81 tff(c_60, plain, (![X_76]: (~xsd_integer(X_76) | ~xsd_string(X_76)))).
% 3.71/1.81 tff(c_62, plain, (![X_76]: (xsd_string(X_76) | xsd_integer(X_76)))).
% 3.71/1.81 tff(c_56, plain, (![X_75]: (cowlThing(X_75)))).
% 3.71/1.81 tff(c_58, plain, (![X_75]: (~cowlNothing(X_75)))).
% 3.71/1.81 tff(c_90, plain, (cSatisfiable(i2003_11_14_17_15_19316))).
% 3.71/1.81 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.71/1.81
%------------------------------------------------------------------------------