%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC442_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 : n004.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:28 PM UTC 2025
% Result : Theorem 11.75s 3.87s
% Output : CNFRefutation 12.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWC442_1 : TPTP v9.0.0. Released v9.0.0.
% 0.10/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.14/0.34 % Computer : n004.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 : Wed Apr 9 02:30:37 EDT 2025
% 0.14/0.34 % CPUTime :
% 11.75/3.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.75/3.88
% 11.75/3.88 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.75/3.89 %$ u0 > div:(Int*Int)>Int > #nlpp > small > fast > f0
% 11.75/3.89
% 11.75/3.89 %Foreground sorts:
% 11.75/3.89
% 11.75/3.89
% 11.75/3.89 %Background operators:
% 11.75/3.89 tff('#skE_7', type, '#skE_7': $int).
% 11.75/3.89 tff('#skE_21', type, '#skE_21': $int).
% 11.75/3.89 tff('#skE_11', type, '#skE_11': $int).
% 11.75/3.89 tff('#skE_25', type, '#skE_25': $int).
% 11.75/3.89 tff('#skE_23', type, '#skE_23': $int).
% 11.75/3.89 tff('#skE_12', type, '#skE_12': $int).
% 11.75/3.89 tff(g0, type, g0: $int).
% 11.75/3.89 tff('#skE_2', type, '#skE_2': $int).
% 11.75/3.89 tff('#skE_1', type, '#skE_1': $int).
% 11.75/3.89 tff(v0, type, v0: $int).
% 11.75/3.89 tff('#skE_20', type, '#skE_20': $int).
% 11.75/3.89 tff('#skE_6', type, '#skE_6': $int).
% 11.75/3.89 tff('#skE_13', type, '#skE_13': $int).
% 11.75/3.89 tff('#skE_26', type, '#skE_26': $int).
% 11.75/3.89 tff('#skE_10', type, '#skE_10': $int).
% 11.75/3.89 tff('#skE_24', type, '#skE_24': $int).
% 11.75/3.89 tff('#skE_5', type, '#skE_5': $int).
% 11.75/3.89 tff('#skE_15', type, '#skE_15': $int).
% 11.75/3.89 tff('#skE_8', type, '#skE_8': $int).
% 11.75/3.89 tff('#skE_4', type, '#skE_4': $int).
% 11.75/3.89 tff('#skE_22', type, '#skE_22': $int).
% 11.75/3.89 tff('#skE_16', type, '#skE_16': $int).
% 11.75/3.89 tff('#skE_17', type, '#skE_17': $int).
% 11.75/3.89 tff('#skE_3', type, '#skE_3': $int).
% 11.75/3.89 tff('#skF_1', type, '#skF_1': $int).
% 11.75/3.89 tff('#skE_9', type, '#skE_9': $int).
% 11.75/3.89 tff('#skE_18', type, '#skE_18': $int).
% 11.75/3.89 tff(h0, type, h0: $int).
% 11.75/3.89 tff('#skE_19', type, '#skE_19': $int).
% 11.75/3.89 tff('#skE_14', type, '#skE_14': $int).
% 11.75/3.89
% 11.75/3.89 %Foreground operators:
% 11.75/3.89 tff(fast, type, fast: $int > $int).
% 11.75/3.89 tff(small, type, small: $int > $int).
% 11.75/3.89 tff(f0, type, f0: $int > $int).
% 11.75/3.89 tff(u0, type, u0: ($int * $int) > $int).
% 11.75/3.89 tff(div:(Int*Int)>Int, type, div:(Int*Int)>Int: ($int * $int) > $int).
% 11.75/3.89
% 12.11/3.91 tff(f_63, negated_conjecture, ~~(?[Ca:$int]: ($greatereq(Ca, 0) & ~(small(Ca) = fast(Ca)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture_1)).
% 12.11/3.91 tff(f_52, axiom, (![Xa:$int]: (small(Xa) = div($difference($product(2, v0), 2), $sum(1, Xa)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_6)).
% 12.11/3.91 tff(f_55, axiom, (![Xa:$int]: (fast(Xa) = div($difference($product(2, $product(2, $product(2, $sum(2, 2)))), 2), $sum(1, Xa)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_7)).
% 12.11/3.91 tff(f_33, axiom, (![Xa:$int]: (f0(Xa) = $product(Xa, Xa))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_1)).
% 12.11/3.91 tff(f_253, axiom, (![M:$int, N:$int]: ($product($sum(1, M), N) = $sum(N, $product(M, N)))), file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p', mult_def_2)).
% 12.11/3.91 tff(f_256, axiom, (![A:$int, B:$int]: ($product(A, B) = $product(B, A))), file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p', mult_comm)).
% 12.11/3.91 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/sandbox/solver/bin/lemmas/mult_lemmas.p', mult_dist)).
% 12.11/3.91 tff(f_264, axiom, (![A:$int, B:$int]: ($uminus($product(A, B)) = $product($uminus(A), B))), file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p', minus_mult_left)).
% 12.11/3.91 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/sandbox/benchmark/theBenchmark.p', formula_4)).
% 12.11/3.91 tff(f_35, axiom, (g0 = 2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_2)).
% 12.11/3.91 tff(f_37, axiom, (h0 = 2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_3)).
% 12.11/3.91 tff(f_49, axiom, (v0 = u0(g0, h0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', formula_5)).
% 12.11/3.91 tff(c_46, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_63])).
% 12.11/3.91 tff(c_243, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_46])).
% 12.11/3.91 tff(c_242, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_46])).
% 12.11/3.91 tff(c_79, plain, (small('#skF_1')!=fast('#skF_1')), inference(cnfTransformation, [status(thm)], [f_63])).
% 12.11/3.91 tff(c_254, plain, ('#skE_2'!='#skE_1'), inference(demodulation, [status(thm), theory('equality')], [c_243, c_242, c_79])).
% 12.11/3.91 tff(c_250, plain, (small('#skF_1')='#skE_1'), inference(define, [status(thm), theory('equality')], [c_46])).
% 12.11/3.91 tff(c_489, plain, (![X_98a:$int]: (div($sum($uminus(2), $product(2, v0)), $sum(1, X_98a))=small(X_98a))), inference(cnfTransformation, [status(thm)], [f_52])).
% 12.11/3.91 tff(c_50, plain, (![X_5a:$int]: (div(30, $sum(1, X_5a))=fast(X_5a))), inference(cnfTransformation, [status(thm)], [f_55])).
% 12.11/3.91 tff(c_508, plain, (![X_98a:$int, X_5a:$int]: (small(X_98a)=fast(X_5a) | $sum(1, X_98a)!=$sum(1, X_5a) | $sum($uminus(2), $product(2, v0))!=30)), inference(superposition, [status(thm), theory('equality')], [c_489, c_50])).
% 12.11/3.91 tff(c_511, plain, (![X_5a:$int]: (small(X_5a)=fast(X_5a) | v0!=16)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_508])).
% 12.11/3.91 tff(c_534, plain, (v0!=16), inference(splitLeft, [status(thm)], [c_511])).
% 12.11/3.91 tff(c_107, plain, (![X_55a:$int]: ($product(X_55a, X_55a)=f0(X_55a))), inference(cnfTransformation, [status(thm)], [f_33])).
% 12.11/3.91 tff(c_78, plain, (![X_52:$int, N_9:$int, M_8:$int]: ($product(X_52, N_9)=$sum(N_9, $product(M_8, N_9)) | X_52!=$sum(1, M_8))), inference(cnfTransformation, [status(thm)], [f_253])).
% 12.11/3.91 tff(c_1826, plain, (![X_169a:$int]: ($product($sum(1, X_169a), X_169a)=$sum(X_169a, f0(X_169a)))), inference(superposition, [status(thm), theory('equality')], [c_107, c_78])).
% 12.11/3.91 tff(c_76, plain, (![B_12:$int, A_13:$int]: ($product(B_12, A_13)=$product(A_13, B_12))), inference(cnfTransformation, [status(thm)], [f_256])).
% 12.11/3.91 tff(c_1963, plain, (![X_169a:$int]: ($product(X_169a, $sum(1, X_169a))=$sum(X_169a, f0(X_169a)))), inference(superposition, [status(thm), theory('equality')], [c_1826, c_76])).
% 12.11/3.91 tff(c_26, 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])).
% 12.11/3.91 tff(c_75, plain, (![A_17:$int, X_51:$int, B_18:$int, C_19:$int]: ($product(A_17, X_51)=$sum($product(A_17, B_18), $product(A_17, C_19)) | X_51!=$sum(B_18, C_19))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_26])).
% 12.11/3.91 tff(c_119, plain, (![X_55a:$int, B_18:$int, C_19:$int]: ($sum($product(X_55a, B_18), $product(X_55a, C_19))=f0(X_55a) | X_55a!=$sum(B_18, C_19))), inference(superposition, [status(thm), theory('equality')], [c_107, c_75])).
% 12.11/3.91 tff(c_3073, plain, (![X_276a:$int, B_277:$int, C_278:$int]: ($product(X_276a, B_277)=$sum($uminus($product(X_276a, C_278)), f0(X_276a)) | X_276a!=$sum(C_278, B_277))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_119])).
% 12.11/3.91 tff(c_3421, plain, (![X_169a:$int, C_278:$int]: ($sum($uminus($product(X_169a, C_278)), f0(X_169a))=$sum(X_169a, f0(X_169a)) | $sum(C_278, $sum(1, X_169a))!=X_169a)), inference(superposition, [status(thm), theory('equality')], [c_1963, c_3073])).
% 12.11/3.91 tff(c_5236, plain, (![X_582a:$int]: ($product(X_582a, $uminus(1))=$uminus(X_582a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_3421])).
% 12.11/3.91 tff(c_5572, plain, (![X_605a:$int]: ($product($uminus(1), X_605a)=$uminus(X_605a))), inference(superposition, [status(thm), theory('equality')], [c_5236, c_76])).
% 12.11/3.91 tff(c_71, plain, (![A_22:$int, B_23:$int, X_50:$int]: ($uminus($product(A_22, B_23))=$product(X_50, B_23) | X_50!=$uminus(A_22))), inference(cnfTransformation, [status(thm)], [f_264])).
% 12.11/3.91 tff(c_73, plain, (![X_50:$int, B_23:$int, A_22:$int]: ($uminus($product(X_50, B_23))=$product(A_22, B_23) | X_50!=$uminus(A_22))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_71])).
% 12.11/3.91 tff(c_5843, plain, (![X_605a:$int]: ($uminus($product($uminus($uminus(1)), X_605a))=$uminus(X_605a))), inference(superposition, [status(thm), theory('equality')], [c_5572, c_73])).
% 12.11/3.91 tff(c_6369, plain, (![X_645a:$int]: ($product(1, X_645a)=X_645a)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5843])).
% 12.11/3.91 tff(c_6604, plain, (![X_645a:$int]: ($product($sum(1, 1), X_645a)=$sum(X_645a, X_645a))), inference(superposition, [status(thm), theory('equality')], [c_6369, c_78])).
% 12.11/3.91 tff(c_14139, plain, (![X_1322a:$int]: ($product(2, X_1322a)=$product(2, X_1322a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_6604])).
% 12.11/3.91 tff(c_14464, plain, (![X_1322a:$int]: ($product($sum(1, 2), X_1322a)=$sum(X_1322a, $product(2, X_1322a)))), inference(superposition, [status(thm), theory('equality')], [c_14139, c_78])).
% 12.11/3.91 tff(c_17634, plain, (![X_1532a:$int]: ($product(3, X_1532a)=$product(3, X_1532a))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_14464])).
% 12.11/3.91 tff(c_151, plain, (![X_55a:$int, M_8:$int]: ($sum(X_55a, $product(M_8, X_55a))=f0(X_55a) | X_55a!=$sum(1, M_8))), inference(superposition, [status(thm), theory('equality')], [c_78, c_107])).
% 12.11/3.91 tff(c_196, plain, (![M_8:$int, X_55a:$int]: ($product(M_8, X_55a)=$sum($uminus(X_55a), f0(X_55a)) | X_55a!=$sum(1, M_8))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_151])).
% 12.11/3.91 tff(c_17929, plain, ($sum($uminus($sum(1, 3)), f0($sum(1, 3)))=$product(3, $sum(1, 3))), inference(superposition, [status(thm), theory('equality')], [c_17634, c_196])).
% 12.11/3.91 tff(c_17931, plain, (f0(4)=16), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_17929])).
% 12.11/3.91 tff(c_157, plain, (![X_55a:$int]: ($uminus($product($uminus(X_55a), X_55a))=f0(X_55a))), inference(superposition, [status(thm), theory('equality')], [c_73, c_107])).
% 12.11/3.91 tff(c_202, plain, (![X_55a:$int]: ($uminus($product(X_55a, $uminus(X_55a)))=f0(X_55a))), inference(demodulation, [status(thm), theory('equality')], [c_76, c_157])).
% 12.11/3.91 tff(c_318, plain, (![X_74a:$int]: ($product(X_74a, $uminus(X_74a))=$uminus(f0(X_74a)))), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_202])).
% 12.11/3.91 tff(c_921, plain, (![X_124a:$int]: ($product($uminus(X_124a), X_124a)=$uminus(f0(X_124a)))), inference(superposition, [status(thm), theory('equality')], [c_318, c_76])).
% 12.11/3.91 tff(c_3900, plain, (![X_362a:$int]: ($product($sum(1, $uminus(X_362a)), X_362a)=$sum(X_362a, $uminus(f0(X_362a))))), inference(superposition, [status(thm), theory('equality')], [c_921, c_78])).
% 12.11/3.91 tff(c_4237, plain, (![X_362a:$int]: ($product(X_362a, $sum(1, $uminus(X_362a)))=$sum(X_362a, $uminus(f0(X_362a))))), inference(superposition, [status(thm), theory('equality')], [c_76, c_3900])).
% 12.11/3.91 tff(c_5337, plain, (![X_362a:$int]: ($sum(X_362a, $uminus(f0(X_362a)))=$uminus(X_362a) | $sum(1, $uminus(X_362a))!=$uminus(1))), inference(superposition, [status(thm), theory('equality')], [c_4237, c_5236])).
% 12.11/3.91 tff(c_5505, plain, (f0(2)=$product(2, 2)), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5337])).
% 12.11/3.91 tff(c_5507, plain, (f0(2)=4), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_5505])).
% 12.11/3.91 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])).
% 12.11/3.91 tff(c_62, 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])).
% 12.11/3.91 tff(c_535, plain, (![X_99a:$int, Y_100a:$int]: (f0(u0($sum($uminus(1), X_99a), Y_100a))=u0(X_99a, Y_100a) | ~$less(0, X_99a))), inference(backgroundSimplification, [status(thm), theory('LRFIA')], [c_7])).
% 12.11/3.91 tff(c_65, plain, (g0=2), inference(cnfTransformation, [status(thm)], [f_35])).
% 12.11/3.91 tff(c_64, plain, (h0=2), inference(cnfTransformation, [status(thm)], [f_37])).
% 12.11/3.91 tff(c_58, plain, (u0(g0, h0)=v0), inference(cnfTransformation, [status(thm)], [f_49])).
% 12.11/3.91 tff(c_93, plain, (u0(g0, 2)=v0), inference(demodulation, [status(thm), theory('equality')], [c_64, c_58])).
% 12.11/3.91 tff(c_97, plain, (u0(2, 2)=v0), inference(demodulation, [status(thm), theory('equality')], [c_65, c_93])).
% 12.11/3.91 tff(c_587, plain, (f0(u0($sum($uminus(1), 2), 2))=v0 | ~$less(0, 2)), inference(superposition, [status(thm), theory('equality')], [c_535, c_97])).
% 12.11/3.91 tff(c_589, plain, (f0(u0(1, 2))=v0), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_587])).
% 12.11/3.91 tff(c_620, plain, (u0(1, 2)='#skE_3'), inference(define, [status(thm), theory('equality')], [c_589])).
% 12.11/3.91 tff(c_657, plain, (f0(u0($sum($uminus(1), 1), 2))='#skE_3' | ~$less(0, 1)), inference(superposition, [status(thm), theory('equality')], [c_62, c_620])).
% 12.11/3.91 tff(c_659, plain, (f0(u0(0, 2))='#skE_3'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_657])).
% 12.11/3.91 tff(c_874, plain, (u0(0, 2)='#skE_4'), inference(define, [status(thm), theory('equality')], [c_659])).
% 12.11/3.91 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])).
% 12.11/3.91 tff(c_63, 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])).
% 12.11/3.91 tff(c_888, plain, ('#skE_4'=2 | $less(0, 0)), inference(superposition, [status(thm), theory('equality')], [c_874, c_63])).
% 12.11/3.91 tff(c_908, plain, ('#skE_4'=2), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_888])).
% 12.11/3.91 tff(c_918, plain, (u0(0, 2)=2), inference(demodulation, [status(thm), theory('equality')], [c_908, c_874])).
% 12.11/3.91 tff(c_644, plain, (f0(u0($sum($uminus(1), 1), 2))='#skE_3' | ~$less(0, 1)), inference(superposition, [status(thm), theory('equality')], [c_620, c_62])).
% 12.11/3.91 tff(c_646, plain, (f0(u0(0, 2))='#skE_3'), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_644])).
% 12.11/3.91 tff(c_1150, plain, (f0(2)='#skE_3'), inference(demodulation, [status(thm), theory('equality')], [c_918, c_646])).
% 12.11/3.91 tff(c_5927, plain, ('#skE_3'=4), inference(demodulation, [status(thm), theory('equality')], [c_5507, c_1150])).
% 12.11/3.91 tff(c_607, plain, (f0(u0($sum($uminus(1), 2), 2))=v0 | ~$less(0, 2)), inference(superposition, [status(thm), theory('equality')], [c_97, c_535])).
% 12.11/3.91 tff(c_609, plain, (f0(u0(1, 2))=v0), inference(backgroundSimplification, [status(thm), theory('LIA')], [c_607])).
% 12.11/3.91 tff(c_666, plain, (f0('#skE_3')=v0), inference(demodulation, [status(thm), theory('equality')], [c_620, c_609])).
% 12.11/3.91 tff(c_6005, plain, (f0(4)=v0), inference(demodulation, [status(thm), theory('equality')], [c_5927, c_666])).
% 12.11/3.91 tff(c_18636, plain, (v0=16), inference(demodulation, [status(thm), theory('equality')], [c_17931, c_6005])).
% 12.11/3.91 tff(c_18638, plain, $false, inference(negUnitSimplification, [status(thm)], [c_534, c_18636])).
% 12.11/3.91 tff(c_18655, plain, (![X_1572a:$int]: (small(X_1572a)=fast(X_1572a))), inference(splitRight, [status(thm)], [c_511])).
% 12.11/3.91 tff(c_18680, plain, (fast('#skF_1')='#skE_1'), inference(superposition, [status(thm), theory('equality')], [c_250, c_18655])).
% 12.11/3.91 tff(c_253, plain, (fast('#skF_1')='#skE_2'), inference(define, [status(thm), theory('equality')], [c_46])).
% 12.11/3.91 tff(c_18686, plain, ('#skE_2'='#skE_1' | '#skF_1'!='#skF_1'), inference(superposition, [status(thm), theory('equality')], [c_18680, c_253])).
% 12.11/3.91 tff(c_18698, plain, $false, inference(negUnitSimplification, [status(thm)], [c_254, c_18686])).
% 12.11/3.91 tff(c_18701, plain, $false, inference(backgroundSimplification, [status(thm), theory('LIA')], [c_18698])).
% 12.11/3.91 % SZS output end CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------