%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWC448_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:28 PM UTC 2025
% Result : Theorem 3.69s 1.96s
% Output : CNFRefutation 3.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 41 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 60 ( 41 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 36 ( 17 ~; 15 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number arithmetic : 214 ( 18 atm; 70 fun; 88 num; 38 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 : 23 ( 9 usr; 13 con; 0-2 aty)
% Number of variables : 38 ( 37 !; 1 ?; 38 :)
% 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) = $product(2,$sum($product(2,$sum(2,$sum(Xa,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_55,axiom,
! [Xa: $int] : ( small(Xa) = $difference(v0(Xa),1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_6) ).
tff(f_52,axiom,
! [Xa: $int] : ( v0(Xa) = u0(g0,h0(Xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_5) ).
tff(f_59,axiom,
! [Xa: $int] : ( fast(Xa) = $sum(2,$product($sum(1,$sum(2,2)),$sum(1,$product(2,$product(2,$sum($product(2,$sum(2,$sum(Xa,Xa))),Xa)))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_7) ).
tff(f_67,negated_conjecture,
~ ~ ? [Ca: $int] :
( $greatereq(Ca,0)
& ( small(Ca) != fast(Ca) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
tff(c_2,plain,
! [X_1a: $int] : ( f0(X_1a) = $product(2,$sum(4,$product(5,X_1a))) ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_41,plain,
! [X_1a: $int] : ( f0(X_1a) = $sum(8,$product(10,X_1a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_2]) ).
tff(c_7,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_38,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_7]) ).
tff(c_9,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_171,plain,
! [X_32a: $int,Y_33a: $int] :
( ( f0(u0($sum($uminus(1),X_32a),Y_33a)) = u0(X_32a,Y_33a) )
| ~ $less(0,X_32a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_9]) ).
tff(c_202,plain,
! [X_32a: $int,Y_4a: $int] :
( ( u0(X_32a,Y_4a) = f0(Y_4a) )
| ~ $less(0,X_32a)
| $less(0,$sum($uminus(1),X_32a)) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_171]) ).
tff(c_241,plain,
! [X_32a: $int,Y_4a: $int] :
( ( u0(X_32a,Y_4a) = $sum(8,$product(10,Y_4a)) )
| ~ $less(0,X_32a)
| $less(0,$sum($uminus(1),X_32a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_41,c_202]) ).
tff(c_458,plain,
! [X_42a: $int,Y_43a: $int] :
( ( u0(X_42a,Y_43a) = $sum(8,$product(10,Y_43a)) )
| ~ $less(0,X_42a)
| $less(1,X_42a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_241]) ).
tff(c_40,plain,
g0 = 2,
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_39,plain,
! [X_2a: $int] : ( h0(X_2a) = X_2a ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_14,plain,
! [X_6a: $int] : ( $difference(v0(X_6a),1) = small(X_6a) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_29,plain,
! [X_6a: $int] : ( v0(X_6a) = $sum(1,small(X_6a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_14]) ).
tff(c_33,plain,
! [X_5a: $int] : ( u0(g0,h0(X_5a)) = v0(X_5a) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_56,plain,
! [X_5a: $int] : ( u0(g0,h0(X_5a)) = $sum(1,small(X_5a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_29,c_33]) ).
tff(c_65,plain,
! [X_5a: $int] : ( u0(g0,X_5a) = $sum(1,small(X_5a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_39,c_56]) ).
tff(c_69,plain,
! [X_5a: $int] : ( u0(2,X_5a) = $sum(1,small(X_5a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_65]) ).
tff(c_223,plain,
! [Y_33a: $int] :
( ( f0(u0($sum($uminus(1),2),Y_33a)) = $sum(1,small(Y_33a)) )
| ~ $less(0,2) ),
inference(superposition,[status(thm),theory(equality)],[c_171,c_69]) ).
tff(c_225,plain,
! [Y_33a: $int] : ( f0(u0(1,Y_33a)) = $sum(1,small(Y_33a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_223]) ).
tff(c_483,plain,
! [Y_43a: $int] :
( ( $sum(1,small(Y_43a)) = f0($sum(8,$product(10,Y_43a))) )
| ~ $less(0,1)
| $less(1,1) ),
inference(superposition,[status(thm),theory(equality)],[c_458,c_225]) ).
tff(c_532,plain,
! [Y_43a: $int] :
( ( $sum(1,small(Y_43a)) = $sum(8,$product(10,$sum(8,$product(10,Y_43a)))) )
| ~ $less(0,1)
| $less(1,1) ),
inference(demodulation,[status(thm),theory(equality)],[c_41,c_483]) ).
tff(c_857,plain,
! [Y_66a: $int] : ( small(Y_66a) = $sum(87,$product(100,Y_66a)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_532]) ).
tff(c_17,plain,
! [X_7a: $int] : ( fast(X_7a) = $sum(2,$sum(85,$product(100,X_7a))) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_28,plain,
! [X_7a: $int] : ( fast(X_7a) = $sum(87,$product(100,X_7a)) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_17]) ).
tff(c_27,plain,
small('#skF_1') != fast('#skF_1'),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_48,plain,
small('#skF_1') != $sum(87,$product(100,'#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_27]) ).
tff(c_153,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_48]) ).
tff(c_873,plain,
$sum(87,$product(100,'#skF_1')) = '#skE_1',
inference(superposition,[status(thm),theory(equality)],[c_857,c_153]) ).
tff(c_147,plain,
small('#skF_1') = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_48]) ).
tff(c_50,plain,
small('#skF_1') != $sum(87,$product(100,'#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_28,c_27]) ).
tff(c_149,plain,
$sum(87,$product(100,'#skF_1')) != '#skE_1',
inference(demodulation,[status(thm),theory(equality)],[c_147,c_50]) ).
tff(c_155,plain,
$product(100,'#skF_1') != $sum($uminus(87),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_149]) ).
tff(c_878,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_873,c_155]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.12 % Problem : SWC448_1 : TPTP v9.0.0. Released v9.0.0.
% 0.13/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 : n010.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.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 02:31:33 EDT 2025
% 0.14/0.35 % CPUTime :
% 3.69/1.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.69/1.96
% 3.69/1.96 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------