%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC438_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 : n010.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:27 PM UTC 2025
% Result : Theorem 3.78s 2.01s
% Output : CNFRefutation 3.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 41 ( 30 unt; 0 typ; 0 def)
% Number of atoms : 54 ( 41 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 27 ( 14 ~; 9 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 173 ( 12 atm; 57 fun; 68 num; 36 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 : 21 ( 9 usr; 11 con; 0-2 aty)
% Number of variables : 36 ( 35 !; 1 ?; 36 :)
% Comments :
%------------------------------------------------------------------------------
%$ u0 > #nlpp > v0 > small > h0 > fast > f0
%Foreground sorts:
%Background operators:
tff(g0,type,
g0: $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skF_1',type,
'#skF_1': $int ).
%Foreground operators:
tff(fast,type,
fast: $int > $int ).
tff(small,type,
small: $int > $int ).
tff(f0,type,
f0: $int > $int ).
tff(u0,type,
u0: ( $int * $int ) > $int ).
tff(v0,type,
v0: $int > $int ).
tff(h0,type,
h0: $int > $int ).
tff(f_34,axiom,
! [Xa: $int] : ( f0(Xa) = $sum(1,$sum(Xa,Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1) ).
tff(f_49,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_36,axiom,
g0 = 2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2) ).
tff(f_39,axiom,
! [Xa: $int] : ( h0(Xa) = Xa ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3) ).
tff(f_52,axiom,
! [Xa: $int] : ( v0(Xa) = u0(g0,h0(Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_5) ).
tff(f_55,axiom,
! [Xa: $int] : ( small(Xa) = $product(2,$sum(v0(Xa),Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_6) ).
tff(f_58,axiom,
! [Xa: $int] : ( fast(Xa) = $sum(1,$product($sum(1,$sum(2,2)),$sum(1,$sum(Xa,Xa)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_7) ).
tff(f_66,negated_conjecture,
~ ~ ? [Ca: $int] :
( $greatereq(Ca,0)
& ( small(Ca) != fast(Ca) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
tff(c_43,plain,
! [X_1a: $int] : ( f0(X_1a) = $sum(1,$product(2,X_1a)) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
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_49]) ).
tff(c_40,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_49]) ).
tff(c_39,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_171,plain,
! [X_33a: $int,Y_34a: $int] :
( ( f0(u0($sum($uminus(1),X_33a),Y_34a)) = u0(X_33a,Y_34a) )
| ~ $less(0,X_33a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_8]) ).
tff(c_42,plain,
g0 = 2,
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_41,plain,
! [X_2a: $int] : ( h0(X_2a) = X_2a ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_35,plain,
! [X_5a: $int] : ( u0(g0,h0(X_5a)) = v0(X_5a) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_63,plain,
! [X_5a: $int] : ( u0(g0,X_5a) = v0(X_5a) ),
inference(demodulation,[status(thm),theory(equality)],[c_41,c_35]) ).
tff(c_67,plain,
! [X_5a: $int] : ( u0(2,X_5a) = v0(X_5a) ),
inference(demodulation,[status(thm),theory(equality)],[c_42,c_63]) ).
tff(c_223,plain,
! [Y_34a: $int] :
( ( f0(u0($sum($uminus(1),2),Y_34a)) = v0(Y_34a) )
| ~ $less(0,2) ),
inference(superposition,[status(thm),theory(equality)],[c_171,c_67]) ).
tff(c_251,plain,
! [Y_38a: $int] : ( f0(u0(1,Y_38a)) = v0(Y_38a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_223]) ).
tff(c_285,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_39,c_251]) ).
tff(c_336,plain,
! [Y_40a: $int] : ( f0(f0(u0(0,Y_40a))) = v0(Y_40a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_285]) ).
tff(c_354,plain,
! [Y_4a: $int] :
( ( v0(Y_4a) = f0(f0(Y_4a)) )
| $less(0,0) ),
inference(superposition,[status(thm),theory(equality)],[c_40,c_336]) ).
tff(c_366,plain,
! [Y_4a: $int] :
( ( v0(Y_4a) = $sum(1,$product(2,$sum(1,$product(2,Y_4a)))) )
| $less(0,0) ),
inference(demodulation,[status(thm),theory(equality)],[c_43,c_43,c_354]) ).
tff(c_368,plain,
! [Y_4a: $int] : ( v0(Y_4a) = $sum(3,$product(4,Y_4a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_366]) ).
tff(c_13,plain,
! [X_6a: $int] : ( $product(2,$sum(X_6a,v0(X_6a))) = small(X_6a) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_31,plain,
! [X_6a: $int] : ( $sum($product(2,X_6a),$product(2,v0(X_6a))) = small(X_6a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_13]) ).
tff(c_428,plain,
! [X_6a: $int] : ( small(X_6a) = $sum($product(2,X_6a),$product(2,$sum(3,$product(4,X_6a)))) ),
inference(demodulation,[status(thm),theory(equality)],[c_368,c_31]) ).
tff(c_813,plain,
! [X_70a: $int] : ( small(X_70a) = $sum(6,$product(10,X_70a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_428]) ).
tff(c_16,plain,
! [X_7a: $int] : ( fast(X_7a) = $sum(1,$sum(5,$product(10,X_7a))) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_27,plain,
! [X_7a: $int] : ( fast(X_7a) = $sum(6,$product(10,X_7a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_16]) ).
tff(c_26,plain,
small('#skF_1') != fast('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_50,plain,
small('#skF_1') != $sum(6,$product(10,'#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_27,c_26]) ).
tff(c_140,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_50]) ).
tff(c_829,plain,
$sum(6,$product(10,'#skF_1')) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_813,c_140]) ).
tff(c_134,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_50]) ).
tff(c_52,plain,
small('#skF_1') != $sum(6,$product(10,'#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_27,c_26]) ).
tff(c_136,plain,
$sum(6,$product(10,'#skF_1')) != '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_134,c_52]) ).
tff(c_142,plain,
$product(10,'#skF_1') != $sum($uminus(6),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_136]) ).
tff(c_834,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_829,c_142]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWC438_1 : TPTP v9.0.0. Released v9.0.0.
% 0.04/0.14 % 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.35 % Computer : n010.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Apr 9 02:31:03 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.78/2.01 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.78/2.01
% 3.78/2.01 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------