%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC473_1 : TPTP v9.0.0. Released v9.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 : 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 09:20:30 PM UTC 2025
% Result : Theorem 5.89s 2.53s
% Output : CNFRefutation 5.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWC473_1 : TPTP v9.0.0. Released v9.0.0.
% 0.11/0.13 % 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.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 02:32:24 EDT 2025
% 0.13/0.34 % CPUTime :
% 5.89/2.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.89/2.54
% 5.89/2.54 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.89/2.54 %$ u0 > mod:(Int*Int)>Int > #nlpp > v0 > small > h0 > g0 > fast
% 5.89/2.54
% 5.89/2.54 %Foreground sorts:
% 5.89/2.54
% 5.89/2.54
% 5.89/2.54 %Background operators:
% 5.89/2.54 tff('#skE_7', type, '#skE_7': $int).
% 5.89/2.54 tff('#skE_11', type, '#skE_11': $int).
% 5.89/2.54 tff('#skE_12', type, '#skE_12': $int).
% 5.89/2.54 tff('#skE_2', type, '#skE_2': $int).
% 5.89/2.54 tff('#skE_1', type, '#skE_1': $int).
% 5.89/2.54 tff('#skE_6', type, '#skE_6': $int).
% 5.89/2.54 tff('#skE_13', type, '#skE_13': $int).
% 5.89/2.54 tff('#skE_10', type, '#skE_10': $int).
% 5.89/2.54 tff('#skE_5', type, '#skE_5': $int).
% 5.89/2.54 tff('#skE_15', type, '#skE_15': $int).
% 5.89/2.54 tff('#skE_8', type, '#skE_8': $int).
% 5.89/2.54 tff('#skE_4', type, '#skE_4': $int).
% 5.89/2.54 tff('#skE_3', type, '#skE_3': $int).
% 5.89/2.54 tff('#skF_1', type, '#skF_1': $int).
% 5.89/2.54 tff('#skE_9', type, '#skE_9': $int).
% 5.89/2.54 tff(f0, type, f0: $int).
% 5.89/2.54 tff('#skE_14', type, '#skE_14': $int).
% 5.89/2.54
% 5.89/2.54 %Foreground operators:
% 5.89/2.54 tff(mod:(Int*Int)>Int, type, mod:(Int*Int)>Int: ($int * $int) > $int).
% 5.89/2.54 tff(fast, type, fast: $int > $int).
% 5.89/2.54 tff(small, type, small: $int > $int).
% 5.89/2.54 tff(u0, type, u0: ($int * $int) > $int).
% 5.89/2.54 tff(v0, type, v0: $int > $int).
% 5.89/2.54 tff(g0, type, g0: $int > $int).
% 5.89/2.54 tff(h0, type, h0: $int > $int).
% 5.89/2.55
% 5.89/2.56 tff(f_72, negated_conjecture, ~~(?[Ca:$int]: ($greatereq(Ca, 0) & ~(small(Ca) = fast(Ca)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture_1)).
% 5.89/2.56 tff(f_45, axiom, (![Xa:$int]: (g0(Xa) = mod(Xa, 2))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_3)).
% 5.89/2.56 tff(f_40, axiom, (![Xa:$int]: (($lesseq(mod(Xa, 2), 0) => (small(Xa) = $sum(1, $sum($product(Xa, Xa), Xa)))) & (~$lesseq(mod(Xa, 2), 0) => (small(Xa) = $sum(1, $sum($product(0, Xa), Xa)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_1)).
% 5.89/2.56 tff(f_48, axiom, (![Xa:$int]: (h0(Xa) = Xa)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_4)).
% 5.89/2.56 tff(f_61, axiom, (![Xa:$int]: (v0(Xa) = u0(g0(Xa), h0(Xa)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_6)).
% 5.89/2.56 tff(f_58, axiom, (![Xa:$int, Ya:$int]: (($lesseq(Xa, 0) => (u0(Xa, Ya) = Ya)) & (~$lesseq(Xa, 0) => (u0(Xa, Ya) = f0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_5)).
% 5.89/2.56 tff(f_64, axiom, (![Xa:$int]: (fast(Xa) = $sum(1, $sum($product(v0(Xa), Xa), Xa)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_7)).
% 5.89/2.56 tff(f_42, axiom, (f0 = 0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_2)).
% 5.89/2.56 tff(f_362, axiom, (![C:$int, B:$int]: (($product(C, B) = C) <=> ((C = 0) | (B = 1)))), file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p', mult_cancel_right1)).
% 5.89/2.56 tff(c_52, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_72])).
% 5.89/2.56 tff(c_164, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_52])).
% 5.89/2.56 tff(c_163, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_52])).
% 5.89/2.56 tff(c_80, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_72])).
% 5.89/2.56 tff(c_175, plain, ('#skE_2'!='#skE_1'), inference(demodulation, [status(thm), theory('equality')], [c_164, c_163, c_80])).
% 5.89/2.56 tff(c_61, plain, (![X_2a:$int]: (mod(X_2a, 2)=g0(X_2a))), inference(cnfTransformation, [status(thm)], [f_45])).
% 5.89/2.56 tff(c_5, plain, (![X_1a:$int]: (small(X_1a)=$sum(1, X_1a) | $lesseq(mod(X_1a, 2), 0))), inference(cnfTransformation, [status(thm)], [f_40])).
% 5.89/2.56 tff(c_63, plain, (![X_1a:$int]: (small(X_1a)=$sum(1, X_1a) | ~$less(0, mod(X_1a, 2)))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_5])).
% 5.89/2.56 tff(c_206, plain, (![X_62a:$int]: (small(X_62a)=$sum(1, X_62a) | ~$less(0, g0(X_62a)))), inference(demodulation, [status(thm), theory('equality')], [c_61, c_63])).
% 5.89/2.56 tff(c_171, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_52])).
% 5.89/2.56 tff(c_221, plain, ($sum(1, '#skF_1')='#skE_1' | ~$less(0, g0('#skF_1'))), inference(superposition, [status(thm), theory('equality')], [c_206, c_171])).
% 5.89/2.56 tff(c_224, plain, ('#skF_1'=$sum($uminus(1), '#skE_1') | ~$less(0, g0('#skF_1'))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_221])).
% 5.89/2.56 tff(c_233, plain, (g0('#skF_1')='#skE_3'), inference(define, [status(thm), theory('equality')], [c_224])).
% 5.89/2.56 tff(c_232, plain, ('#skF_1'=$sum($uminus(1), '#skE_1') | ~$less(0, g0('#skF_1'))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_221])).
% 5.89/2.56 tff(c_240, plain, ('#skF_1'=$sum($uminus(1), '#skE_1') | ~$less(0, '#skE_3')), inference(demodulation, [status(thm), theory('equality')], [c_233, c_232])).
% 5.89/2.56 tff(c_264, plain, (~$less(0, '#skE_3')), inference(splitLeft, [status(thm)], [c_240])).
% 5.89/2.56 tff(c_243, plain, (g0('#skF_1')='#skE_3'), inference(define, [status(thm), theory('equality')], [c_224])).
% 5.89/2.56 tff(c_60, plain, (![X_3a:$int]: (h0(X_3a)=X_3a)), inference(cnfTransformation, [status(thm)], [f_48])).
% 5.89/2.56 tff(c_57, plain, (![X_6a:$int]: (u0(g0(X_6a), h0(X_6a))=v0(X_6a))), inference(cnfTransformation, [status(thm)], [f_61])).
% 5.89/2.56 tff(c_85, plain, (![X_6a:$int]: (u0(g0(X_6a), X_6a)=v0(X_6a))), inference(demodulation, [status(thm), theory('equality')], [c_60, c_57])).
% 5.89/2.56 tff(c_259, plain, (u0('#skE_3', '#skF_1')=v0('#skF_1')), inference(superposition, [status(thm), theory('equality')], [c_243, c_85])).
% 5.89/2.56 tff(c_693, plain, (u0('#skE_3', '#skF_1')='#skE_8'), inference(define, [status(thm), theory('equality')], [c_259])).
% 5.89/2.56 tff(c_12, plain, (![X_4a:$int, Y_5a:$int]: (u0(X_4a, Y_5a)=Y_5a | ~$lesseq(X_4a, 0))), inference(cnfTransformation, [status(thm)], [f_58])).
% 5.89/2.56 tff(c_59, plain, (![X_4a:$int, Y_5a:$int]: (u0(X_4a, Y_5a)=Y_5a | $less(0, X_4a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_12])).
% 5.89/2.56 tff(c_716, plain, ('#skF_1'='#skE_8' | $less(0, '#skE_3')), inference(superposition, [status(thm), theory('equality')], [c_693, c_59])).
% 5.89/2.56 tff(c_727, plain, ('#skF_1'='#skE_8'), inference(negUnitSimplification, [status(thm)], [c_264, c_716])).
% 5.89/2.56 tff(c_239, plain, (g0('#skF_1')='#skE_3'), inference(define, [status(thm), theory('equality')], [c_224])).
% 5.89/2.56 tff(c_833, plain, (g0('#skE_8')='#skE_3'), inference(demodulation, [status(thm), theory('equality')], [c_727, c_239])).
% 5.89/2.56 tff(c_777, plain, (small('#skE_8')='#skE_1'), inference(demodulation, [status(thm), theory('equality')], [c_727, c_171])).
% 5.89/2.56 tff(c_177, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_52])).
% 5.89/2.56 tff(c_596, plain, (v0('#skF_1')='#skE_9'), inference(define, [status(thm), theory('equality')], [c_259])).
% 5.89/2.56 tff(c_595, plain, (u0('#skE_3', '#skF_1')='#skE_8'), inference(define, [status(thm), theory('equality')], [c_259])).
% 5.89/2.56 tff(c_594, plain, (u0('#skE_3', '#skF_1')=v0('#skF_1')), inference(superposition, [status(thm), theory('equality')], [c_243, c_85])).
% 5.89/2.56 tff(c_607, plain, ('#skE_9'='#skE_8'), inference(demodulation, [status(thm), theory('equality')], [c_596, c_595, c_594])).
% 5.89/2.56 tff(c_606, plain, (v0('#skF_1')='#skE_9'), inference(define, [status(thm), theory('equality')], [c_259])).
% 5.89/2.56 tff(c_659, plain, (v0('#skF_1')='#skE_8'), inference(demodulation, [status(thm), theory('equality')], [c_607, c_606])).
% 5.89/2.56 tff(c_19, plain, (![X_7a:$int]: ($sum(1, $sum(X_7a, $product(v0(X_7a), X_7a)))=fast(X_7a))), inference(cnfTransformation, [status(thm)], [f_64])).
% 5.89/2.56 tff(c_56, plain, (![X_7a:$int]: ($product(v0(X_7a), X_7a)=$sum($uminus(1), $sum($uminus(X_7a), fast(X_7a))))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_19])).
% 5.89/2.56 tff(c_669, plain, ($product('#skE_8', '#skF_1')=$sum($uminus(1), $sum($uminus('#skF_1'), fast('#skF_1')))), inference(superposition, [status(thm), theory('equality')], [c_659, c_56])).
% 5.89/2.56 tff(c_684, plain, ($product('#skE_8', '#skF_1')=$sum($uminus(1), $sum($uminus('#skF_1'), '#skE_2'))), inference(demodulation, [status(thm), theory('equality')], [c_177, c_669])).
% 5.89/2.56 tff(c_1987, plain, ($product('#skE_8', '#skE_8')=$sum($uminus(1), $sum($uminus('#skE_8'), '#skE_2'))), inference(demodulation, [status(thm), theory('equality')], [c_727, c_727, c_684])).
% 5.89/2.56 tff(c_2, plain, (![X_1a:$int]: ($sum(1, $sum(X_1a, $product(X_1a, X_1a)))=small(X_1a) | ~$lesseq(mod(X_1a, 2), 0))), inference(cnfTransformation, [status(thm)], [f_40])).
% 5.89/2.56 tff(c_67, plain, (![X_1a:$int]: ($product(X_1a, X_1a)=$sum($uminus(1), $sum($uminus(X_1a), small(X_1a))) | $less(0, mod(X_1a, 2)))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_2])).
% 5.89/2.56 tff(c_95, plain, (![X_1a:$int]: ($product(X_1a, X_1a)=$sum($uminus(1), $sum($uminus(X_1a), small(X_1a))) | $less(0, g0(X_1a)))), inference(demodulation, [status(thm), theory('equality')], [c_61, c_67])).
% 5.89/2.56 tff(c_2003, plain, ($sum($uminus(1), $sum($uminus('#skE_8'), small('#skE_8')))=$sum($uminus(1), $sum($uminus('#skE_8'), '#skE_2')) | $less(0, g0('#skE_8')) | '#skE_8'!='#skE_8'), inference(superposition, [status(thm), theory('equality')], [c_1987, c_95])).
% 5.89/2.56 tff(c_2095, plain, ($sum($uminus(1), $sum($uminus('#skE_8'), '#skE_2'))=$sum($uminus(1), $sum($uminus('#skE_8'), '#skE_1')) | $less(0, '#skE_3')), inference(demodulation, [status(thm), theory('equality')], [c_833, c_777, c_2003])).
% 5.89/2.56 tff(c_2096, plain, ($sum($uminus(1), $sum($uminus('#skE_8'), '#skE_2'))=$sum($uminus(1), $sum($uminus('#skE_8'), '#skE_1'))), inference(negUnitSimplification, [status(thm)], [c_264, c_2095])).
% 5.89/2.56 tff(c_2098, plain, ('#skE_2'='#skE_1'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_2096])).
% 5.89/2.56 tff(c_2179, plain, $false, inference(negUnitSimplification, [status(thm)], [c_175, c_2098])).
% 5.89/2.56 tff(c_2182, plain, ('#skF_1'=$sum($uminus(1), '#skE_1')), inference(splitRight, [status(thm)], [c_240])).
% 5.89/2.56 tff(c_174, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_52])).
% 5.89/2.56 tff(c_2393, plain, (fast($sum($uminus(1), '#skE_1'))='#skE_2'), inference(demodulation, [status(thm), theory('equality')], [c_2182, c_174])).
% 5.89/2.56 tff(c_2183, plain, ($less(0, '#skE_3')), inference(splitRight, [status(thm)], [c_240])).
% 5.89/2.56 tff(c_2983, plain, (u0('#skE_3', $sum($uminus(1), '#skE_1'))=v0($sum($uminus(1), '#skE_1'))), inference(demodulation, [status(thm), theory('equality')], [c_2182, c_2182, c_259])).
% 5.89/2.56 tff(c_2986, plain, (v0($sum($uminus(1), '#skE_1'))='#skE_15'), inference(define, [status(thm), theory('equality')], [c_2983])).
% 5.89/2.56 tff(c_2985, plain, (u0('#skE_3', $sum($uminus(1), '#skE_1'))='#skE_14'), inference(define, [status(thm), theory('equality')], [c_2983])).
% 5.89/2.56 tff(c_2984, plain, (u0('#skE_3', $sum($uminus(1), '#skE_1'))=v0($sum($uminus(1), '#skE_1'))), inference(demodulation, [status(thm), theory('equality')], [c_2182, c_2182, c_259])).
% 5.89/2.56 tff(c_2997, plain, ('#skE_15'='#skE_14'), inference(demodulation, [status(thm), theory('equality')], [c_2986, c_2985, c_2984])).
% 5.89/2.56 tff(c_2996, plain, (v0($sum($uminus(1), '#skE_1'))='#skE_15'), inference(define, [status(thm), theory('equality')], [c_2983])).
% 5.89/2.56 tff(c_3072, plain, (v0($sum($uminus(1), '#skE_1'))='#skE_14'), inference(demodulation, [status(thm), theory('equality')], [c_2997, c_2996])).
% 5.89/2.56 tff(c_2214, plain, (g0($sum($uminus(1), '#skE_1'))='#skE_3'), inference(demodulation, [status(thm), theory('equality')], [c_2182, c_239])).
% 5.89/2.56 tff(c_2230, plain, (u0('#skE_3', $sum($uminus(1), '#skE_1'))=v0($sum($uminus(1), '#skE_1'))), inference(superposition, [status(thm), theory('equality')], [c_2214, c_85])).
% 5.89/2.56 tff(c_3141, plain, (u0('#skE_3', $sum($uminus(1), '#skE_1'))='#skE_14'), inference(demodulation, [status(thm), theory('equality')], [c_3072, c_2230])).
% 5.89/2.56 tff(c_62, plain, (f0=0), inference(cnfTransformation, [status(thm)], [f_42])).
% 5.89/2.56 tff(c_14, plain, (![X_4a:$int, Y_5a:$int]: (u0(X_4a, Y_5a)=f0 | $lesseq(X_4a, 0))), inference(cnfTransformation, [status(thm)], [f_58])).
% 5.89/2.56 tff(c_58, plain, (![X_4a:$int, Y_5a:$int]: (u0(X_4a, Y_5a)=f0 | ~$less(0, X_4a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_14])).
% 5.89/2.56 tff(c_87, plain, (![X_4a:$int, Y_5a:$int]: (u0(X_4a, Y_5a)=0 | ~$less(0, X_4a))), inference(demodulation, [status(thm), theory('equality')], [c_62, c_58])).
% 5.89/2.56 tff(c_3154, plain, ('#skE_14'=0 | ~$less(0, '#skE_3')), inference(superposition, [status(thm), theory('equality')], [c_3141, c_87])).
% 5.89/2.56 tff(c_3179, plain, ('#skE_14'=0), inference(demodulation, [status(thm), theory('equality')], [c_2183, c_3154])).
% 5.89/2.56 tff(c_3071, plain, (v0($sum($uminus(1), '#skE_1'))='#skE_14'), inference(demodulation, [status(thm), theory('equality')], [c_2997, c_2996])).
% 5.89/2.56 tff(c_3350, plain, (v0($sum($uminus(1), '#skE_1'))=0), inference(demodulation, [status(thm), theory('equality')], [c_3179, c_3071])).
% 5.89/2.56 tff(c_3362, plain, ($product(0, $sum($uminus(1), '#skE_1'))=$sum($uminus(1), $sum($uminus($sum($uminus(1), '#skE_1')), fast($sum($uminus(1), '#skE_1'))))), inference(superposition, [status(thm), theory('equality')], [c_3350, c_56])).
% 5.89/2.56 tff(c_3382, plain, ($product(0, $sum($uminus(1), '#skE_1'))=$sum($uminus(1), $sum($uminus($sum($uminus(1), '#skE_1')), '#skE_2'))), inference(demodulation, [status(thm), theory('equality')], [c_2393, c_3362])).
% 5.89/2.56 tff(c_3403, plain, ($product(0, $sum($uminus(1), '#skE_1'))=$sum($uminus('#skE_1'), '#skE_2')), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_3382])).
% 5.89/2.56 tff(c_69, plain, (![B_31:$int]: ($product(0, B_31)=0)), inference(cnfTransformation, [status(thm)], [f_362])).
% 5.89/2.56 tff(c_3548, plain, ($sum($uminus('#skE_1'), '#skE_2')=0), inference(superposition, [status(thm), theory('equality')], [c_3403, c_69])).
% 5.89/2.56 tff(c_3550, plain, ('#skE_2'='#skE_1'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_3548])).
% 5.89/2.56 tff(c_3595, plain, $false, inference(negUnitSimplification, [status(thm)], [c_175, c_3550])).
% 5.89/2.56 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------