%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ITP001_1 : TPTP v9.0.0. Released v8.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 : n023.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 06:53:41 PM UTC 2025
% Result : Theorem 10.91s 3.42s
% Output : CNFRefutation 10.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : ITP001_1 : TPTP v9.0.0. Released v8.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.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 02:19:24 EDT 2025
% 0.14/0.34 % CPUTime :
% 10.91/3.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.91/3.43
% 10.91/3.43 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.91/3.43 %$ member$ > fun_app$ > eventually$ > uui$ > uuh$ > uvd$ > uvb$ > uve$ > uuz$ > uuy$ > uux$ > uuq$ > uup$ > uuo$ > uun$ > uum$ > uuk$ > uuj$ > uug$ > fun_app$b > fun_app$a > #nlpp > uvc$ > uva$ > uuw$ > uuv$ > uuu$ > uur$ > uul$ > uud$ > times$ > rnatmod$ > divide$ > collect$ > uut$ > uus$ > uuf$ > uue$ > uuc$ > uub$ > uua$ > uu$ > tltrue > tlfalse > tanh$ > rfloor$ > rceil$ > ln$ > lambert_W$ > exp$ > at_top$ > artanh$ > arsinh$ > arcosh$ > a$ > #skF_6 > #skF_1 > #skF_2 > #skF_8 > #skF_5 > #skF_7 > #skF_19 > #skF_4 > #skF_13 > #skF_9 > #skF_16 > #skF_12 > #skF_3 > #skF_14 > #skF_15 > #skF_17 > #skF_11 > #skF_10 > #skF_18
% 10.91/3.43
% 10.91/3.43 %Foreground sorts:
% 10.91/3.43 tff(Real_real_bool_fun_fun$, type, Real_real_bool_fun_fun$: $tType ).
% 10.91/3.43 tff(Real_set$, type, Real_set$: $tType ).
% 10.91/3.43 tff(tlbool, type, tlbool: $tType ).
% 10.91/3.43 tff(Real_filter$, type, Real_filter$: $tType ).
% 10.91/3.43 tff(Real_bool_fun$, type, Real_bool_fun$: $tType ).
% 10.91/3.43 tff(Real_real_fun$, type, Real_real_fun$: $tType ).
% 10.91/3.43
% 10.91/3.43 %Background operators:
% 10.91/3.43 tff(c$, type, c$: $real).
% 10.91/3.43
% 10.91/3.43 %Foreground operators:
% 10.91/3.43 tff(uus$, type, uus$: Real_real_fun$).
% 10.91/3.43 tff('#skF_6', type, '#skF_6': (Real_set$ * $real) > $real).
% 10.91/3.43 tff(uum$, type, uum$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uuw$, type, uuw$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43 tff(arcosh$, type, arcosh$: Real_real_fun$).
% 10.91/3.43 tff(divide$, type, divide$: $real > Real_real_fun$).
% 10.91/3.43 tff('#skF_1', type, '#skF_1': (Real_bool_fun$ * Real_bool_fun$) > $real).
% 10.91/3.43 tff(uur$, type, uur$: $real > Real_real_fun$).
% 10.91/3.43 tff(fun_app$, type, fun_app$: (Real_bool_fun$ * $real) > $o).
% 10.91/3.43 tff('#skF_2', type, '#skF_2': (Real_bool_fun$ * Real_bool_fun$) > $real).
% 10.91/3.43 tff(tanh$, type, tanh$: Real_real_fun$).
% 10.91/3.43 tff(uuj$, type, uuj$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(eventually$, type, eventually$: (Real_bool_fun$ * Real_filter$) > $o).
% 10.91/3.43 tff(uui$, type, uui$: (Real_real_fun$ * Real_real_fun$ * Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uuc$, type, uuc$: Real_bool_fun$).
% 10.91/3.43 tff(collect$, type, collect$: Real_bool_fun$ > Real_set$).
% 10.91/3.43 tff(uu$, type, uu$: Real_bool_fun$).
% 10.91/3.43 tff('#skF_8', type, '#skF_8': (Real_real_bool_fun_fun$ * $real * $real) > $real).
% 10.91/3.43 tff('#skF_5', type, '#skF_5': Real_set$ > $real).
% 10.91/3.43 tff(uvd$, type, uvd$: (Real_real_fun$ * Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uvb$, type, uvb$: (Real_real_fun$ * Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff('#skF_7', type, '#skF_7': (Real_real_bool_fun_fun$ * $real * $real) > $real).
% 10.91/3.43 tff(tlfalse, type, tlfalse: tlbool).
% 10.91/3.43 tff(uug$, type, uug$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(fun_app$a, type, fun_app$a: (Real_real_fun$ * $real) > $real).
% 10.91/3.43 tff(a$, type, a$: Real_real_fun$).
% 10.91/3.43 tff(uua$, type, uua$: Real_bool_fun$).
% 10.91/3.43 tff(uuy$, type, uuy$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uuh$, type, uuh$: (Real_real_fun$ * Real_real_fun$ * Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(rfloor$, type, rfloor$: Real_real_fun$).
% 10.91/3.43 tff(member$, type, member$: ($real * Real_set$) > $o).
% 10.91/3.43 tff(uuq$, type, uuq$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(artanh$, type, artanh$: Real_real_fun$).
% 10.91/3.43 tff('#skF_19', type, '#skF_19': $real > $real).
% 10.91/3.43 tff(uuf$, type, uuf$: Real_real_fun$).
% 10.91/3.43 tff('#skF_4', type, '#skF_4': (Real_set$ * $real) > $real).
% 10.91/3.43 tff(arsinh$, type, arsinh$: Real_real_fun$).
% 10.91/3.43 tff('#skF_13', type, '#skF_13': ($real * $real * Real_real_fun$ * $real) > $real).
% 10.91/3.43 tff(rceil$, type, rceil$: Real_real_fun$).
% 10.91/3.43 tff(uve$, type, uve$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uut$, type, uut$: Real_real_fun$).
% 10.91/3.43 tff(uub$, type, uub$: Real_bool_fun$).
% 10.91/3.43 tff('#skF_9', type, '#skF_9': (Real_real_bool_fun_fun$ * $real * $real) > $real).
% 10.91/3.43 tff('#skF_16', type, '#skF_16': ($real * Real_real_fun$ * $real * $real) > $real).
% 10.91/3.43 tff(exp$, type, exp$: Real_real_fun$).
% 10.91/3.43 tff(uva$, type, uva$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43 tff(fun_app$b, type, fun_app$b: (Real_real_bool_fun_fun$ * $real) > Real_bool_fun$).
% 10.91/3.43 tff('#skF_12', type, '#skF_12': ($real * Real_real_fun$ * $real * $real) > $real).
% 10.91/3.43 tff('#skF_3', type, '#skF_3': $real > $real).
% 10.91/3.43 tff(ln$, type, ln$: Real_real_fun$).
% 10.91/3.43 tff(lambert_W$, type, lambert_W$: Real_real_fun$).
% 10.91/3.43 tff(uuo$, type, uuo$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uuz$, type, uuz$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff('#skF_14', type, '#skF_14': ($real * $real * Real_real_fun$ * $real) > $real).
% 10.91/3.43 tff(uun$, type, uun$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff('#skF_15', type, '#skF_15': ($real * Real_real_fun$ * $real * $real) > $real).
% 10.91/3.43 tff(uue$, type, uue$: Real_real_fun$).
% 10.91/3.43 tff(rnatmod$, type, rnatmod$: $real > Real_real_fun$).
% 10.91/3.43 tff(uul$, type, uul$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43 tff(tltrue, type, tltrue: tlbool).
% 10.91/3.43 tff(uud$, type, uud$: Real_set$ > Real_bool_fun$).
% 10.91/3.43 tff(uuk$, type, uuk$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(uup$, type, uup$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff('#skF_17', type, '#skF_17': ($real * $real * Real_real_fun$ * $real) > $real).
% 10.91/3.43 tff('#skF_11', type, '#skF_11': ($real * Real_real_fun$ * $real * $real) > $real).
% 10.91/3.43 tff(times$, type, times$: $real > Real_real_fun$).
% 10.91/3.43 tff('#skF_10', type, '#skF_10': (Real_real_bool_fun_fun$ * $real * $real) > $real).
% 10.91/3.43 tff(uuu$, type, uuu$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43 tff(uuv$, type, uuv$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43 tff('#skF_18', type, '#skF_18': ($real * $real * Real_real_fun$ * $real) > $real).
% 10.91/3.43 tff(uux$, type, uux$: (Real_real_fun$ * Real_real_fun$) > Real_bool_fun$).
% 10.91/3.43 tff(at_top$, type, at_top$: Real_filter$).
% 10.91/3.43 tff(uvc$, type, uvc$: Real_real_fun$ > Real_bool_fun$).
% 10.91/3.43
% 10.91/3.44 tff(f_2376, axiom, (![A__questionmark_v0a:$real, A__questionmark_v1a:$real, A__questionmark_v2a:$real]: ((A__questionmark_v0a = $uminus(fun_app$a(divide$(A__questionmark_v1a), A__questionmark_v2a))) <=> ((~(A__questionmark_v2a = 0) => (fun_app$a(times$(A__questionmark_v0a), A__questionmark_v2a) = $uminus(A__questionmark_v1a))) & (~~(A__questionmark_v2a = 0) => (A__questionmark_v0a = 0))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom432)).
% 10.91/3.44 tff(f_2485, axiom, (![A__questionmark_v0a:$real, A__questionmark_v1a:$real, A__questionmark_v2a:$real]: (((A__questionmark_v1a = 0) => ($difference($uminus(fun_app$a(divide$(A__questionmark_v0a), A__questionmark_v1a)), A__questionmark_v2a) = $uminus(A__questionmark_v2a))) & (~(A__questionmark_v1a = 0) => ($difference($uminus(fun_app$a(divide$(A__questionmark_v0a), A__questionmark_v1a)), A__questionmark_v2a) = fun_app$a(divide$($difference($uminus(A__questionmark_v0a), fun_app$a(times$(A__questionmark_v2a), A__questionmark_v1a))), A__questionmark_v1a))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom447)).
% 10.91/3.44 tff(f_2179, axiom, (![A__questionmark_v0a:$real, A__questionmark_v1a:$real]: (($sum(A__questionmark_v0a, A__questionmark_v1a) = 0) <=> (A__questionmark_v1a = $uminus(A__questionmark_v0a)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom405)).
% 10.91/3.44 tff(f_2528, axiom, (![A__questionmark_v0a:$real]: (($sum(A__questionmark_v0a, A__questionmark_v0a) = 0) <=> (A__questionmark_v0a = 0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom454)).
% 10.91/3.44 tff(c_1367, plain, (![A__questionmark_v1_955a:$real]: ($uminus(fun_app$a(divide$(A__questionmark_v1_955a), 0))=0)), inference(cnfTransformation, [status(thm)], [f_2376])).
% 10.91/3.44 tff(c_1413, plain, (![A__questionmark_v0_993a:$real, A__questionmark_v2_995a:$real]: ($difference($uminus(fun_app$a(divide$(A__questionmark_v0_993a), 0)), A__questionmark_v2_995a)=$uminus(A__questionmark_v2_995a))), inference(cnfTransformation, [status(thm)], [f_2485])).
% 10.91/3.44 tff(c_1654, plain, (![A__questionmark_v2_995a:$real]: ($uminus(A__questionmark_v2_995a)=$difference(0, A__questionmark_v2_995a))), inference(demodulation, [status(thm), theory('equality')], [c_1367, c_1413])).
% 10.91/3.44 tff(c_1655, plain, (![A__questionmark_v2_995a:$real]: ($uminus(A__questionmark_v2_995a)=A__questionmark_v2_995a)), inference(backgroundSimplification, [status(thm), theory('LFA')], [c_1654])).
% 10.91/3.44 tff(c_1299, plain, (![A__questionmark_v0_890a:$real]: ($sum(A__questionmark_v0_890a, $uminus(A__questionmark_v0_890a))=0)), inference(cnfTransformation, [status(thm)], [f_2179])).
% 10.91/3.44 tff(c_1685, plain, (![A__questionmark_v0_890a:$real]: ($sum(A__questionmark_v0_890a, A__questionmark_v0_890a)=0)), inference(demodulation, [status(thm), theory('equality')], [c_1655, c_1299])).
% 10.91/3.44 tff(c_1432, plain, (![A__questionmark_v0_1006a:$real]: ($sum(A__questionmark_v0_1006a, A__questionmark_v0_1006a)!=0 | A__questionmark_v0_1006a=0)), inference(cnfTransformation, [status(thm)], [f_2528])).
% 10.91/3.44 tff(c_1687, plain, (![A__questionmark_v0_1006a:$real]: (A__questionmark_v0_1006a=0)), inference(demodulation, [status(thm), theory('equality')], [c_1685, c_1432])).
% 10.91/3.44 tff(c_2042, plain, $false, inference(quantifierElimination, [status(thm), theory('LFA')], [c_1687])).
% 10.91/3.44 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------