%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ARI659_1 : TPTP v9.0.0. Released v6.3.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 : n016.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 05:40:47 PM UTC 2025
% Result : Theorem 16.55s 4.98s
% Output : CNFRefutation 16.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 7
% Syntax : Number of formulae : 124 ( 79 unt; 0 typ; 0 def)
% Number of atoms : 177 ( 89 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 114 ( 61 ~; 49 |; 1 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 439 ( 77 atm; 183 fun; 129 num; 50 var)
% Number of types : 1 ( 0 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 3 usr; 7 con; 0-2 aty)
% Number of variables : 50 ( 50 !; 0 ?; 50 :)
% Comments :
%------------------------------------------------------------------------------
%$ #nlpp
%Foreground sorts:
%Background operators:
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff(a,type,
a: $int ).
%Foreground operators:
tff(f_127,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) ).
tff(f_130,axiom,
! [A: $int,B: $int] : ( $product(A,B) = $product(B,A) ),
file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p',mult_comm) ).
tff(f_33,negated_conjecture,
~ ( $greatereq(3,$product($product(a,a),a))
<=> $lesseq(a,1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
tff(f_155,axiom,
! [A: $int,B: $int] :
( ( $less(0,A)
& $less(0,B) )
=> $less(0,$product(A,B)) ),
file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p',mult_nonneg_nonneg) ).
tff(f_138,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) ).
tff(f_146,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) ).
tff(f_132,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) ).
tff(c_56,plain,
! [X_49: $int,N_4: $int,M_3: $int] :
( ( $product(X_49,N_4) = $sum(N_4,$product(M_3,N_4)) )
| ( X_49 != $sum(1,M_3) ) ),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_54,plain,
! [B_7: $int,A_8: $int] : ( $product(B_7,A_8) = $product(A_8,B_7) ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_8,plain,
( $greatereq(3,$product($product(a,a),a))
| $lesseq(a,1) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_36,plain,
( ~ $less(3,$product($product(a,a),a))
| ~ $less(1,a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_8]) ).
tff(c_68,plain,
( ~ $less(3,$product(a,$product(a,a)))
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_36]) ).
tff(c_85,plain,
$product(a,a) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_68]) ).
tff(c_1,plain,
( ~ $greatereq(3,$product($product(a,a),a))
| ~ $lesseq(a,1) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_44,plain,
( $less(3,$product($product(a,a),a))
| $less(1,a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_1]) ).
tff(c_248,plain,
( $less(3,$product('#skE_1',a))
| $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_85,c_54,c_44]) ).
tff(c_30390,plain,
$product('#skE_1',a) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_248]) ).
tff(c_30527,plain,
! [M_3: $int] :
( ( $sum(a,$product(M_3,a)) = '#skE_2' )
| ( $sum(1,M_3) != '#skE_1' ) ),
inference(superposition,[status(thm),theory(equality)],[c_56,c_30390]) ).
tff(c_30529,plain,
$product($sum($uminus(1),'#skE_1'),a) = $sum($uminus(a),'#skE_2'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_30527]) ).
tff(c_32700,plain,
$product($sum($uminus(1),'#skE_1'),a) = $sum('#skE_2',$uminus(a)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_30529]) ).
tff(c_45,plain,
! [A_27: $int,B_28: $int] :
( $less(0,$product(A_27,B_28))
| ~ $less(0,A_27)
| ~ $less(0,B_28) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_32928,plain,
( $less(0,$sum('#skE_2',$uminus(a)))
| ~ $less(0,$sum($uminus(1),'#skE_1'))
| ~ $less(0,a) ),
inference(superposition,[status(thm),theory(equality)],[c_32700,c_45]) ).
tff(c_32930,plain,
( $less(a,'#skE_2')
| ~ $less(1,'#skE_1')
| ~ $less(0,a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_32928]) ).
tff(c_43219,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_32930]) ).
tff(c_49,plain,
! [A_17: $int,B_18: $int,X_47: $int] :
( ( $uminus($product(A_17,B_18)) = $product(X_47,B_18) )
| ( X_47 != $uminus(A_17) ) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_51,plain,
! [X_47: $int,B_18: $int,A_17: $int] :
( ( $uminus($product(X_47,B_18)) = $product(A_17,B_18) )
| ( X_47 != $uminus(A_17) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_49]) ).
tff(c_86,plain,
$product(a,a) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_68]) ).
tff(c_150,plain,
$uminus($product($uminus(a),a)) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_51,c_86]) ).
tff(c_222,plain,
$uminus($product(a,$uminus(a))) = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_54,c_150]) ).
tff(c_1025,plain,
$product(a,$uminus(a)) = $uminus('#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_222]) ).
tff(c_1223,plain,
$uminus($product($uminus(a),$uminus(a))) = $uminus('#skE_1'),
inference(superposition,[status(thm),theory(equality)],[c_51,c_1025]) ).
tff(c_26192,plain,
$product($uminus(a),$uminus(a)) = '#skE_1',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1223]) ).
tff(c_26949,plain,
( $less(0,'#skE_1')
| ~ $less(0,$uminus(a)) ),
inference(superposition,[status(thm),theory(equality)],[c_26192,c_45]) ).
tff(c_26951,plain,
( $less(0,'#skE_1')
| ~ $less(a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_26949]) ).
tff(c_28128,plain,
~ $less(a,0),
inference(splitLeft,[status(thm)],[c_26951]) ).
tff(c_203,plain,
( $less(0,'#skE_1')
| ~ $less(0,a) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_45]) ).
tff(c_263,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_203]) ).
tff(c_46,plain,
! [B_24: $int] : ( $product(0,B_24) = 0 ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_229,plain,
( ( '#skE_1' = 0 )
| ( a != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_86]) ).
tff(c_243,plain,
a != 0,
inference(splitLeft,[status(thm)],[c_229]) ).
tff(c_28131,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_28128,c_263,c_243]) ).
tff(c_28135,plain,
$less(a,0),
inference(splitRight,[status(thm)],[c_26951]) ).
tff(c_28134,plain,
$less(0,'#skE_1'),
inference(splitRight,[status(thm)],[c_26951]) ).
tff(c_266,plain,
$product('#skE_1',a) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_248]) ).
tff(c_438,plain,
$product(a,'#skE_1') = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_266,c_54]) ).
tff(c_514,plain,
$uminus($product($uminus(a),'#skE_1')) = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_51,c_438]) ).
tff(c_600,plain,
$uminus($product('#skE_1',$uminus(a))) = '#skE_2',
inference(demodulation,[status(thm),theory(equality)],[c_54,c_514]) ).
tff(c_27229,plain,
$product('#skE_1',$uminus(a)) = $uminus('#skE_2'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_600]) ).
tff(c_27919,plain,
( $less(0,$uminus('#skE_2'))
| ~ $less(0,'#skE_1')
| ~ $less(0,$uminus(a)) ),
inference(superposition,[status(thm),theory(equality)],[c_27229,c_45]) ).
tff(c_27921,plain,
( $less('#skE_2',0)
| ~ $less(0,'#skE_1')
| ~ $less(a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_27919]) ).
tff(c_30209,plain,
$less('#skE_2',0),
inference(demodulation,[status(thm),theory(equality)],[c_28135,c_28134,c_27921]) ).
tff(c_70,plain,
$product(a,a) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_68]) ).
tff(c_69,plain,
( ~ $less(3,$product(a,$product(a,a)))
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_36]) ).
tff(c_73,plain,
( ~ $less(3,$product(a,'#skE_1'))
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_70,c_69]) ).
tff(c_83,plain,
( ~ $less(3,$product('#skE_1',a))
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_73]) ).
tff(c_234,plain,
$product('#skE_1',a) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_83]) ).
tff(c_233,plain,
( ~ $less(3,$product('#skE_1',a))
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_73]) ).
tff(c_241,plain,
( ~ $less(3,'#skE_2')
| ~ $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_233]) ).
tff(c_259,plain,
~ $less(1,a),
inference(splitLeft,[status(thm)],[c_241]) ).
tff(c_250,plain,
$product('#skE_1',a) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_248]) ).
tff(c_249,plain,
( $less(3,$product('#skE_1',a))
| $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_54,c_85,c_54,c_44]) ).
tff(c_257,plain,
( $less(3,'#skE_2')
| $less(1,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_250,c_249]) ).
tff(c_261,plain,
$less(3,'#skE_2'),
inference(negUnitSimplification,[status(thm)],[c_259,c_257]) ).
tff(c_30210,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_30209,c_261]) ).
tff(c_30214,plain,
$less(0,a),
inference(splitRight,[status(thm)],[c_203]) ).
tff(c_47,plain,
! [C_23: $int] : ( $product(C_23,1) = C_23 ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_199,plain,
( ( a = '#skE_1' )
| ( a != 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_47]) ).
tff(c_231,plain,
a != 1,
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_30215,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_30214,c_259,c_231]) ).
tff(c_30219,plain,
$less(1,a),
inference(splitRight,[status(thm)],[c_241]) ).
tff(c_43220,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_43219,c_30219]) ).
tff(c_43223,plain,
( ~ $less(1,'#skE_1')
| $less(a,'#skE_2') ),
inference(splitRight,[status(thm)],[c_32930]) ).
tff(c_43225,plain,
~ $less(1,'#skE_1'),
inference(splitLeft,[status(thm)],[c_43223]) ).
tff(c_30565,plain,
$product(a,'#skE_1') = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_54,c_30390]) ).
tff(c_30735,plain,
( ( a = '#skE_2' )
| ( '#skE_1' != 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_30565]) ).
tff(c_30740,plain,
'#skE_1' != 1,
inference(splitLeft,[status(thm)],[c_30735]) ).
tff(c_30227,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_203]) ).
tff(c_30386,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_30227,c_30219]) ).
tff(c_30389,plain,
$less(0,'#skE_1'),
inference(splitRight,[status(thm)],[c_203]) ).
tff(c_43226,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_43225,c_30740,c_30389]) ).
tff(c_43229,plain,
$less(a,'#skE_2'),
inference(splitRight,[status(thm)],[c_43223]) ).
tff(c_265,plain,
$product('#skE_1',a) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_248]) ).
tff(c_17,plain,
! [A_9: $int,C_11: $int,B_10: $int] : ( $product(A_9,$sum(C_11,B_10)) = $sum($product(A_9,B_10),$product(A_9,C_11)) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_53,plain,
! [A_12: $int,X_48: $int,B_13: $int,C_14: $int] :
( ( $product(A_12,X_48) = $sum($product(A_12,B_13),$product(A_12,C_14)) )
| ( X_48 != $sum(B_13,C_14) ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_17]) ).
tff(c_178,plain,
! [X_48: $int,C_14: $int] :
( ( $product(a,X_48) = $sum('#skE_1',$product(a,C_14)) )
| ( X_48 != $sum(a,C_14) ) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_53]) ).
tff(c_6535,plain,
! [C_14: $int] : ( $product(a,$sum(C_14,a)) = $sum('#skE_1',$product(a,C_14)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_178]) ).
tff(c_62,plain,
! [A_12: $int,B_13: $int,C_14: $int] : ( $product(A_12,$sum(B_13,C_14)) = $sum($product(A_12,B_13),$product(A_12,C_14)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_17]) ).
tff(c_30499,plain,
! [B_13: $int,X_48: $int] :
( ( $sum($product('#skE_1',B_13),'#skE_2') = $product('#skE_1',X_48) )
| ( X_48 != $sum(B_13,a) ) ),
inference(superposition,[status(thm),theory(equality)],[c_30390,c_53]) ).
tff(c_36983,plain,
! [X_4048: $int,B_4051: $int] :
( ( $sum($uminus('#skE_2'),$product('#skE_1',X_4048)) = $product('#skE_1',B_4051) )
| ( X_4048 != $sum(a,B_4051) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_30499]) ).
tff(c_37327,plain,
$sum($uminus('#skE_2'),$product('#skE_1',$sum(a,1))) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_47,c_36983]) ).
tff(c_37753,plain,
$sum($uminus('#skE_2'),$sum('#skE_2',$product(1,'#skE_1'))) = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_265,c_54,c_62,c_37327]) ).
tff(c_38601,plain,
$product(1,'#skE_1') = '#skE_1',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_37753]) ).
tff(c_38893,plain,
$product($sum(1,1),'#skE_1') = $sum('#skE_1','#skE_1'),
inference(superposition,[status(thm),theory(equality)],[c_38601,c_56]) ).
tff(c_40833,plain,
$product(2,'#skE_1') = $product(2,'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_38893]) ).
tff(c_181,plain,
! [C_14: $int,X_48: $int] :
( ( $sum('#skE_1',$product(a,C_14)) = $product(a,X_48) )
| ( X_48 != $sum(C_14,a) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_178]) ).
tff(c_40863,plain,
( ( $product(a,$sum('#skE_1',a)) = $sum('#skE_1',$product(2,'#skE_1')) )
| ( a != 2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_40833,c_181]) ).
tff(c_41117,plain,
( ( $sum('#skE_1','#skE_2') = $sum('#skE_1',$product(2,'#skE_1')) )
| ( a != 2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_265,c_54,c_6535,c_40863]) ).
tff(c_41119,plain,
( ( '#skE_2' = $product(2,'#skE_1') )
| ( a != 2 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_41117]) ).
tff(c_41318,plain,
a != 2,
inference(splitLeft,[status(thm)],[c_41119]) ).
tff(c_30218,plain,
~ $less(3,'#skE_2'),
inference(splitRight,[status(thm)],[c_241]) ).
tff(c_43231,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_43229,c_41318,c_30219,c_30218]) ).
tff(c_43234,plain,
'#skE_2' = $product(2,'#skE_1'),
inference(splitRight,[status(thm)],[c_41119]) ).
tff(c_43951,plain,
~ $less(3,$product(2,'#skE_1')),
inference(demodulation,[status(thm),theory(equality)],[c_43234,c_30218]) ).
tff(c_43958,plain,
~ $less(1,'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_43951]) ).
tff(c_43959,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_43958,c_30740,c_30389]) ).
tff(c_43962,plain,
a = '#skE_2',
inference(splitRight,[status(thm)],[c_30735]) ).
tff(c_43995,plain,
'#skE_2' != 1,
inference(demodulation,[status(thm),theory(equality)],[c_43962,c_231]) ).
tff(c_43963,plain,
'#skE_1' = 1,
inference(splitRight,[status(thm)],[c_30735]) ).
tff(c_166,plain,
$product($sum(1,a),a) = $sum(a,'#skE_1'),
inference(superposition,[status(thm),theory(equality)],[c_86,c_56]) ).
tff(c_169,plain,
$product($sum(1,a),a) = $sum('#skE_1',a),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_166]) ).
tff(c_45489,plain,
$product($sum(1,'#skE_2'),'#skE_2') = $sum(1,'#skE_2'),
inference(demodulation,[status(thm),theory(equality)],[c_43963,c_43962,c_43962,c_43962,c_169]) ).
tff(c_48,plain,
! [C_21: $int,B_22: $int] :
( ( $product(C_21,B_22) != C_21 )
| ( C_21 = 0 )
| ( B_22 = 1 ) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_45688,plain,
( ( $sum(1,'#skE_2') = 0 )
| ( '#skE_2' = 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_45489,c_48]) ).
tff(c_45690,plain,
( ( '#skE_2' = $uminus(1) )
| ( '#skE_2' = 1 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_45688]) ).
tff(c_45753,plain,
'#skE_2' = $uminus(1),
inference(negUnitSimplification,[status(thm)],[c_43995,c_45690]) ).
tff(c_43993,plain,
$less(1,'#skE_2'),
inference(demodulation,[status(thm),theory(equality)],[c_43962,c_30219]) ).
tff(c_45788,plain,
$less(1,$uminus(1)),
inference(demodulation,[status(thm),theory(equality)],[c_45753,c_43993]) ).
tff(c_45807,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_45788]) ).
tff(c_45811,plain,
a = 0,
inference(splitRight,[status(thm)],[c_229]) ).
tff(c_45833,plain,
( $less(3,0)
| $less(1,0) ),
inference(demodulation,[status(thm),theory(equality)],[c_45811,c_46,c_45811,c_54,c_44]) ).
tff(c_45835,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_45833]) ).
tff(c_45839,plain,
a = 1,
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_45869,plain,
( $less(3,1)
| $less(1,1) ),
inference(demodulation,[status(thm),theory(equality)],[c_45839,c_47,c_47,c_45839,c_45839,c_45839,c_54,c_44]) ).
tff(c_45871,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_45869]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : ARI659_1 : TPTP v9.0.0. Released v6.3.0.
% 0.06/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 : n016.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 : Mon Apr 7 15:16:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 16.55/4.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.55/4.99
% 16.55/4.99 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------