%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO641+1 : TPTP v9.0.0. Released v7.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 : n013.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 10:38:01 PM UTC 2025
% Result : Satisfiable 2.59s 1.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYO641+1 : TPTP v9.0.0. Released v7.1.0.
% 0.06/0.12 % 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.12/0.34 % Computer : n013.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 09:39:47 EDT 2025
% 0.12/0.34 % CPUTime :
% 2.59/1.61
% 2.59/1.61 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.59/1.61
% 2.59/1.61 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.59/1.62 %$ f > #nlpp > #skF_1 > #skF_2 > #skF_3
% 2.59/1.62
% 2.59/1.62 %Foreground sorts:
% 2.59/1.62
% 2.59/1.62
% 2.59/1.62 %Background operators:
% 2.59/1.62
% 2.59/1.62
% 2.59/1.62 %Foreground operators:
% 2.59/1.62 tff('#skF_1', type, '#skF_1': $i > $i).
% 2.59/1.62 tff(f, type, f: ($i * $i * $i) > $o).
% 2.59/1.62 tff('#skF_2', type, '#skF_2': $i).
% 2.59/1.62 tff('#skF_3', type, '#skF_3': $i).
% 2.59/1.62
% 2.59/1.62 %Saturated clause set:
% 2.59/1.62 tff(c_50, plain, (![X1_20, X3_60]: (~f(X1_20, X3_60, '#skF_1'(X1_20)) | ~f(X1_20, X1_20, '#skF_1'(X1_20))))).
% 2.59/1.62 tff(c_28, plain, (![X1_49, X1_20, X1_46, X3_25]: (~f(X1_49, '#skF_1'(X1_20), '#skF_1'(X1_49)) | ~f(X1_46, '#skF_1'(X1_49), '#skF_1'(X1_46)) | ~f(X1_20, X3_25, '#skF_1'(X1_20))))).
% 2.59/1.62 tff(c_34, plain, (![X1_52]: (~f(X1_52, '#skF_1'('#skF_2'), '#skF_1'(X1_52))))).
% 2.59/1.63 tff(c_29, plain, (![X1_49, X1_46]: (~f(X1_49, '#skF_3', '#skF_1'(X1_49)) | ~f(X1_46, '#skF_1'(X1_49), '#skF_1'(X1_46))))).
% 2.59/1.63 tff(c_22, plain, (![X3_42, X4_41, X1_20, X8_45, X1_40]: (~f(X4_41, X3_42, X8_45) | ~f(X1_40, X3_42, '#skF_1'(X1_40)) | ~f(X1_20, '#skF_1'(X1_40), '#skF_1'(X1_20))))).
% 2.59/1.63 tff(c_14, plain, (![X9_33, X1_20, X3_25, X8_37, X6_35, X4_34]: (~f('#skF_1'(X1_20), X6_35, X9_33) | ~f(X4_34, X3_25, X8_37) | ~f(X1_20, X3_25, '#skF_1'(X1_20))))).
% 2.59/1.63 tff(c_16, plain, (![X4_34, X8_37]: (~f(X4_34, '#skF_2', X8_37)))).
% 2.59/1.63 tff(c_2, plain, (![X6_17, X5_13, X8_12, X10_19, X4_11, X2_1, X9_18]: (~f(X2_1, X5_13, X10_19) | ~f(X5_13, X6_17, X9_18) | ~f(X4_11, X2_1, X8_12)))).
% 2.59/1.63 tff(c_4, plain, (![X1_20, X3_25]: (~f(X1_20, X3_25, '#skF_1'(X1_20)) | f(X3_25, '#skF_1'(X1_20), '#skF_1'(X1_20))))).
% 2.59/1.63 tff(c_6, plain, (![X7_27]: (f('#skF_2', '#skF_3', X7_27)))).
% 2.59/1.63 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.59/1.63
%------------------------------------------------------------------------------