%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ARI671_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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n020.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:48 PM UTC 2025
% Result : Unsatisfiable 120.60s 62.51s
% Output : CNFRefutation 120.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 7
% Syntax : Number of formulae : 93 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 153 ( 95 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 127 ( 67 ~; 57 |; 1 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 499 ( 51 atm; 221 fun; 167 num; 60 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 : 9 ( 1 usr; 6 con; 0-2 aty)
% Number of variables : 60 ( 60 !; 0 ?; 60 :)
% Comments :
%------------------------------------------------------------------------------
%$ #nlpp
%Foreground sorts:
%Background operators:
tff(a,type,
a: $int ).
%Foreground operators:
tff(f_49,axiom,
! [A: $int,B: $int] : ( $product(A,B) = $product(B,A) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',mult_comm) ).
tff(f_30,axiom,
$product(a,a) = 2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj) ).
tff(f_51,axiom,
! [A: $int,B: $int,C: $int] : ( $product(A,$sum(B,C)) = $sum($product(A,B),$product(A,C)) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',mult_dist) ).
tff(f_65,axiom,
! [C: $int,B: $int] :
( ( $product(C,B) = C )
<=> ( ( C = 0 )
| ( B = 1 ) ) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',mult_cancel_right1) ).
tff(f_46,axiom,
! [M: $int,N: $int] : ( $product($sum(1,M),N) = $sum(N,$product(M,N)) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',mult_def_2) ).
tff(f_74,axiom,
! [A: $int,B: $int] :
( ( $less(0,A)
& $less(0,B) )
=> $less(0,$product(A,B)) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',mult_nonneg_nonneg) ).
tff(f_57,axiom,
! [A: $int,B: $int] : ( $uminus($product(A,B)) = $product($uminus(A),B) ),
file('/export/starexec/sandbox2/solver/bin/lemmas/mult_lemmas.p',minus_mult_left) ).
tff(c_39,plain,
! [B_7: $int,A_8: $int] : ( $product(B_7,A_8) = $product(A_8,B_7) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_47,plain,
$product(a,a) = 2,
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_10,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_51]) ).
tff(c_38,plain,
! [A_12: $int,X_34: $int,B_13: $int,C_14: $int] :
( ( $product(A_12,X_34) = $sum($product(A_12,B_13),$product(A_12,C_14)) )
| ( X_34 != $sum(B_13,C_14) ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_10]) ).
tff(c_137,plain,
! [X_34: $int,C_14: $int] :
( ( $product(a,X_34) = $sum(2,$product(a,C_14)) )
| ( X_34 != $sum(a,C_14) ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_38]) ).
tff(c_9789,plain,
! [C_1168: $int,X_1170: $int] :
( ( $sum(2,$product(a,C_1168)) = $product(a,X_1170) )
| ( X_1170 != $sum(C_1168,a) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_137]) ).
tff(c_32,plain,
! [C_23: $int] : ( $product(C_23,1) = C_23 ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_10137,plain,
! [C_1168: $int] :
( ( $sum(2,$product(a,C_1168)) = a )
| ( $sum(C_1168,a) != 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9789,c_32]) ).
tff(c_17915,plain,
$product(a,$sum(1,$uminus(a))) = $sum($uminus(2),a),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_10137]) ).
tff(c_41,plain,
! [X_35: $int,N_4: $int,M_3: $int] :
( ( $product(X_35,N_4) = $sum(N_4,$product(M_3,N_4)) )
| ( X_35 != $sum(1,M_3) ) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_18311,plain,
$product($sum(1,a),$sum(1,$uminus(a))) = $sum($sum(1,$uminus(a)),$sum($uminus(2),a)),
inference(superposition,[status(thm),theory(equality)],[c_17915,c_41]) ).
tff(c_365582,plain,
$product($sum(1,a),$sum(1,$uminus(a))) = $uminus(1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_18311]) ).
tff(c_368491,plain,
$product($sum(1,$uminus(a)),$sum(1,a)) = $uminus(1),
inference(superposition,[status(thm),theory(equality)],[c_39,c_365582]) ).
tff(c_370803,plain,
$product($sum(1,$sum(1,$uminus(a))),$sum(1,a)) = $sum($sum(1,a),$uminus(1)),
inference(superposition,[status(thm),theory(equality)],[c_368491,c_41]) ).
tff(c_371562,plain,
$product($sum(2,$uminus(a)),$sum(1,a)) = a,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_370803]) ).
tff(c_374595,plain,
$product($sum(1,a),$sum(2,$uminus(a))) = a,
inference(superposition,[status(thm),theory(equality)],[c_39,c_371562]) ).
tff(c_376887,plain,
$product($sum(1,$sum(1,a)),$sum(2,$uminus(a))) = $sum($sum(2,$uminus(a)),a),
inference(superposition,[status(thm),theory(equality)],[c_374595,c_41]) ).
tff(c_377603,plain,
$product($sum(2,a),$sum(2,$uminus(a))) = 2,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_376887]) ).
tff(c_380474,plain,
$product($sum(2,$uminus(a)),$sum(2,a)) = 2,
inference(superposition,[status(thm),theory(equality)],[c_39,c_377603]) ).
tff(c_382787,plain,
$product($sum(1,$sum(2,$uminus(a))),$sum(2,a)) = $sum($sum(2,a),2),
inference(superposition,[status(thm),theory(equality)],[c_380474,c_41]) ).
tff(c_506585,plain,
$product($sum(3,$uminus(a)),$sum(2,a)) = $sum(4,a),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_382787]) ).
tff(c_30,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_74]) ).
tff(c_509375,plain,
( $less(0,$sum(4,a))
| ~ $less(0,$sum(3,$uminus(a)))
| ~ $less(0,$sum(2,a)) ),
inference(superposition,[status(thm),theory(equality)],[c_506585,c_30]) ).
tff(c_509377,plain,
( $less($uminus(4),a)
| ~ $less(a,3)
| ~ $less($uminus(2),a) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_509375]) ).
tff(c_513566,plain,
~ $less($uminus(2),a),
inference(splitLeft,[status(thm)],[c_509377]) ).
tff(c_34,plain,
! [A_17: $int,B_18: $int,X_33: $int] :
( ( $uminus($product(A_17,B_18)) = $product(X_33,B_18) )
| ( X_33 != $uminus(A_17) ) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_36,plain,
! [X_33: $int,B_18: $int,A_17: $int] :
( ( $uminus($product(X_33,B_18)) = $product(A_17,B_18) )
| ( X_33 != $uminus(A_17) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_34]) ).
tff(c_145,plain,
! [A_17: $int] :
( ( $product(A_17,a) = $uminus(2) )
| ( a != $uminus(A_17) ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_36]) ).
tff(c_530,plain,
! [A_120: $int] :
( ( $product(A_120,a) = $uminus(2) )
| ( a != $uminus(A_120) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_145]) ).
tff(c_677,plain,
! [A_120: $int] :
( $less(0,$uminus(2))
| ~ $less(0,A_120)
| ~ $less(0,a)
| ( a != $uminus(A_120) ) ),
inference(superposition,[status(thm),theory(equality)],[c_530,c_30]) ).
tff(c_679,plain,
! [A_120: $int] :
( ~ $less(0,A_120)
| ~ $less(0,a)
| ( a != $uminus(A_120) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_677]) ).
tff(c_1400,plain,
~ $less(0,a),
inference(splitLeft,[status(thm)],[c_679]) ).
tff(c_77,plain,
$uminus($product($uminus(a),a)) = 2,
inference(superposition,[status(thm),theory(equality)],[c_47,c_36]) ).
tff(c_152,plain,
$uminus($product(a,$uminus(a))) = 2,
inference(demodulation,[status(thm),theory(equality)],[c_39,c_77]) ).
tff(c_201,plain,
$product(a,$uminus(a)) = $uminus(2),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_152]) ).
tff(c_325,plain,
( $less(0,$uminus(2))
| ~ $less(0,a)
| ~ $less(0,$uminus(a)) ),
inference(superposition,[status(thm),theory(equality)],[c_201,c_30]) ).
tff(c_327,plain,
( ~ $less(0,a)
| ~ $less(a,0) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_325]) ).
tff(c_717,plain,
~ $less(a,0),
inference(splitLeft,[status(thm)],[c_327]) ).
tff(c_31,plain,
! [B_24: $int] : ( $product(0,B_24) = 0 ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_161,plain,
( ( 2 = 0 )
| ( a != 0 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_31]) ).
tff(c_163,plain,
a != 0,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_161]) ).
tff(c_1401,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_1400,c_717,c_163]) ).
tff(c_1405,plain,
$less(0,a),
inference(splitRight,[status(thm)],[c_679]) ).
tff(c_170,plain,
! [M_3: $int] :
( ( $sum(a,$product(M_3,a)) = 2 )
| ( a != $sum(1,M_3) ) ),
inference(superposition,[status(thm),theory(equality)],[c_41,c_47]) ).
tff(c_1159,plain,
! [M_208: $int] :
( ( $product(M_208,a) = $sum(2,$uminus(a)) )
| ( a != $sum(1,M_208) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_170]) ).
tff(c_1339,plain,
! [M_208: $int] :
( $less(0,$sum(2,$uminus(a)))
| ~ $less(0,M_208)
| ~ $less(0,a)
| ( a != $sum(1,M_208) ) ),
inference(superposition,[status(thm),theory(equality)],[c_1159,c_30]) ).
tff(c_1341,plain,
! [M_208: $int] :
( $less(a,2)
| ~ $less(0,M_208)
| ~ $less(0,a)
| ( a != $sum(1,M_208) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1339]) ).
tff(c_8196,plain,
! [M_208: $int] :
( $less(a,2)
| ~ $less(0,M_208)
| ( a != $sum(1,M_208) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1405,c_1341]) ).
tff(c_8198,plain,
! [M_208: $int] :
( ~ $less(0,M_208)
| ( a != $sum(1,M_208) ) ),
inference(splitLeft,[status(thm)],[c_8196]) ).
tff(c_8201,plain,
$lesseq(a,1),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_8198]) ).
tff(c_8203,plain,
~ $less(1,a),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_8201]) ).
tff(c_33,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_65]) ).
tff(c_156,plain,
( ( 2 = 0 )
| ( a = 1 )
| ( a != 2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_33]) ).
tff(c_158,plain,
( ( a = 1 )
| ( a != 2 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_156]) ).
tff(c_195,plain,
a != 2,
inference(splitLeft,[status(thm)],[c_158]) ).
tff(c_160,plain,
( ( a = 2 )
| ( a != 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47,c_32]) ).
tff(c_197,plain,
a != 1,
inference(negUnitSimplification,[status(thm)],[c_195,c_160]) ).
tff(c_8204,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_8203,c_717,c_197,c_163]) ).
tff(c_8206,plain,
$less(a,2),
inference(splitRight,[status(thm)],[c_8196]) ).
tff(c_8207,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_8206,c_717,c_197,c_163]) ).
tff(c_8211,plain,
$less(a,0),
inference(splitRight,[status(thm)],[c_327]) ).
tff(c_348,plain,
$uminus($product($uminus(a),$uminus(a))) = $uminus(2),
inference(superposition,[status(thm),theory(equality)],[c_36,c_201]) ).
tff(c_12842,plain,
$product($uminus(a),$uminus(a)) = 2,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_348]) ).
tff(c_13235,plain,
! [M_3: $int] :
( ( $sum($uminus(a),$product(M_3,$uminus(a))) = 2 )
| ( $uminus(a) != $sum(1,M_3) ) ),
inference(superposition,[status(thm),theory(equality)],[c_41,c_12842]) ).
tff(c_437685,plain,
! [M_116330: $int] :
( ( $product(M_116330,$uminus(a)) = $sum(2,a) )
| ( a != $sum($uminus(1),$uminus(M_116330)) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_13235]) ).
tff(c_440282,plain,
! [M_116330: $int] :
( $less(0,$sum(2,a))
| ~ $less(0,M_116330)
| ~ $less(0,$uminus(a))
| ( a != $sum($uminus(1),$uminus(M_116330)) ) ),
inference(superposition,[status(thm),theory(equality)],[c_437685,c_30]) ).
tff(c_440284,plain,
! [M_116330: $int] :
( $less($uminus(2),a)
| ~ $less(0,M_116330)
| ~ $less(a,0)
| ( a != $sum($uminus(1),$uminus(M_116330)) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_440282]) ).
tff(c_588356,plain,
! [M_116330: $int] :
( $less($uminus(2),a)
| ~ $less(0,M_116330)
| ( a != $sum($uminus(1),$uminus(M_116330)) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_8211,c_440284]) ).
tff(c_588358,plain,
! [M_116330: $int] :
( ~ $less(0,M_116330)
| ( a != $sum($uminus(1),$uminus(M_116330)) ) ),
inference(negUnitSimplification,[status(thm)],[c_513566,c_588356]) ).
tff(c_588359,plain,
$lesseq(0,$sum(1,a)),
inference(quantifierElimination,[status(thm),theory('LIA')],[c_588358]) ).
tff(c_588361,plain,
~ $less(a,$uminus(1)),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_588359]) ).
tff(c_588362,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_588361,c_513566]) ).
tff(c_588366,plain,
$less($uminus(2),a),
inference(splitRight,[status(thm)],[c_509377]) ).
tff(c_321,plain,
( ( a = $uminus(2) )
| ( $uminus(a) != 1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_201,c_32]) ).
tff(c_323,plain,
( ( a = $uminus(2) )
| ( a != $uminus(1) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_321]) ).
tff(c_8214,plain,
a != $uminus(1),
inference(splitLeft,[status(thm)],[c_323]) ).
tff(c_588367,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_588366,c_8214,c_8211]) ).
tff(c_588370,plain,
a = $uminus(2),
inference(splitRight,[status(thm)],[c_323]) ).
tff(c_148,plain,
! [A_17: $int] :
( ( $product(A_17,a) = $uminus(2) )
| ( a != $uminus(A_17) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_145]) ).
tff(c_588378,plain,
! [A_17: $int] :
( ( $product(A_17,$uminus(2)) = $uminus(2) )
| ( $uminus(A_17) != $uminus(2) ) ),
inference(demodulation,[status(thm),theory(equality)],[c_588370,c_588370,c_148]) ).
tff(c_588380,plain,
2 = 1,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_588378]) ).
tff(c_588399,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_588380]) ).
tff(c_588402,plain,
a = 1,
inference(splitRight,[status(thm)],[c_158]) ).
tff(c_29,plain,
$product(a,a) = 2,
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_588405,plain,
$product(1,1) = 2,
inference(demodulation,[status(thm),theory(equality)],[c_588402,c_588402,c_29]) ).
tff(c_588414,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_588405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ARI671_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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 15:15:49 EDT 2025
% 0.12/0.34 % CPUTime :
% 120.60/62.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.60/62.53
% 120.60/62.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------