%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC474_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 : n017.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 35.26s 15.00s
% Output : CNFRefutation 35.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 15
% Syntax : Number of formulae : 98 ( 70 unt; 0 typ; 0 def)
% Number of atoms : 143 ( 91 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 79 ( 34 ~; 36 |; 4 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 302 ( 51 atm; 97 fun; 80 num; 74 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 : 104 ( 97 usr; 90 con; 0-2 aty)
% Number of variables : 74 ( 73 !; 1 ?; 74 :)
% Comments :
%------------------------------------------------------------------------------
%$ u1 > u0 > #nlpp > v1 > v0 > small > h1 > h0 > fast > f1 > f0
%Foreground sorts:
%Background operators:
tff('#skE_46',type,
'#skE_46': $int ).
tff('#skE_74',type,
'#skE_74': $int ).
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_21',type,
'#skE_21': $int ).
tff('#skE_62',type,
'#skE_62': $int ).
tff('#skE_30',type,
'#skE_30': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_52',type,
'#skE_52': $int ).
tff('#skE_28',type,
'#skE_28': $int ).
tff('#skE_48',type,
'#skE_48': $int ).
tff('#skE_23',type,
'#skE_23': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_41',type,
'#skE_41': $int ).
tff(g0,type,
g0: $int ).
tff('#skE_43',type,
'#skE_43': $int ).
tff('#skE_37',type,
'#skE_37': $int ).
tff('#skE_73',type,
'#skE_73': $int ).
tff('#skE_80',type,
'#skE_80': $int ).
tff('#skE_84',type,
'#skE_84': $int ).
tff('#skE_42',type,
'#skE_42': $int ).
tff('#skE_57',type,
'#skE_57': $int ).
tff('#skE_63',type,
'#skE_63': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_33',type,
'#skE_33': $int ).
tff('#skE_20',type,
'#skE_20': $int ).
tff('#skE_78',type,
'#skE_78': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_26',type,
'#skE_26': $int ).
tff('#skE_32',type,
'#skE_32': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_38',type,
'#skE_38': $int ).
tff('#skE_31',type,
'#skE_31': $int ).
tff('#skE_51',type,
'#skE_51': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_36',type,
'#skE_36': $int ).
tff('#skE_69',type,
'#skE_69': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_54',type,
'#skE_54': $int ).
tff('#skE_76',type,
'#skE_76': $int ).
tff('#skE_70',type,
'#skE_70': $int ).
tff('#skE_64',type,
'#skE_64': $int ).
tff('#skE_82',type,
'#skE_82': $int ).
tff('#skE_60',type,
'#skE_60': $int ).
tff('#skE_50',type,
'#skE_50': $int ).
tff('#skE_22',type,
'#skE_22': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_55',type,
'#skE_55': $int ).
tff('#skF_1',type,
'#skF_1': $int ).
tff('#skE_77',type,
'#skE_77': $int ).
tff('#skE_79',type,
'#skE_79': $int ).
tff('#skE_71',type,
'#skE_71': $int ).
tff('#skE_67',type,
'#skE_67': $int ).
tff('#skE_58',type,
'#skE_58': $int ).
tff('#skE_47',type,
'#skE_47': $int ).
tff('#skE_68',type,
'#skE_68': $int ).
tff('#skE_40',type,
'#skE_40': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_75',type,
'#skE_75': $int ).
tff('#skE_29',type,
'#skE_29': $int ).
tff('#skE_44',type,
'#skE_44': $int ).
tff('#skE_49',type,
'#skE_49': $int ).
tff('#skE_34',type,
'#skE_34': $int ).
tff('#skE_45',type,
'#skE_45': $int ).
tff('#skE_27',type,
'#skE_27': $int ).
tff('#skE_59',type,
'#skE_59': $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_83',type,
'#skE_83': $int ).
tff('#skE_81',type,
'#skE_81': $int ).
tff('#skE_35',type,
'#skE_35': $int ).
tff(g1,type,
g1: $int ).
tff('#skE_61',type,
'#skE_61': $int ).
tff('#skE_39',type,
'#skE_39': $int ).
tff('#skE_66',type,
'#skE_66': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_53',type,
'#skE_53': $int ).
tff('#skE_65',type,
'#skE_65': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
tff('#skE_72',type,
'#skE_72': $int ).
tff('#skE_56',type,
'#skE_56': $int ).
%Foreground operators:
tff(fast,type,
fast: $int > $int ).
tff(small,type,
small: $int > $int ).
tff(f1,type,
f1: $int > $int ).
tff(f0,type,
f0: $int > $int ).
tff(u1,type,
u1: ( $int * $int ) > $int ).
tff(u0,type,
u0: ( $int * $int ) > $int ).
tff(v0,type,
v0: $int > $int ).
tff(v1,type,
v1: $int > $int ).
tff(h0,type,
h0: $int > $int ).
tff(h1,type,
h1: $int > $int ).
tff(f_89,negated_conjecture,
~ ~ ? [Ca: $int] :
( $greatereq(Ca,0)
& ( small(Ca) != fast(Ca) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
tff(f_51,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) ).
tff(f_38,axiom,
g0 = 2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2) ).
tff(f_41,axiom,
! [Xa: $int] : ( h0(Xa) = Xa ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3) ).
tff(f_54,axiom,
! [Xa: $int] : ( v0(Xa) = u0(g0,h0(Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_5) ).
tff(f_57,axiom,
! [Xa: $int] : ( small(Xa) = $sum($product(v0(Xa),Xa),Xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_6) ).
tff(f_445,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_36,axiom,
! [Xa: $int] : ( f0(Xa) = $product($product(Xa,Xa),Xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1) ).
tff(f_60,axiom,
! [Xa: $int] : ( f1(Xa) = $product($product(Xa,Xa),Xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_7) ).
tff(f_65,axiom,
! [Xa: $int] : ( h1(Xa) = $product($product(Xa,Xa),Xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_9) ).
tff(f_62,axiom,
g1 = 1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_8) ).
tff(f_78,axiom,
! [Xa: $int] : ( v1(Xa) = u1(g1,h1(Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_11) ).
tff(f_75,axiom,
! [Xa: $int,Ya: $int] :
( ( $lesseq(Xa,0)
=> ( u1(Xa,Ya) = Ya ) )
& ( ~ $lesseq(Xa,0)
=> ( u1(Xa,Ya) = f1(u1($difference(Xa,1),Ya)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_10) ).
tff(f_420,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_81,axiom,
! [Xa: $int] : ( fast(Xa) = $sum($product(v1(Xa),Xa),Xa) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_12) ).
tff(c_60,plain,
small('#skF_1') != fast('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_210,plain,
fast('#skF_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_60]) ).
tff(c_209,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_60]) ).
tff(c_105,plain,
small('#skF_1') != fast('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_221,plain,
'#skE_2' != '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_210,c_209,c_105]) ).
tff(c_217,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_60]) ).
tff(c_6,plain,
! [X_3a: $int,Y_4a: $int] :
( ( u0(X_3a,Y_4a) = Y_4a )
| ~ $lesseq(X_3a,0) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_89,plain,
! [X_3a: $int,Y_4a: $int] :
( ( u0(X_3a,Y_4a) = Y_4a )
| $less(0,X_3a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_6]) ).
tff(c_8,plain,
! [X_3a: $int,Y_4a: $int] :
( ( f0(u0($sum($uminus(1),X_3a),Y_4a)) = u0(X_3a,Y_4a) )
| $lesseq(X_3a,0) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_88,plain,
! [X_3a: $int,Y_4a: $int] :
( ( f0(u0($sum($uminus(1),X_3a),Y_4a)) = u0(X_3a,Y_4a) )
| ~ $less(0,X_3a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_8]) ).
tff(c_961,plain,
! [X_122a: $int,Y_123a: $int] :
( ( f0(u0($sum($uminus(1),X_122a),Y_123a)) = u0(X_122a,Y_123a) )
| ~ $less(0,X_122a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_8]) ).
tff(c_91,plain,
g0 = 2,
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_90,plain,
! [X_2a: $int] : ( h0(X_2a) = X_2a ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_84,plain,
! [X_5a: $int] : ( u0(g0,h0(X_5a)) = v0(X_5a) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_129,plain,
! [X_5a: $int] : ( u0(g0,X_5a) = v0(X_5a) ),
inference(demodulation,[status(thm),theory(equality)],[c_90,c_84]) ).
tff(c_133,plain,
! [X_5a: $int] : ( u0(2,X_5a) = v0(X_5a) ),
inference(demodulation,[status(thm),theory(equality)],[c_91,c_129]) ).
tff(c_1013,plain,
! [Y_123a: $int] :
( ( f0(u0($sum($uminus(1),2),Y_123a)) = v0(Y_123a) )
| ~ $less(0,2) ),
inference(superposition,[status(thm),theory(equality)],[c_961,c_133]) ).
tff(c_1040,plain,
! [Y_127a: $int] : ( f0(u0(1,Y_127a)) = v0(Y_127a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1013]) ).
tff(c_1074,plain,
! [Y_4a: $int] :
( ( f0(f0(u0($sum($uminus(1),1),Y_4a))) = v0(Y_4a) )
| ~ $less(0,1) ),
inference(superposition,[status(thm),theory(equality)],[c_88,c_1040]) ).
tff(c_1124,plain,
! [Y_129a: $int] : ( f0(f0(u0(0,Y_129a))) = v0(Y_129a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1074]) ).
tff(c_1142,plain,
! [Y_4a: $int] :
( ( v0(Y_4a) = f0(f0(Y_4a)) )
| $less(0,0) ),
inference(superposition,[status(thm),theory(equality)],[c_89,c_1124]) ).
tff(c_1155,plain,
! [Y_4a: $int] : ( v0(Y_4a) = f0(f0(Y_4a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1142]) ).
tff(c_13,plain,
! [X_6a: $int] : ( $sum($product(v0(X_6a),X_6a),X_6a) = small(X_6a) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_405,plain,
! [X_82a: $int] : ( $product(v0(X_82a),X_82a) = $sum($uminus(X_82a),small(X_82a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_13]) ).
tff(c_93,plain,
! [A_39: $int,B_40: $int] :
( $less(0,$product(A_39,B_40))
| ~ $less(0,A_39)
| ~ $less(0,B_40) ),
inference(cnfTransformation,[status(thm)],[f_445]) ).
tff(c_508,plain,
! [X_82a: $int] :
( $less(0,$sum($uminus(X_82a),small(X_82a)))
| ~ $less(0,v0(X_82a))
| ~ $less(0,X_82a) ),
inference(superposition,[status(thm),theory(equality)],[c_405,c_93]) ).
tff(c_510,plain,
! [X_82a: $int] :
( $less(X_82a,small(X_82a))
| ~ $less(0,v0(X_82a))
| ~ $less(0,X_82a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_508]) ).
tff(c_4524,plain,
! [X_218a: $int] :
( $less(X_218a,small(X_218a))
| ~ $less(0,f0(f0(X_218a)))
| ~ $less(0,X_218a) ),
inference(demodulation,[status(thm),theory(equality)],[c_1155,c_510]) ).
tff(c_4542,plain,
( $less('#skF_1','#skE_1')
| ~ $less(0,f0(f0('#skF_1')))
| ~ $less(0,'#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_217,c_4524]) ).
tff(c_4689,plain,
f0('#skF_1') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_4542]) ).
tff(c_4688,plain,
( $less('#skF_1','#skE_1')
| ~ $less(0,f0(f0('#skF_1')))
| ~ $less(0,'#skF_1') ),
inference(superposition,[status(thm),theory(equality)],[c_217,c_4524]) ).
tff(c_4699,plain,
( $less('#skF_1','#skE_1')
| ~ $less(0,f0('#skE_11'))
| ~ $less(0,'#skF_1') ),
inference(demodulation,[status(thm),theory(equality)],[c_4689,c_4688]) ).
tff(c_5380,plain,
f0('#skE_11') = '#skE_12',
inference(define,[status(thm),theory(equality)],[c_4699]) ).
tff(c_4942,plain,
f0('#skF_1') = '#skE_11',
inference(define,[status(thm),theory(equality)],[c_4542]) ).
tff(c_92,plain,
! [X_1a: $int] : ( $product($product(X_1a,X_1a),X_1a) = f0(X_1a) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_76,plain,
! [X_7a: $int] : ( $product($product(X_7a,X_7a),X_7a) = f1(X_7a) ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_135,plain,
! [X_7a: $int] : ( f1(X_7a) = f0(X_7a) ),
inference(demodulation,[status(thm),theory(equality)],[c_92,c_76]) ).
tff(c_74,plain,
! [X_8a: $int] : ( $product($product(X_8a,X_8a),X_8a) = h1(X_8a) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_116,plain,
! [X_8a: $int] : ( h1(X_8a) = f1(X_8a) ),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_74]) ).
tff(c_75,plain,
g1 = 1,
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_68,plain,
! [X_11a: $int] : ( u1(g1,h1(X_11a)) = v1(X_11a) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_114,plain,
! [X_11a: $int] : ( u1(1,h1(X_11a)) = v1(X_11a) ),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_68]) ).
tff(c_118,plain,
! [X_11a: $int] : ( u1(1,f1(X_11a)) = v1(X_11a) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_114]) ).
tff(c_139,plain,
! [X_11a: $int] : ( u1(1,f0(X_11a)) = v1(X_11a) ),
inference(demodulation,[status(thm),theory(equality)],[c_135,c_118]) ).
tff(c_4981,plain,
u1(1,'#skE_11') = v1('#skF_1'),
inference(superposition,[status(thm),theory(equality)],[c_4942,c_139]) ).
tff(c_6475,plain,
u1(1,'#skE_11') = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_4981]) ).
tff(c_20,plain,
! [X_9a: $int,Y_10a: $int] :
( ( u1(X_9a,Y_10a) = Y_10a )
| ~ $lesseq(X_9a,0) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_73,plain,
! [X_9a: $int,Y_10a: $int] :
( ( u1(X_9a,Y_10a) = Y_10a )
| $less(0,X_9a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_20]) ).
tff(c_22,plain,
! [X_9a: $int,Y_10a: $int] :
( ( f1(u1($sum($uminus(1),X_9a),Y_10a)) = u1(X_9a,Y_10a) )
| $lesseq(X_9a,0) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_1208,plain,
! [X_134a: $int,Y_135a: $int] :
( ( f1(u1($sum($uminus(1),X_134a),Y_135a)) = u1(X_134a,Y_135a) )
| ~ $less(0,X_134a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_22]) ).
tff(c_1255,plain,
! [X_134a: $int,Y_10a: $int] :
( ( u1(X_134a,Y_10a) = f1(Y_10a) )
| ~ $less(0,X_134a)
| $less(0,$sum($uminus(1),X_134a)) ),
inference(superposition,[status(thm),theory(equality)],[c_73,c_1208]) ).
tff(c_1315,plain,
! [X_134a: $int,Y_10a: $int] :
( ( u1(X_134a,Y_10a) = f0(Y_10a) )
| ~ $less(0,X_134a)
| $less(0,$sum($uminus(1),X_134a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_135,c_1255]) ).
tff(c_1317,plain,
! [X_134a: $int,Y_10a: $int] :
( ( u1(X_134a,Y_10a) = f0(Y_10a) )
| ~ $less(0,X_134a)
| $less(1,X_134a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1315]) ).
tff(c_6481,plain,
( ( f0('#skE_11') = '#skE_13' )
| ~ $less(0,1)
| $less(1,1) ),
inference(superposition,[status(thm),theory(equality)],[c_6475,c_1317]) ).
tff(c_6523,plain,
( ( '#skE_13' = '#skE_12' )
| ~ $less(0,1)
| $less(1,1) ),
inference(demodulation,[status(thm),theory(equality)],[c_5380,c_6481]) ).
tff(c_6525,plain,
'#skE_13' = '#skE_12',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6523]) ).
tff(c_238,plain,
fast('#skF_1') = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_60]) ).
tff(c_5919,plain,
v1('#skF_1') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_4981]) ).
tff(c_5918,plain,
u1(1,'#skE_11') = '#skE_13',
inference(define,[status(thm),theory(equality)],[c_4981]) ).
tff(c_5917,plain,
u1(1,'#skE_11') = v1('#skF_1'),
inference(superposition,[status(thm),theory(equality)],[c_4942,c_139]) ).
tff(c_5930,plain,
'#skE_14' = '#skE_13',
inference(demodulation,[status(thm),theory(equality)],[c_5919,c_5918,c_5917]) ).
tff(c_5929,plain,
v1('#skF_1') = '#skE_14',
inference(define,[status(thm),theory(equality)],[c_4981]) ).
tff(c_6130,plain,
v1('#skF_1') = '#skE_13',
inference(demodulation,[status(thm),theory(equality)],[c_5930,c_5929]) ).
tff(c_102,plain,
! [B_19: $int,A_20: $int] : ( $product(B_19,A_20) = $product(A_20,B_19) ),
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_27,plain,
! [X_12a: $int] : ( $sum($product(v1(X_12a),X_12a),X_12a) = fast(X_12a) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_704,plain,
! [X_103a: $int] : ( $product(v1(X_103a),X_103a) = $sum($uminus(X_103a),fast(X_103a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_27]) ).
tff(c_827,plain,
! [X_103a: $int] : ( $product(X_103a,v1(X_103a)) = $sum($uminus(X_103a),fast(X_103a)) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_704]) ).
tff(c_6140,plain,
$product('#skF_1','#skE_13') = $sum($uminus('#skF_1'),fast('#skF_1')),
inference(superposition,[status(thm),theory(equality)],[c_6130,c_827]) ).
tff(c_6163,plain,
$product('#skF_1','#skE_13') = $sum($uminus('#skF_1'),'#skE_2'),
inference(demodulation,[status(thm),theory(equality)],[c_238,c_6140]) ).
tff(c_6166,plain,
$product('#skF_1','#skE_13') = $sum('#skE_2',$uminus('#skF_1')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6163]) ).
tff(c_76851,plain,
$product('#skF_1','#skE_12') = $sum('#skE_2',$uminus('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_6525,c_6166]) ).
tff(c_76856,plain,
$product('#skF_1','#skE_12') = $sum($uminus('#skF_1'),'#skE_2'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_76851]) ).
tff(c_223,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_60]) ).
tff(c_520,plain,
! [X_82a: $int] : ( $product(X_82a,v0(X_82a)) = $sum($uminus(X_82a),small(X_82a)) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_405]) ).
tff(c_2682,plain,
! [X_82a: $int] : ( $product(X_82a,f0(f0(X_82a))) = $sum($uminus(X_82a),small(X_82a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_1155,c_520]) ).
tff(c_4949,plain,
$product('#skF_1',f0('#skE_11')) = $sum($uminus('#skF_1'),small('#skF_1')),
inference(superposition,[status(thm),theory(equality)],[c_4942,c_2682]) ).
tff(c_4975,plain,
$product('#skF_1',f0('#skE_11')) = $sum($uminus('#skF_1'),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_223,c_4949]) ).
tff(c_4978,plain,
$product('#skF_1',f0('#skE_11')) = $sum('#skE_1',$uminus('#skF_1')),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4975]) ).
tff(c_68567,plain,
$product('#skF_1','#skE_12') = $sum('#skE_1',$uminus('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_5380,c_4978]) ).
tff(c_68570,plain,
$product('#skF_1','#skE_12') = $sum($uminus('#skF_1'),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_68567]) ).
tff(c_77073,plain,
$sum($uminus('#skF_1'),'#skE_2') = $sum($uminus('#skF_1'),'#skE_1'),
inference(superposition,[status(thm),theory(equality)],[c_76856,c_68570]) ).
tff(c_77075,plain,
'#skE_2' = '#skE_1',
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_77073]) ).
tff(c_77232,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_221,c_77075]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWC474_1 : TPTP v9.0.0. Released v9.0.0.
% 0.03/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 : n017.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:10 EDT 2025
% 0.13/0.34 % CPUTime :
% 35.26/15.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.26/15.01
% 35.26/15.01 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------