%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS030+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/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 : n007.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.96s 2.15s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.10 % Problem : KRS030+1 : TPTP v9.0.0. Released v3.1.0.
% 0.08/0.10 % 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.09/0.30 % Computer : n007.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Tue Apr 8 02:54:53 EDT 2025
% 0.09/0.30 % CPUTime :
% 3.96/2.15
% 3.96/2.15 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.96/2.15
% 3.96/2.15 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.96/2.16 %$ rs > rinvS > rinvF1 > rinvF > rf1 > rf > xsd_string > xsd_integer > cp > cowlThing > cowlNothing > cSatisfiable > #nlpp > i2003_11_14_17_15_26245 > #skF_2 > #skF_1
% 3.96/2.16
% 3.96/2.16 %Foreground sorts:
% 3.96/2.16
% 3.96/2.16
% 3.96/2.16 %Background operators:
% 3.96/2.16
% 3.96/2.16
% 3.96/2.16 %Foreground operators:
% 3.96/2.16 tff(rf, type, rf: ($i * $i) > $o).
% 3.96/2.16 tff(i2003_11_14_17_15_26245, type, i2003_11_14_17_15_26245: $i).
% 3.96/2.16 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.96/2.16 tff(cowlThing, type, cowlThing: $i > $o).
% 3.96/2.16 tff(rinvS, type, rinvS: ($i * $i) > $o).
% 3.96/2.16 tff(rs, type, rs: ($i * $i) > $o).
% 3.96/2.16 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.96/2.16 tff(rinvF, type, rinvF: ($i * $i) > $o).
% 3.96/2.16 tff(xsd_integer, type, xsd_integer: $i > $o).
% 3.96/2.16 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 3.96/2.16 tff(rf1, type, rf1: ($i * $i) > $o).
% 3.96/2.16 tff(xsd_string, type, xsd_string: $i > $o).
% 3.96/2.16 tff(cp, type, cp: $i > $o).
% 3.96/2.16 tff(rinvF1, type, rinvF1: ($i * $i) > $o).
% 3.96/2.16 tff(cowlNothing, type, cowlNothing: $i > $o).
% 3.96/2.16
% 3.96/2.16 %Saturated clause set:
% 3.96/2.16 tff(c_148, plain, (![X_68, X_119, Y_69]: (X_68=X_119 | ~rinvS(X_119, Y_69) | ~rinvS(X_68, Y_69)))).
% 3.96/2.16 tff(c_46, plain, (![X_51, Y_57, Y_56]: (cSatisfiable(X_51) | ~cp(Y_57) | ~rf(X_51, Y_57) | cp(Y_56) | ~rf1(X_51, Y_56)))).
% 3.96/2.16 tff(c_124, plain, (![Y_106, X_68, Y_69]: (Y_106=X_68 | ~rs(Y_69, Y_106) | ~rinvS(X_68, Y_69)))).
% 3.96/2.16 tff(c_132, plain, (![Y_112, X_51]: (Y_112='#skF_1'(X_51) | ~rf1(X_51, Y_112) | ~cSatisfiable(X_51)))).
% 3.96/2.16 tff(c_128, plain, (![Y_109, X_51]: (Y_109='#skF_2'(X_51) | ~rf(X_51, Y_109) | ~cSatisfiable(X_51)))).
% 3.96/2.17 tff(c_58, plain, (![Z_63, Y_62, X_61]: (Z_63=Y_62 | ~rf1(X_61, Z_63) | ~rf1(X_61, Y_62)))).
% 3.96/2.17 tff(c_56, plain, (![Z_60, Y_59, X_58]: (Z_60=Y_59 | ~rf(X_58, Z_60) | ~rf(X_58, Y_59)))).
% 3.96/2.17 tff(c_72, plain, (![Z_72, Y_71, X_70]: (Z_72=Y_71 | ~rs(X_70, Z_72) | ~rs(X_70, Y_71)))).
% 3.96/2.17 tff(c_118, plain, (![Y_69, X_68]: (rf1(Y_69, X_68) | ~rinvS(X_68, Y_69)))).
% 3.96/2.17 tff(c_101, plain, (![Y_69, X_68]: (rf(Y_69, X_68) | ~rinvS(X_68, Y_69)))).
% 3.96/2.17 tff(c_78, plain, (![X_75, Y_76]: (rf1(X_75, Y_76) | ~rs(X_75, Y_76)))).
% 3.96/2.17 tff(c_50, plain, (![X_51]: (rf(X_51, '#skF_2'(X_51)) | ~cSatisfiable(X_51)))).
% 3.96/2.17 tff(c_62, plain, (![X_64, Y_65]: (rinvF(X_64, Y_65) | ~rf(Y_65, X_64)))).
% 3.96/2.17 tff(c_54, plain, (![X_51]: (rf1(X_51, '#skF_1'(X_51)) | ~cSatisfiable(X_51)))).
% 3.96/2.17 tff(c_64, plain, (![Y_67, X_66]: (rf1(Y_67, X_66) | ~rinvF1(X_66, Y_67)))).
% 3.96/2.17 tff(c_76, plain, (![X_73, Y_74]: (rf(X_73, Y_74) | ~rs(X_73, Y_74)))).
% 3.96/2.17 tff(c_60, plain, (![Y_65, X_64]: (rf(Y_65, X_64) | ~rinvF(X_64, Y_65)))).
% 3.96/2.17 tff(c_66, plain, (![X_66, Y_67]: (rinvF1(X_66, Y_67) | ~rf1(Y_67, X_66)))).
% 3.96/2.17 tff(c_70, plain, (![X_68, Y_69]: (rinvS(X_68, Y_69) | ~rs(Y_69, X_68)))).
% 3.96/2.17 tff(c_68, plain, (![Y_69, X_68]: (rs(Y_69, X_68) | ~rinvS(X_68, Y_69)))).
% 3.96/2.17 tff(c_52, plain, (![X_51]: (~cp('#skF_1'(X_51)) | ~cSatisfiable(X_51)))).
% 3.96/2.17 tff(c_48, plain, (![X_51]: (cp('#skF_2'(X_51)) | ~cSatisfiable(X_51)))).
% 3.96/2.17 tff(c_44, plain, (![X_50]: (xsd_string(X_50) | xsd_integer(X_50)))).
% 3.96/2.17 tff(c_42, plain, (![X_50]: (~xsd_integer(X_50) | ~xsd_string(X_50)))).
% 3.96/2.17 tff(c_38, plain, (![X_49]: (cowlThing(X_49)))).
% 3.96/2.17 tff(c_40, plain, (![X_49]: (~cowlNothing(X_49)))).
% 3.96/2.17 tff(c_74, plain, (cSatisfiable(i2003_11_14_17_15_26245))).
% 3.96/2.17 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.96/2.17
%------------------------------------------------------------------------------