%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC484_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/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 : n032.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 10.78s 3.62s
% Output : CNFRefutation 10.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.09 % Problem : SWC484_1 : TPTP v9.0.0. Released v9.0.0.
% 0.08/0.09 % 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.10/0.28 % Computer : n032.cluster.edu
% 0.10/0.28 % Model : x86_64 x86_64
% 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.28 % Memory : 8042.1875MB
% 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.28 % CPULimit : 300
% 0.10/0.28 % WCLimit : 300
% 0.10/0.28 % DateTime : Wed Apr 9 02:32:15 EDT 2025
% 0.10/0.28 % CPUTime :
% 10.78/3.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.78/3.63
% 10.78/3.63 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.78/3.64 %$ u0 > mod:(Int*Int)>Int > #nlpp > small > fast > f0
% 10.78/3.64
% 10.78/3.64 %Foreground sorts:
% 10.78/3.64
% 10.78/3.64
% 10.78/3.64 %Background operators:
% 10.78/3.64 tff('#skE_7', type, '#skE_7': $int).
% 10.78/3.64 tff('#skE_21', type, '#skE_21': $int).
% 10.78/3.64 tff('#skE_11', type, '#skE_11': $int).
% 10.78/3.64 tff('#skE_25', type, '#skE_25': $int).
% 10.78/3.64 tff('#skE_23', type, '#skE_23': $int).
% 10.78/3.64 tff('#skE_12', type, '#skE_12': $int).
% 10.78/3.64 tff(g0, type, g0: $int).
% 10.78/3.64 tff('#skE_2', type, '#skE_2': $int).
% 10.78/3.64 tff('#skE_1', type, '#skE_1': $int).
% 10.78/3.64 tff(v0, type, v0: $int).
% 10.78/3.64 tff('#skE_20', type, '#skE_20': $int).
% 10.78/3.64 tff('#skE_6', type, '#skE_6': $int).
% 10.78/3.64 tff('#skE_13', type, '#skE_13': $int).
% 10.78/3.64 tff('#skE_26', type, '#skE_26': $int).
% 10.78/3.64 tff('#skE_10', type, '#skE_10': $int).
% 10.78/3.64 tff('#skE_24', type, '#skE_24': $int).
% 10.78/3.64 tff('#skE_5', type, '#skE_5': $int).
% 10.78/3.64 tff('#skE_15', type, '#skE_15': $int).
% 10.78/3.64 tff('#skE_8', type, '#skE_8': $int).
% 10.78/3.64 tff('#skE_4', type, '#skE_4': $int).
% 10.78/3.64 tff('#skE_22', type, '#skE_22': $int).
% 10.78/3.64 tff('#skE_16', type, '#skE_16': $int).
% 10.78/3.64 tff('#skE_17', type, '#skE_17': $int).
% 10.78/3.64 tff('#skE_3', type, '#skE_3': $int).
% 10.78/3.64 tff('#skF_1', type, '#skF_1': $int).
% 10.78/3.64 tff('#skE_9', type, '#skE_9': $int).
% 10.78/3.64 tff('#skE_18', type, '#skE_18': $int).
% 10.78/3.64 tff(h0, type, h0: $int).
% 10.78/3.64 tff('#skE_19', type, '#skE_19': $int).
% 10.78/3.64 tff('#skE_14', type, '#skE_14': $int).
% 10.78/3.64
% 10.78/3.64 %Foreground operators:
% 10.78/3.64 tff(mod:(Int*Int)>Int, type, mod:(Int*Int)>Int: ($int * $int) > $int).
% 10.78/3.64 tff(fast, type, fast: $int > $int).
% 10.78/3.64 tff(small, type, small: $int > $int).
% 10.78/3.64 tff(f0, type, f0: $int > $int).
% 10.78/3.64 tff(u0, type, u0: ($int * $int) > $int).
% 10.78/3.64
% 10.78/3.65 tff(f_63, negated_conjecture, ~~(?[Ca:$int]: ($greatereq(Ca, 0) & ~(small(Ca) = fast(Ca)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conjecture_1)).
% 10.78/3.65 tff(f_52, axiom, (![Xa:$int]: (small(Xa) = $sum(2, $sum($difference(Xa, mod($sum(1, Xa), v0)), Xa)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_6)).
% 10.78/3.65 tff(f_55, axiom, (![Xa:$int]: (fast(Xa) = $sum(2, $sum($difference(Xa, mod($sum(1, Xa), $product(2, $product(2, $sum(2, 2))))), Xa)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_7)).
% 10.78/3.65 tff(f_264, axiom, (![A:$int, B:$int]: ($uminus($product(A, B)) = $product($uminus(A), B))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', minus_mult_left)).
% 10.78/3.65 tff(f_256, axiom, (![A:$int, B:$int]: ($product(A, B) = $product(B, A))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_comm)).
% 10.78/3.65 tff(f_33, axiom, (![Xa:$int]: (f0(Xa) = $product(Xa, Xa))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_1)).
% 10.78/3.65 tff(f_253, axiom, (![M:$int, N:$int]: ($product($sum(1, M), N) = $sum(N, $product(M, N)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_def_2)).
% 10.78/3.65 tff(f_258, axiom, (![A:$int, B:$int, C:$int]: ($product(A, $sum(B, C)) = $sum($product(A, B), $product(A, C)))), file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p', mult_dist)).
% 10.78/3.65 tff(f_47, axiom, (![Xa:$int, Ya:$int]: (($lesseq(Xa, 0) => (u0(Xa, Ya) = Ya)) & (~$lesseq(Xa, 0) => (u0(Xa, Ya) = f0(u0($difference(Xa, 1), Ya)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_4)).
% 10.78/3.65 tff(f_35, axiom, (g0 = 2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_2)).
% 10.78/3.65 tff(f_37, axiom, (h0 = 2), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_3)).
% 10.78/3.65 tff(f_49, axiom, (v0 = u0(g0, h0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', formula_5)).
% 10.78/3.65 tff(c_48, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_63])).
% 10.78/3.65 tff(c_245, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_48])).
% 10.78/3.65 tff(c_244, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_48])).
% 10.78/3.65 tff(c_81, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_63])).
% 10.78/3.65 tff(c_256, plain, ('#skE_2'!='#skE_1'), inference(demodulation, [status(thm), theory('equality')], [c_245, c_244, c_81])).
% 10.78/3.65 tff(c_12, plain, (![X_4a:$int]: ($sum(2, $sum($product(2, X_4a), $uminus(mod($sum(1, X_4a), v0))))=small(X_4a))), inference(cnfTransformation, [status(thm)], [f_52])).
% 10.78/3.65 tff(c_804, plain, (![X_106a:$int]: (mod($sum(1, X_106a), v0)=$sum(2, $sum($product(2, X_106a), $uminus(small(X_106a)))))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_12])).
% 10.78/3.65 tff(c_15, plain, (![X_5a:$int]: ($sum(2, $sum($product(2, X_5a), $uminus(mod($sum(1, X_5a), 16))))=fast(X_5a))), inference(cnfTransformation, [status(thm)], [f_55])).
% 10.78/3.65 tff(c_52, plain, (![X_5a:$int]: (mod($sum(1, X_5a), 16)=$sum(2, $sum($product(2, X_5a), $uminus(fast(X_5a)))))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_15])).
% 10.78/3.65 tff(c_823, plain, (![X_106a:$int, X_5a:$int]: ($sum(2, $sum($product(2, X_106a), $uminus(small(X_106a))))=$sum(2, $sum($product(2, X_5a), $uminus(fast(X_5a)))) | v0!=16 | $sum(1, X_5a)!=$sum(1, X_106a))), inference(superposition, [status(thm), theory('equality')], [c_804, c_52])).
% 10.78/3.65 tff(c_825, plain, (![X_106a:$int]: (small(X_106a)=$sum($product(2, X_106a), $sum($product($uminus(2), X_106a), fast(X_106a))) | v0!=16)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_823])).
% 10.78/3.65 tff(c_827, plain, (![X_106a:$int]: (small(X_106a)=fast(X_106a) | v0!=16)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_825])).
% 10.78/3.65 tff(c_946, plain, (v0!=16), inference(splitLeft, [status(thm)], [c_827])).
% 10.78/3.65 tff(c_73, plain, (![A_22:$int, B_23:$int, X_54:$int]: ($uminus($product(A_22, B_23))=$product(X_54, B_23) | X_54!=$uminus(A_22))), inference(cnfTransformation, [status(thm)], [f_264])).
% 10.78/3.65 tff(c_75, plain, (![X_54:$int, B_23:$int, A_22:$int]: ($uminus($product(X_54, B_23))=$product(A_22, B_23) | X_54!=$uminus(A_22))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_73])).
% 10.78/3.65 tff(c_78, plain, (![B_12:$int, A_13:$int]: ($product(B_12, A_13)=$product(A_13, B_12))), inference(cnfTransformation, [status(thm)], [f_256])).
% 10.78/3.65 tff(c_109, plain, (![X_59a:$int]: ($product(X_59a, X_59a)=f0(X_59a))), inference(cnfTransformation, [status(thm)], [f_33])).
% 10.78/3.65 tff(c_80, plain, (![X_56:$int, N_9:$int, M_8:$int]: ($product(X_56, N_9)=$sum(N_9, $product(M_8, N_9)) | X_56!=$sum(1, M_8))), inference(cnfTransformation, [status(thm)], [f_253])).
% 10.78/3.65 tff(c_1117, plain, (![X_120a:$int]: ($product($sum(1, X_120a), X_120a)=$sum(X_120a, f0(X_120a)))), inference(superposition, [status(thm), theory('equality')], [c_109, c_80])).
% 10.78/3.65 tff(c_1296, plain, (![X_120a:$int]: ($product(X_120a, $sum(1, X_120a))=$sum(X_120a, f0(X_120a)))), inference(superposition, [status(thm), theory('equality')], [c_78, c_1117])).
% 10.78/3.65 tff(c_28, plain, (![A_14:$int, C_16:$int, B_15:$int]: ($product(A_14, $sum(C_16, B_15))=$sum($product(A_14, B_15), $product(A_14, C_16)))), inference(cnfTransformation, [status(thm)], [f_258])).
% 10.78/3.65 tff(c_77, plain, (![A_17:$int, X_55:$int, B_18:$int, C_19:$int]: ($product(A_17, X_55)=$sum($product(A_17, B_18), $product(A_17, C_19)) | X_55!=$sum(B_18, C_19))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_28])).
% 10.78/3.65 tff(c_121, plain, (![X_59a:$int, B_18:$int, C_19:$int]: ($sum($product(X_59a, B_18), $product(X_59a, C_19))=f0(X_59a) | X_59a!=$sum(B_18, C_19))), inference(superposition, [status(thm), theory('equality')], [c_109, c_77])).
% 10.78/3.65 tff(c_4971, plain, (![X_505a:$int, B_506:$int, C_507:$int]: ($product(X_505a, B_506)=$sum($uminus($product(X_505a, C_507)), f0(X_505a)) | X_505a!=$sum(C_507, B_506))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_121])).
% 10.78/3.65 tff(c_5488, plain, (![X_120a:$int, B_506:$int]: ($product(X_120a, B_506)=$sum($uminus($sum(X_120a, f0(X_120a))), f0(X_120a)) | $sum($sum(1, X_120a), B_506)!=X_120a)), inference(superposition, [status(thm), theory('equality')], [c_1296, c_4971])).
% 10.78/3.65 tff(c_5616, plain, (![X_584a:$int]: ($product(X_584a, $uminus(1))=$uminus(X_584a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5488])).
% 10.78/3.65 tff(c_6220, plain, (![X_627a:$int]: ($product($uminus(1), X_627a)=$uminus(X_627a))), inference(superposition, [status(thm), theory('equality')], [c_78, c_5616])).
% 10.78/3.65 tff(c_6580, plain, (![X_627a:$int]: ($uminus($product($uminus($uminus(1)), X_627a))=$uminus(X_627a))), inference(superposition, [status(thm), theory('equality')], [c_75, c_6220])).
% 10.78/3.65 tff(c_6810, plain, (![X_648a:$int]: ($product(1, X_648a)=X_648a)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_6580])).
% 10.78/3.65 tff(c_7056, plain, (![X_648a:$int]: ($product($sum(1, 1), X_648a)=$sum(X_648a, X_648a))), inference(superposition, [status(thm), theory('equality')], [c_6810, c_80])).
% 10.78/3.65 tff(c_13821, plain, (![X_1285a:$int]: ($product(2, X_1285a)=$product(2, X_1285a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_7056])).
% 10.78/3.65 tff(c_14146, plain, (![X_1285a:$int]: ($product($sum(1, 2), X_1285a)=$sum(X_1285a, $product(2, X_1285a)))), inference(superposition, [status(thm), theory('equality')], [c_13821, c_80])).
% 10.78/3.65 tff(c_17063, plain, (![X_1476a:$int]: ($product(3, X_1476a)=$product(3, X_1476a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_14146])).
% 10.78/3.65 tff(c_115, plain, (![X_59a:$int, M_8:$int]: ($sum(X_59a, $product(M_8, X_59a))=f0(X_59a) | X_59a!=$sum(1, M_8))), inference(superposition, [status(thm), theory('equality')], [c_109, c_80])).
% 10.78/3.65 tff(c_172, plain, (![M_8:$int, X_59a:$int]: ($product(M_8, X_59a)=$sum($uminus(X_59a), f0(X_59a)) | X_59a!=$sum(1, M_8))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_115])).
% 10.78/3.65 tff(c_17351, plain, ($sum($uminus($sum(1, 3)), f0($sum(1, 3)))=$product(3, $sum(1, 3))), inference(superposition, [status(thm), theory('equality')], [c_17063, c_172])).
% 10.78/3.65 tff(c_17353, plain, (f0(4)=16), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_17351])).
% 10.78/3.65 tff(c_133, plain, (![X_59a:$int]: ($uminus($product($uminus(X_59a), X_59a))=f0(X_59a))), inference(superposition, [status(thm), theory('equality')], [c_109, c_75])).
% 10.78/3.65 tff(c_186, plain, (![X_59a:$int]: ($uminus($product(X_59a, $uminus(X_59a)))=f0(X_59a))), inference(demodulation, [status(thm), theory('equality')], [c_78, c_133])).
% 10.78/3.65 tff(c_2066, plain, (![X_191a:$int]: ($product(X_191a, $uminus(X_191a))=$uminus(f0(X_191a)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_186])).
% 10.78/3.65 tff(c_2311, plain, (![X_219a:$int]: ($product($uminus(X_219a), X_219a)=$uminus(f0(X_219a)))), inference(superposition, [status(thm), theory('equality')], [c_78, c_2066])).
% 10.78/3.65 tff(c_3886, plain, (![X_348a:$int]: ($product($sum(1, $uminus(X_348a)), X_348a)=$sum(X_348a, $uminus(f0(X_348a))))), inference(superposition, [status(thm), theory('equality')], [c_2311, c_80])).
% 10.78/3.65 tff(c_4220, plain, (![X_348a:$int]: ($product(X_348a, $sum(1, $uminus(X_348a)))=$sum(X_348a, $uminus(f0(X_348a))))), inference(superposition, [status(thm), theory('equality')], [c_78, c_3886])).
% 10.78/3.65 tff(c_5724, plain, (![X_348a:$int]: ($sum(X_348a, $uminus(f0(X_348a)))=$uminus(X_348a) | $sum(1, $uminus(X_348a))!=$uminus(1))), inference(superposition, [status(thm), theory('equality')], [c_4220, c_5616])).
% 10.78/3.65 tff(c_5900, plain, (f0(2)=$product(2, 2)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5724])).
% 10.78/3.65 tff(c_5902, plain, (f0(2)=4), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5900])).
% 10.78/3.65 tff(c_7, plain, (![X_2a:$int, Y_3a:$int]: (f0(u0($sum($uminus(1), X_2a), Y_3a))=u0(X_2a, Y_3a) | $lesseq(X_2a, 0))), inference(cnfTransformation, [status(thm)], [f_47])).
% 10.78/3.65 tff(c_64, plain, (![X_2a:$int, Y_3a:$int]: (f0(u0($sum($uminus(1), X_2a), Y_3a))=u0(X_2a, Y_3a) | ~$less(0, X_2a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_7])).
% 10.78/3.65 tff(c_301, plain, (![X_76a:$int, Y_77a:$int]: (f0(u0($sum($uminus(1), X_76a), Y_77a))=u0(X_76a, Y_77a) | ~$less(0, X_76a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_7])).
% 10.78/3.65 tff(c_67, plain, (g0=2), inference(cnfTransformation, [status(thm)], [f_35])).
% 10.78/3.65 tff(c_66, plain, (h0=2), inference(cnfTransformation, [status(thm)], [f_37])).
% 10.78/3.65 tff(c_60, plain, (u0(g0, h0)=v0), inference(cnfTransformation, [status(thm)], [f_49])).
% 10.78/3.65 tff(c_95, plain, (u0(g0, 2)=v0), inference(demodulation, [status(thm), theory('equality')], [c_66, c_60])).
% 10.78/3.65 tff(c_99, plain, (u0(2, 2)=v0), inference(demodulation, [status(thm), theory('equality')], [c_67, c_95])).
% 10.78/3.65 tff(c_353, plain, (f0(u0($sum($uminus(1), 2), 2))=v0 | ~$less(0, 2)), inference(superposition, [status(thm), theory('equality')], [c_301, c_99])).
% 10.78/3.65 tff(c_355, plain, (f0(u0(1, 2))=v0), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_353])).
% 10.78/3.65 tff(c_386, plain, (u0(1, 2)='#skE_3'), inference(define, [status(thm), theory('equality')], [c_355])).
% 10.78/3.65 tff(c_423, plain, (f0(u0($sum($uminus(1), 1), 2))='#skE_3' | ~$less(0, 1)), inference(superposition, [status(thm), theory('equality')], [c_64, c_386])).
% 10.78/3.65 tff(c_425, plain, (f0(u0(0, 2))='#skE_3'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_423])).
% 10.78/3.65 tff(c_843, plain, (u0(0, 2)='#skE_4'), inference(define, [status(thm), theory('equality')], [c_425])).
% 10.78/3.65 tff(c_5, plain, (![X_2a:$int, Y_3a:$int]: (u0(X_2a, Y_3a)=Y_3a | ~$lesseq(X_2a, 0))), inference(cnfTransformation, [status(thm)], [f_47])).
% 10.78/3.65 tff(c_65, plain, (![X_2a:$int, Y_3a:$int]: (u0(X_2a, Y_3a)=Y_3a | $less(0, X_2a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_5])).
% 10.78/3.65 tff(c_857, plain, ('#skE_4'=2 | $less(0, 0)), inference(superposition, [status(thm), theory('equality')], [c_843, c_65])).
% 10.78/3.65 tff(c_877, plain, ('#skE_4'=2), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_857])).
% 10.78/3.65 tff(c_887, plain, (u0(0, 2)=2), inference(demodulation, [status(thm), theory('equality')], [c_877, c_843])).
% 10.78/3.65 tff(c_410, plain, (f0(u0($sum($uminus(1), 1), 2))='#skE_3' | ~$less(0, 1)), inference(superposition, [status(thm), theory('equality')], [c_386, c_64])).
% 10.78/3.65 tff(c_412, plain, (f0(u0(0, 2))='#skE_3'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_410])).
% 10.78/3.65 tff(c_925, plain, (f0(2)='#skE_3'), inference(demodulation, [status(thm), theory('equality')], [c_887, c_412])).
% 10.78/3.65 tff(c_6587, plain, ('#skE_3'=4), inference(demodulation, [status(thm), theory('equality')], [c_5902, c_925])).
% 10.78/3.65 tff(c_373, plain, (f0(u0($sum($uminus(1), 2), 2))=v0 | ~$less(0, 2)), inference(superposition, [status(thm), theory('equality')], [c_99, c_301])).
% 10.78/3.65 tff(c_375, plain, (f0(u0(1, 2))=v0), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_373])).
% 10.78/3.65 tff(c_432, plain, (f0('#skE_3')=v0), inference(demodulation, [status(thm), theory('equality')], [c_386, c_375])).
% 10.78/3.65 tff(c_6665, plain, (f0(4)=v0), inference(demodulation, [status(thm), theory('equality')], [c_6587, c_432])).
% 10.78/3.65 tff(c_17838, plain, (v0=16), inference(demodulation, [status(thm), theory('equality')], [c_17353, c_6665])).
% 10.78/3.65 tff(c_17840, plain, $false, inference(negUnitSimplification, [status(thm)], [c_946, c_17838])).
% 10.78/3.65 tff(c_17864, plain, (![X_1519a:$int]: (small(X_1519a)=fast(X_1519a))), inference(splitRight, [status(thm)], [c_827])).
% 10.78/3.65 tff(c_252, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_48])).
% 10.78/3.65 tff(c_17889, plain, (fast('#skF_1')='#skE_1'), inference(superposition, [status(thm), theory('equality')], [c_17864, c_252])).
% 10.78/3.65 tff(c_255, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_48])).
% 10.78/3.65 tff(c_17895, plain, ('#skE_2'='#skE_1' | '#skF_1'!='#skF_1'), inference(superposition, [status(thm), theory('equality')], [c_17889, c_255])).
% 10.78/3.65 tff(c_17907, plain, $false, inference(negUnitSimplification, [status(thm)], [c_256, c_17895])).
% 10.78/3.65 tff(c_17910, plain, $false, inference(backgroundSimplification, [status(thm), theory('LIA')], [c_17907])).
% 10.78/3.65 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------