%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ARI681_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 : n031.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:50 PM UTC 2025
% Result : Theorem 38.56s 15.15s
% Output : CNFRefutation 38.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 8
% Syntax : Number of formulae : 177 ( 129 unt; 0 typ; 0 def)
% Number of atoms : 249 ( 99 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 169 ( 97 ~; 69 |; 1 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 491 ( 130 atm; 163 fun; 166 num; 32 var)
% Number of types : 1 ( 0 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 8 usr; 10 con; 0-2 aty)
% Number of variables : 32 ( 32 !; 0 ?; 32 :)
% Comments :
%------------------------------------------------------------------------------
%$ #nlpp
%Foreground sorts:
%Background operators:
tff(c,type,
c: $int ).
tff(d,type,
d: $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff(b,type,
b: $int ).
tff(a,type,
a: $int ).
%Foreground operators:
tff(f_68,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_34,negated_conjecture,
~ $less(0,$product(b,d)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_003) ).
tff(f_76,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_93,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_32,axiom,
$less(0,$product(a,b)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_002) ).
tff(f_84,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_31,axiom,
$less(0,$product(c,d)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_001) ).
tff(f_30,axiom,
$less(0,$product(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj) ).
tff(c_57,plain,
! [B_7: $int,A_8: $int] : ( $product(B_7,A_8) = $product(A_8,B_7) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_35,plain,
~ $less(0,$product(b,d)),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_71,plain,
$product(b,d) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_35]) ).
tff(c_60,plain,
~ $less(0,$product(b,d)),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_78,plain,
~ $less(0,'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_71,c_60]) ).
tff(c_81,plain,
$product(b,d) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_35]) ).
tff(c_52,plain,
! [A_17: $int,B_18: $int,X_45: $int] :
( ( $uminus($product(A_17,B_18)) = $product(X_45,B_18) )
| ( X_45 != $uminus(A_17) ) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_54,plain,
! [X_45: $int,B_18: $int,A_17: $int] :
( ( $uminus($product(X_45,B_18)) = $product(A_17,B_18) )
| ( X_45 != $uminus(A_17) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_52]) ).
tff(c_1635,plain,
! [A_328: $int] :
( ( $product(A_328,d) = $uminus('#skE_1') )
| ( b != $uminus(A_328) ) ),
inference(superposition,[status(thm),theory(equality)],[c_81,c_54]) ).
tff(c_7286,plain,
! [A_885: $int] :
( ( $product(d,A_885) = $uminus('#skE_1') )
| ( b != $uminus(A_885) ) ),
inference(superposition,[status(thm),theory(equality)],[c_1635,c_57]) ).
tff(c_7638,plain,
! [A_17: $int,A_885: $int] :
( ( $product(A_17,A_885) = $uminus($uminus('#skE_1')) )
| ( d != $uminus(A_17) )
| ( b != $uminus(A_885) ) ),
inference(superposition,[status(thm),theory(equality)],[c_7286,c_54]) ).
tff(c_151863,plain,
! [A_18011: $int,A_18012: $int] :
( ( $product(A_18011,A_18012) = '#skE_1' )
| ( d != $uminus(A_18011) )
| ( b != $uminus(A_18012) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_7638]) ).
tff(c_48,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_93]) ).
tff(c_152216,plain,
! [A_18011: $int,A_18012: $int] :
( $less(0,'#skE_1')
| ~ $less(0,A_18011)
| ~ $less(0,A_18012)
| ( d != $uminus(A_18011) )
| ( b != $uminus(A_18012) ) ),
inference(superposition,[status(thm),theory(equality)],[c_151863,c_48]) ).
tff(c_152757,plain,
! [A_18011: $int,A_18012: $int] :
( ~ $less(0,A_18011)
| ~ $less(0,A_18012)
| ( d != $uminus(A_18011) )
| ( b != $uminus(A_18012) ) ),
inference(negUnitSimplification,[status(thm)],[c_78,c_152216]) ).
tff(c_152993,plain,
! [A_18012: $int] :
( ~ $less(0,A_18012)
| ( b != $uminus(A_18012) ) ),
inference(splitLeft,[status(thm)],[c_152757]) ).
tff(c_152994,plain,
$lesseq(0,b),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_152993]) ).
tff(c_152996,plain,
~ $less(b,0),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_152994]) ).
tff(c_39,plain,
$less(0,$product(a,b)),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_790,plain,
$product(a,b) = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_39]) ).
tff(c_929,plain,
$uminus($product($uminus(a),b)) = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_790,c_54]) ).
tff(c_2432,plain,
$product($uminus(a),b) = $uminus('#skE_4'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_929]) ).
tff(c_2650,plain,
( $less(0,$uminus('#skE_4'))
| ~ $less(0,$uminus(a))
| ~ $less(0,b) ),
inference(superposition,[status(thm),theory(equality)],[c_2432,c_48]) ).
tff(c_2652,plain,
( $less('#skE_4',0)
| ~ $less(a,0)
| ~ $less(0,b) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2650]) ).
tff(c_33414,plain,
~ $less(0,b),
inference(splitLeft,[status(thm)],[c_2652]) ).
tff(c_49,plain,
! [B_24: $int] : ( $product(0,B_24) = 0 ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_195,plain,
( ( '#skE_1' = 0 )
| ( b != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_81,c_49]) ).
tff(c_236,plain,
b != 0,
inference(splitLeft,[status(thm)],[c_195]) ).
tff(c_152997,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_152996,c_33414,c_236]) ).
tff(c_152999,plain,
! [A_18011: $int] :
( ~ $less(0,A_18011)
| ( d != $uminus(A_18011) ) ),
inference(splitRight,[status(thm)],[c_152757]) ).
tff(c_153000,plain,
$lesseq(0,d),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_152999]) ).
tff(c_153002,plain,
~ $less(d,0),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_153000]) ).
tff(c_418,plain,
$product(d,b) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_57,c_81]) ).
tff(c_550,plain,
( ( '#skE_1' = 0 )
| ( d != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_49]) ).
tff(c_589,plain,
d != 0,
inference(splitLeft,[status(thm)],[c_550]) ).
tff(c_127,plain,
( $less(0,'#skE_1')
| ~ $less(0,b)
| ~ $less(0,d) ),
inference(superposition,[status(thm),theory(equality)],[c_81,c_48]) ).
tff(c_199,plain,
( ~ $less(0,b)
| ~ $less(0,d) ),
inference(negUnitSimplification,[status(thm)],[c_78,c_127]) ).
tff(c_242,plain,
~ $less(0,d),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_153003,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_153002,c_589,c_242]) ).
tff(c_153007,plain,
$less(0,b),
inference(splitRight,[status(thm)],[c_2652]) ).
tff(c_494,plain,
$uminus($product($uminus(d),b)) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_54,c_418]) ).
tff(c_578,plain,
$uminus($product(b,$uminus(d))) = '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_57,c_494]) ).
tff(c_160134,plain,
$product(b,$uminus(d)) = $uminus('#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_578]) ).
tff(c_160349,plain,
( $less(0,$uminus('#skE_1'))
| ~ $less(0,b)
| ~ $less(0,$uminus(d)) ),
inference(superposition,[status(thm),theory(equality)],[c_160134,c_48]) ).
tff(c_160789,plain,
( $less(0,$uminus('#skE_1'))
| ~ $less(0,$uminus(d)) ),
inference(demodulation,[status(thm),theory(equality)],[c_153007,c_160349]) ).
tff(c_160791,plain,
( $less('#skE_1',0)
| ~ $less(d,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_160789]) ).
tff(c_160982,plain,
~ $less(d,0),
inference(splitLeft,[status(thm)],[c_160791]) ).
tff(c_160983,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_160982,c_589,c_242]) ).
tff(c_160987,plain,
$less(d,0),
inference(splitRight,[status(thm)],[c_160791]) ).
tff(c_43,plain,
$less(0,$product(c,d)),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_592,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_987,plain,
$product(d,c) = '#skE_3',
inference(superposition,[status(thm),theory(equality)],[c_57,c_592]) ).
tff(c_1034,plain,
$uminus($product($uminus(d),c)) = '#skE_3',
inference(superposition,[status(thm),theory(equality)],[c_987,c_54]) ).
tff(c_1136,plain,
$uminus($product(c,$uminus(d))) = '#skE_3',
inference(demodulation,[status(thm),theory(equality)],[c_57,c_1034]) ).
tff(c_162003,plain,
$product(c,$uminus(d)) = $uminus('#skE_3'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1136]) ).
tff(c_162673,plain,
( $less(0,$uminus('#skE_3'))
| ~ $less(0,c)
| ~ $less(0,$uminus(d)) ),
inference(superposition,[status(thm),theory(equality)],[c_162003,c_48]) ).
tff(c_162675,plain,
( $less('#skE_3',0)
| ~ $less(0,c)
| ~ $less(d,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_162673]) ).
tff(c_164729,plain,
( $less('#skE_3',0)
| ~ $less(0,c) ),
inference(demodulation,[status(thm),theory(equality)],[c_160987,c_162675]) ).
tff(c_164731,plain,
~ $less(0,c),
inference(splitLeft,[status(thm)],[c_164729]) ).
tff(c_47,plain,
$less(0,$product(a,c)),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_245,plain,
$product(a,c) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_47]) ).
tff(c_1396,plain,
$product(c,a) = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_57,c_245]) ).
tff(c_1502,plain,
$uminus($product($uminus(c),a)) = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_54,c_1396]) ).
tff(c_1607,plain,
$uminus($product(a,$uminus(c))) = '#skE_2',
inference(demodulation,[status(thm),theory(equality)],[c_57,c_1502]) ).
tff(c_158487,plain,
$product(a,$uminus(c)) = $uminus('#skE_2'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1607]) ).
tff(c_159119,plain,
( $less(0,$uminus('#skE_2'))
| ~ $less(0,a)
| ~ $less(0,$uminus(c)) ),
inference(superposition,[status(thm),theory(equality)],[c_158487,c_48]) ).
tff(c_159121,plain,
( $less('#skE_2',0)
| ~ $less(0,a)
| ~ $less(c,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_159119]) ).
tff(c_161879,plain,
~ $less(c,0),
inference(splitLeft,[status(thm)],[c_159121]) ).
tff(c_731,plain,
( ( '#skE_3' = 0 )
| ( c != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_592,c_49]) ).
tff(c_770,plain,
c != 0,
inference(splitLeft,[status(thm)],[c_731]) ).
tff(c_164733,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_164731,c_161879,c_770]) ).
tff(c_164736,plain,
$less('#skE_3',0),
inference(splitRight,[status(thm)],[c_164729]) ).
tff(c_408,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_62,plain,
$less(0,$product(c,d)),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_415,plain,
$less(0,'#skE_3'),
inference(demodulation,[status(thm),theory(equality)],[c_408,c_62]) ).
tff(c_164738,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_164736,c_415]) ).
tff(c_164741,plain,
( ~ $less(0,a)
| $less('#skE_2',0) ),
inference(splitRight,[status(thm)],[c_159121]) ).
tff(c_164744,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_164741]) ).
tff(c_153006,plain,
( ~ $less(a,0)
| $less('#skE_4',0) ),
inference(splitRight,[status(thm)],[c_2652]) ).
tff(c_153063,plain,
~ $less(a,0),
inference(splitLeft,[status(thm)],[c_153006]) ).
tff(c_397,plain,
( ( '#skE_2' = 0 )
| ( a != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_49,c_245]) ).
tff(c_403,plain,
a != 0,
inference(splitLeft,[status(thm)],[c_397]) ).
tff(c_164745,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_164744,c_153063,c_403]) ).
tff(c_164748,plain,
$less('#skE_2',0),
inference(splitRight,[status(thm)],[c_164741]) ).
tff(c_227,plain,
$product(a,c) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_47]) ).
tff(c_63,plain,
$less(0,$product(a,c)),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_234,plain,
$less(0,'#skE_2'),
inference(demodulation,[status(thm),theory(equality)],[c_227,c_63]) ).
tff(c_164750,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_164748,c_234]) ).
tff(c_164753,plain,
$less('#skE_4',0),
inference(splitRight,[status(thm)],[c_153006]) ).
tff(c_772,plain,
$product(a,b) = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_39]) ).
tff(c_61,plain,
$less(0,$product(a,b)),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_779,plain,
$less(0,'#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_772,c_61]) ).
tff(c_164756,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_164753,c_779]) ).
tff(c_164759,plain,
'#skE_3' = 0,
inference(splitRight,[status(thm)],[c_731]) ).
tff(c_164766,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_164759,c_415]) ).
tff(c_164778,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_164766]) ).
tff(c_164782,plain,
d = 0,
inference(splitRight,[status(thm)],[c_550]) ).
tff(c_414,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_164813,plain,
$product(c,0) = '#skE_3',
inference(demodulation,[status(thm),theory(equality)],[c_164782,c_414]) ).
tff(c_164815,plain,
'#skE_3' = 0,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_164813]) ).
tff(c_164816,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_164815,c_415]) ).
tff(c_164819,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_164816]) ).
tff(c_164822,plain,
'#skE_2' = 0,
inference(splitRight,[status(thm)],[c_397]) ).
tff(c_164829,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_164822,c_234]) ).
tff(c_164841,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_164829]) ).
tff(c_164845,plain,
$less(0,d),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_217,plain,
$uminus($product($uminus(b),d)) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_54,c_81]) ).
tff(c_167623,plain,
$product($uminus(b),d) = $uminus('#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_217]) ).
tff(c_167703,plain,
( $less(0,$uminus('#skE_1'))
| ~ $less(0,$uminus(b))
| ~ $less(0,d) ),
inference(superposition,[status(thm),theory(equality)],[c_167623,c_48]) ).
tff(c_167850,plain,
( $less(0,$uminus('#skE_1'))
| ~ $less(0,$uminus(b)) ),
inference(demodulation,[status(thm),theory(equality)],[c_164845,c_167703]) ).
tff(c_167852,plain,
( $less('#skE_1',0)
| ~ $less(b,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_167850]) ).
tff(c_167924,plain,
~ $less(b,0),
inference(splitLeft,[status(thm)],[c_167852]) ).
tff(c_164844,plain,
~ $less(0,b),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_167925,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_167924,c_164844,c_236]) ).
tff(c_167929,plain,
$less(b,0),
inference(splitRight,[status(thm)],[c_167852]) ).
tff(c_165143,plain,
$product(a,b) = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_39]) ).
tff(c_165663,plain,
$product(b,a) = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_57,c_165143]) ).
tff(c_165755,plain,
$uminus($product($uminus(b),a)) = '#skE_4',
inference(superposition,[status(thm),theory(equality)],[c_54,c_165663]) ).
tff(c_165843,plain,
$uminus($product(a,$uminus(b))) = '#skE_4',
inference(demodulation,[status(thm),theory(equality)],[c_57,c_165755]) ).
tff(c_196148,plain,
$product(a,$uminus(b)) = $uminus('#skE_4'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_165843]) ).
tff(c_196838,plain,
( $less(0,$uminus('#skE_4'))
| ~ $less(0,a)
| ~ $less(0,$uminus(b)) ),
inference(superposition,[status(thm),theory(equality)],[c_196148,c_48]) ).
tff(c_196840,plain,
( $less('#skE_4',0)
| ~ $less(0,a)
| ~ $less(b,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_196838]) ).
tff(c_197090,plain,
( $less('#skE_4',0)
| ~ $less(0,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_167929,c_196840]) ).
tff(c_197092,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_197090]) ).
tff(c_164988,plain,
$product(a,c) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_47]) ).
tff(c_165123,plain,
$uminus($product($uminus(a),c)) = '#skE_2',
inference(superposition,[status(thm),theory(equality)],[c_54,c_164988]) ).
tff(c_166553,plain,
$product($uminus(a),c) = $uminus('#skE_2'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_165123]) ).
tff(c_166741,plain,
( $less(0,$uminus('#skE_2'))
| ~ $less(0,$uminus(a))
| ~ $less(0,c) ),
inference(superposition,[status(thm),theory(equality)],[c_166553,c_48]) ).
tff(c_166743,plain,
( $less('#skE_2',0)
| ~ $less(a,0)
| ~ $less(0,c) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_166741]) ).
tff(c_185319,plain,
~ $less(0,c),
inference(splitLeft,[status(thm)],[c_166743]) ).
tff(c_165309,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_165467,plain,
$uminus($product($uminus(c),d)) = '#skE_3',
inference(superposition,[status(thm),theory(equality)],[c_54,c_165309]) ).
tff(c_167339,plain,
$product($uminus(c),d) = $uminus('#skE_3'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_165467]) ).
tff(c_167416,plain,
( $less(0,$uminus('#skE_3'))
| ~ $less(0,$uminus(c))
| ~ $less(0,d) ),
inference(superposition,[status(thm),theory(equality)],[c_167339,c_48]) ).
tff(c_167559,plain,
( $less(0,$uminus('#skE_3'))
| ~ $less(0,$uminus(c)) ),
inference(demodulation,[status(thm),theory(equality)],[c_164845,c_167416]) ).
tff(c_167561,plain,
( $less('#skE_3',0)
| ~ $less(c,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_167559]) ).
tff(c_167921,plain,
~ $less(c,0),
inference(splitLeft,[status(thm)],[c_167561]) ).
tff(c_166308,plain,
! [A_19790: $int] :
( ( $product(A_19790,d) = $uminus('#skE_3') )
| ( c != $uminus(A_19790) ) ),
inference(superposition,[status(thm),theory(equality)],[c_165309,c_54]) ).
tff(c_165303,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_166446,plain,
( ( $uminus('#skE_3') = '#skE_3' )
| ( $uminus(c) != c ) ),
inference(superposition,[status(thm),theory(equality)],[c_166308,c_165303]) ).
tff(c_166448,plain,
( ( '#skE_3' = 0 )
| ( c != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_166446]) ).
tff(c_166549,plain,
c != 0,
inference(splitLeft,[status(thm)],[c_166448]) ).
tff(c_185320,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_185319,c_167921,c_166549]) ).
tff(c_185323,plain,
( ~ $less(a,0)
| $less('#skE_2',0) ),
inference(splitRight,[status(thm)],[c_166743]) ).
tff(c_185326,plain,
~ $less(a,0),
inference(splitLeft,[status(thm)],[c_185323]) ).
tff(c_233,plain,
$product(a,c) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_47]) ).
tff(c_166694,plain,
( ( $uminus('#skE_2') = '#skE_2' )
| ( $uminus(a) != a ) ),
inference(superposition,[status(thm),theory(equality)],[c_166553,c_233]) ).
tff(c_166696,plain,
( ( '#skE_2' = 0 )
| ( a != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_166694]) ).
tff(c_166794,plain,
a != 0,
inference(splitLeft,[status(thm)],[c_166696]) ).
tff(c_197093,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_197092,c_185326,c_166794]) ).
tff(c_197096,plain,
$less('#skE_4',0),
inference(splitRight,[status(thm)],[c_197090]) ).
tff(c_165129,plain,
$product(a,b) = '#skE_4',
inference(define,[status(thm),theory(equality)],[c_39]) ).
tff(c_165136,plain,
$less(0,'#skE_4'),
inference(demodulation,[status(thm),theory(equality)],[c_165129,c_61]) ).
tff(c_197098,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_197096,c_165136]) ).
tff(c_197101,plain,
$less('#skE_2',0),
inference(splitRight,[status(thm)],[c_185323]) ).
tff(c_197103,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_197101,c_234]) ).
tff(c_197106,plain,
$less('#skE_3',0),
inference(splitRight,[status(thm)],[c_167561]) ).
tff(c_165297,plain,
$product(c,d) = '#skE_3',
inference(define,[status(thm),theory(equality)],[c_43]) ).
tff(c_165304,plain,
$less(0,'#skE_3'),
inference(demodulation,[status(thm),theory(equality)],[c_165297,c_62]) ).
tff(c_197108,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_197106,c_165304]) ).
tff(c_197111,plain,
'#skE_2' = 0,
inference(splitRight,[status(thm)],[c_166696]) ).
tff(c_197133,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_197111,c_234]) ).
tff(c_197146,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_197133]) ).
tff(c_197149,plain,
'#skE_3' = 0,
inference(splitRight,[status(thm)],[c_166448]) ).
tff(c_197171,plain,
$less(0,0),
inference(demodulation,[status(thm),theory(equality)],[c_197149,c_165304]) ).
tff(c_197185,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_197171]) ).
tff(c_197189,plain,
b = 0,
inference(splitRight,[status(thm)],[c_195]) ).
tff(c_197635,plain,
$less(0,$product(0,a)),
inference(demodulation,[status(thm),theory(equality)],[c_57,c_197189,c_39]) ).
tff(c_197637,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_197635]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ARI681_1 : TPTP v9.0.0. Released v6.3.0.
% 0.07/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.33 % Computer : n031.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Apr 7 15:16:52 EDT 2025
% 0.13/0.33 % CPUTime :
% 38.56/15.15 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.83/15.17
% 38.83/15.17 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------