%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM925+7 : TPTP v9.0.0. Released v5.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 : n029.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 07:57:37 PM UTC 2025
% Result : Theorem 151.85s 117.42s
% Output : CNFRefutation 151.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 22
% Syntax : Number of formulae : 71 ( 58 unt; 0 typ; 0 def)
% Number of atoms : 91 ( 67 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 39 ( 19 ~; 13 |; 1 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 61 ( 59 usr; 1 prp; 0-2 aty)
% Number of functors : 86 ( 86 usr; 31 con; 0-4 aty)
% Number of variables : 48 ( 48 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ zero_neq_one > zero > semiring_char_0 > semiring_1 > semiring_0 > semiring > semiri456707255roduct > ring_n68954251visors > ring_char_0 > ring_11004092258visors > ring_1 > ring > power > ordered_semiring > ordered_ring_abs > ordered_ring > ordered_ab_group_add > ordere779506340up_add > ordere453448008miring > ordere236663937imp_le > ordere223160158up_add > ordere216010020id_add > ordere1490568538miring > ordere142940540dd_abs > order > one > number_semiring > number_ring > number > no_zero_divisors > mult_zero > monoid_mult > monoid_add > linordered_semiring > linordered_semidom > linordered_ring > linordered_idom > linorder > linord893533164strict > linord626643107strict > linord581940658strict > linord219039673up_add > linord20386208strict > linord1278240602ring_1 > idom > hBOOL > group_add > dvd > comm_semiring_1 > comm_semiring > comm_ring_1 > comm_ring > comm_monoid_mult > comm_monoid_add > cancel_semigroup_add > cancel146912293up_add > ab_semigroup_mult > ab_semigroup_add > ab_group_add > if > hAPP > times_times > plus_plus > minus_minus > zcong > ti > power_power > number_number_of > legendre > fun > abs_abs > #nlpp > zero_zero > undefined > succ > semiring_1_of_nat > quadRes > ord_less_eq > ord_less > one_one > nat_1 > dvd_dvd > bit1 > bit0 > zprime > y > x > twoSqu658283162sum2sq > tn > t > s1 > s > real > pls > nat > n > min > m1 > m > int > fTrue > fFalse > bool > #skF_9 > #skF_33 > #skF_7 > #skF_22 > #skF_31 > #skF_1 > #skF_20 > #skF_2 > #skF_18 > #skF_17 > #skF_25 > #skF_8 > #skF_19 > #skF_38 > #skF_3 > #skF_39 > #skF_14 > #skF_29 > #skF_26 > #skF_30 > #skF_10 > #skF_37 > #skF_21 > #skF_36 > #skF_32 > #skF_43 > #skF_15 > #skF_40 > #skF_13 > #skF_11 > #skF_35 > #skF_24 > #skF_23 > #skF_12 > #skF_41 > #skF_27 > #skF_5 > #skF_28 > #skF_6 > #skF_4 > #skF_42 > #skF_16 > #skF_34
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(linord1278240602ring_1,type,
linord1278240602ring_1: $i > $o ).
tff(tn,type,
tn: $i ).
tff('#skF_9',type,
'#skF_9': $i > $i ).
tff(hAPP,type,
hAPP: ( $i * $i * $i * $i ) > $i ).
tff(ordered_semiring,type,
ordered_semiring: $i > $o ).
tff(zcong,type,
zcong: ( $i * $i ) > $i ).
tff(semiring_1,type,
semiring_1: $i > $o ).
tff('#skF_33',type,
'#skF_33': $i ).
tff(ab_semigroup_mult,type,
ab_semigroup_mult: $i > $o ).
tff(power,type,
power: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i > $i ).
tff(semiri456707255roduct,type,
semiri456707255roduct: $i > $o ).
tff(comm_semiring,type,
comm_semiring: $i > $o ).
tff(m,type,
m: $i ).
tff(ord_less_eq,type,
ord_less_eq: $i > $i ).
tff('#skF_22',type,
'#skF_22': ( $i * $i ) > $i ).
tff(s1,type,
s1: $i ).
tff('#skF_31',type,
'#skF_31': ( $i * $i * $i ) > $i ).
tff(group_add,type,
group_add: $i > $o ).
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i ) > $i ).
tff(idom,type,
idom: $i > $o ).
tff(ring_n68954251visors,type,
ring_n68954251visors: $i > $o ).
tff('#skF_20',type,
'#skF_20': $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff(linord581940658strict,type,
linord581940658strict: $i > $o ).
tff('#skF_18',type,
'#skF_18': $i ).
tff(min,type,
min: $i ).
tff(one_one,type,
one_one: $i > $i ).
tff(ring_1,type,
ring_1: $i > $o ).
tff(number,type,
number: $i > $o ).
tff(t,type,
t: $i ).
tff(pls,type,
pls: $i ).
tff(monoid_add,type,
monoid_add: $i > $o ).
tff(x,type,
x: $i ).
tff(linordered_ring,type,
linordered_ring: $i > $o ).
tff(ring_11004092258visors,type,
ring_11004092258visors: $i > $o ).
tff(linordered_semidom,type,
linordered_semidom: $i > $o ).
tff(ab_semigroup_add,type,
ab_semigroup_add: $i > $o ).
tff('#skF_17',type,
'#skF_17': ( $i * $i ) > $i ).
tff('#skF_25',type,
'#skF_25': $i ).
tff(twoSqu658283162sum2sq,type,
twoSqu658283162sum2sq: $i ).
tff(bit0,type,
bit0: $i > $i ).
tff(no_zero_divisors,type,
no_zero_divisors: $i > $o ).
tff(plus_plus,type,
plus_plus: ( $i * $i * $i ) > $i ).
tff(s,type,
s: $i ).
tff(linord626643107strict,type,
linord626643107strict: $i > $o ).
tff(zero_neq_one,type,
zero_neq_one: $i > $o ).
tff('#skF_8',type,
'#skF_8': $i > $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff('#skF_38',type,
'#skF_38': ( $i * $i ) > $i ).
tff(bool,type,
bool: $i ).
tff(minus_minus,type,
minus_minus: ( $i * $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff('#skF_39',type,
'#skF_39': ( $i * $i * $i ) > $i ).
tff(number_ring,type,
number_ring: $i > $o ).
tff(ordere142940540dd_abs,type,
ordere142940540dd_abs: $i > $o ).
tff(comm_monoid_mult,type,
comm_monoid_mult: $i > $o ).
tff(comm_ring_1,type,
comm_ring_1: $i > $o ).
tff(linord219039673up_add,type,
linord219039673up_add: $i > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff(semiring_1_of_nat,type,
semiring_1_of_nat: $i > $i ).
tff(nat,type,
nat: $i ).
tff('#skF_29',type,
'#skF_29': $i > $i ).
tff(fun,type,
fun: ( $i * $i ) > $i ).
tff('#skF_26',type,
'#skF_26': $i ).
tff(ordered_ring_abs,type,
ordered_ring_abs: $i > $o ).
tff(ordere779506340up_add,type,
ordere779506340up_add: $i > $o ).
tff('#skF_30',type,
'#skF_30': ( $i * $i * $i ) > $i ).
tff(quadRes,type,
quadRes: $i > $i ).
tff(y,type,
y: $i ).
tff(linordered_semiring,type,
linordered_semiring: $i > $o ).
tff(dvd_dvd,type,
dvd_dvd: $i > $i ).
tff(ordered_ring,type,
ordered_ring: $i > $o ).
tff('#skF_10',type,
'#skF_10': $i > $i ).
tff(if,type,
if: ( $i * $i * $i * $i ) > $i ).
tff(ordere1490568538miring,type,
ordere1490568538miring: $i > $o ).
tff(ordere236663937imp_le,type,
ordere236663937imp_le: $i > $o ).
tff(cancel146912293up_add,type,
cancel146912293up_add: $i > $o ).
tff(undefined,type,
undefined: $i > $i ).
tff('#skF_37',type,
'#skF_37': ( $i * $i * $i ) > $i ).
tff(comm_monoid_add,type,
comm_monoid_add: $i > $o ).
tff(ordere223160158up_add,type,
ordere223160158up_add: $i > $o ).
tff(comm_semiring_1,type,
comm_semiring_1: $i > $o ).
tff('#skF_21',type,
'#skF_21': $i ).
tff(zprime,type,
zprime: $i ).
tff('#skF_36',type,
'#skF_36': ( $i * $i ) > $i ).
tff(comm_ring,type,
comm_ring: $i > $o ).
tff('#skF_32',type,
'#skF_32': $i ).
tff('#skF_43',type,
'#skF_43': ( $i * $i * $i ) > $i ).
tff(ordered_ab_group_add,type,
ordered_ab_group_add: $i > $o ).
tff(ring,type,
ring: $i > $o ).
tff(int,type,
int: $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i * $i ) > $i ).
tff('#skF_40',type,
'#skF_40': ( $i * $i * $i ) > $i ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff(ti,type,
ti: ( $i * $i ) > $i ).
tff(semiring_0,type,
semiring_0: $i > $o ).
tff(n,type,
n: $i ).
tff(fTrue,type,
fTrue: $i ).
tff(linord20386208strict,type,
linord20386208strict: $i > $o ).
tff(linordered_idom,type,
linordered_idom: $i > $o ).
tff(nat_1,type,
nat_1: $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(bit1,type,
bit1: $i > $i ).
tff(ab_group_add,type,
ab_group_add: $i > $o ).
tff(ordere216010020id_add,type,
ordere216010020id_add: $i > $o ).
tff(ordere453448008miring,type,
ordere453448008miring: $i > $o ).
tff(hBOOL,type,
hBOOL: $i > $o ).
tff(mult_zero,type,
mult_zero: $i > $o ).
tff(legendre,type,
legendre: ( $i * $i ) > $i ).
tff(number_number_of,type,
number_number_of: ( $i * $i ) > $i ).
tff('#skF_35',type,
'#skF_35': $i ).
tff(cancel_semigroup_add,type,
cancel_semigroup_add: $i > $o ).
tff('#skF_24',type,
'#skF_24': $i ).
tff(ring_char_0,type,
ring_char_0: $i > $o ).
tff(power_power,type,
power_power: ( $i * $i ) > $i ).
tff('#skF_23',type,
'#skF_23': $i ).
tff(semiring_char_0,type,
semiring_char_0: $i > $o ).
tff(times_times,type,
times_times: ( $i * $i * $i ) > $i ).
tff(zero_zero,type,
zero_zero: $i > $i ).
tff(number_semiring,type,
number_semiring: $i > $o ).
tff(monoid_mult,type,
monoid_mult: $i > $o ).
tff(ord_less,type,
ord_less: $i > $i ).
tff('#skF_12',type,
'#skF_12': $i > $i ).
tff('#skF_41',type,
'#skF_41': ( $i * $i * $i ) > $i ).
tff(real,type,
real: $i ).
tff(one,type,
one: $i > $o ).
tff('#skF_27',type,
'#skF_27': ( $i * $i ) > $i ).
tff(semiring,type,
semiring: $i > $o ).
tff(fFalse,type,
fFalse: $i ).
tff(succ,type,
succ: $i > $i ).
tff(order,type,
order: $i > $o ).
tff(dvd,type,
dvd: $i > $o ).
tff(m1,type,
m1: $i ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_28',type,
'#skF_28': ( $i * $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(zero,type,
zero: $i > $o ).
tff(linord893533164strict,type,
linord893533164strict: $i > $o ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_42',type,
'#skF_42': ( $i * $i * $i ) > $i ).
tff('#skF_16',type,
'#skF_16': ( $i * $i * $i ) > $i ).
tff('#skF_34',type,
'#skF_34': $i ).
tff(abs_abs,type,
abs_abs: ( $i * $i ) > $i ).
tff(linorder,type,
linorder: $i > $o ).
tff(f_3795,axiom,
! [Ma,Na] :
( hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),Ma),Na))
<=> ( hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less_eq(nat),Ma),Na))
& ( Ma != Na ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_609_nat__less__le) ).
tff(f_2298,axiom,
! [N] : ( nat_1(hAPP(nat,int,semiring_1_of_nat(int),N)) = N ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_346_nat__int) ).
tff(f_6044,axiom,
ring_11004092258visors(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring__1__no__zero__divisors) ).
tff(f_623,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_Pls__def) ).
tff(f_213,axiom,
! [B_1_1] : ( ti(int,succ(B_1_1)) = succ(B_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_Osucc_res) ).
tff(f_195,hypothesis,
! [B_1_1] : ( ti(int,bit1(B_1_1)) = bit1(B_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OBit1_res) ).
tff(f_841,axiom,
! [K_1] : ( number_number_of(int,K_1) = ti(int,K_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_number__of__is__id) ).
tff(f_471,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_one__is__num__one) ).
tff(f_3349,axiom,
! [K_1] : ( succ(K_1) = plus_plus(int,K_1,one_one(int)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_519_succ__def) ).
tff(f_510,axiom,
! [Z,W] : ( plus_plus(int,Z,W) = plus_plus(int,W,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_zadd__commute) ).
tff(f_2802,axiom,
! [V_1] : ( number_number_of(nat,V_1) = nat_1(number_number_of(int,V_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_427_nat__number__of__def) ).
tff(f_199,axiom,
! [B_1_1] : ( nat_1(ti(int,B_1_1)) = nat_1(B_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_Onat_arg1) ).
tff(f_6201,negated_conjecture,
~ ( ( hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f_1073,axiom,
! [X_a] :
( ring_11004092258visors(X_a)
=> ! [N,A_1] :
( ( ti(X_a,A_1) != zero_zero(X_a) )
=> ( hAPP(nat,X_a,power_power(X_a,A_1),N) != zero_zero(X_a) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_field__power__not__zero) ).
tff(f_6067,axiom,
ab_group_add(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Oab__group__add) ).
tff(f_196,axiom,
ti(int,min) = min,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OMin_res) ).
tff(f_4597,axiom,
! [K_1] : ( minus_minus(int,K_1,min) = succ(K_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_777_diff__bin__simps_I2_J) ).
tff(f_2154,axiom,
! [X_a] :
( ab_group_add(X_a)
=> ! [A_2,B] :
( ( ti(X_a,A_2) = ti(X_a,B) )
<=> ( minus_minus(X_a,A_2,B) = zero_zero(X_a) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_321_eq__iff__diff__eq__0) ).
tff(f_4523,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min),pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_758_rel__simps_I23_J) ).
tff(f_2640,axiom,
nat_1(zero_zero(int)) = zero_zero(nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_408_nat__0) ).
tff(f_2112,axiom,
! [I_1] :
( ( nat_1(I_1) = zero_zero(nat) )
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),I_1),zero_zero(int))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_315_nat__0__iff) ).
tff(f_393,axiom,
hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_n0) ).
tff(c_1978,plain,
! [Na_2335] : ~ hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),Na_2335),Na_2335)),
inference(cnfTransformation,[status(thm)],[f_3795]) ).
tff(c_1202,plain,
! [N_1455] : ( nat_1(hAPP(nat,int,semiring_1_of_nat(int),N_1455)) = N_1455 ),
inference(cnfTransformation,[status(thm)],[f_2298]) ).
tff(c_3211,plain,
ring_11004092258visors(int),
inference(cnfTransformation,[status(thm)],[f_6044]) ).
tff(c_417,plain,
zero_zero(int) = pls,
inference(cnfTransformation,[status(thm)],[f_623]) ).
tff(c_116,plain,
! [B_1_1_137] : ( ti(int,succ(B_1_1_137)) = succ(B_1_1_137) ),
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_4544,plain,
! [B_1_1_3465] : ( ti(int,bit1(B_1_1_3465)) = bit1(B_1_1_3465) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_533,plain,
! [K_1_425] : ( ti(int,K_1_425) = number_number_of(int,K_1_425) ),
inference(cnfTransformation,[status(thm)],[f_841]) ).
tff(c_4550,plain,
! [B_1_1_3465] : ( number_number_of(int,bit1(B_1_1_3465)) = bit1(B_1_1_3465) ),
inference(superposition,[status(thm),theory(equality)],[c_4544,c_533]) ).
tff(c_298,plain,
number_number_of(int,bit1(pls)) = one_one(int),
inference(cnfTransformation,[status(thm)],[f_471]) ).
tff(c_5102,plain,
one_one(int) = bit1(pls),
inference(demodulation,[status(thm),theory(equality)],[c_4550,c_298]) ).
tff(c_1730,plain,
! [K_1_2111] : ( plus_plus(int,K_1_2111,one_one(int)) = succ(K_1_2111) ),
inference(cnfTransformation,[status(thm)],[f_3349]) ).
tff(c_5303,plain,
! [K_1_2111] : ( plus_plus(int,K_1_2111,bit1(pls)) = succ(K_1_2111) ),
inference(demodulation,[status(thm),theory(equality)],[c_5102,c_1730]) ).
tff(c_6400,plain,
! [Z_3515,W_3516] : ( plus_plus(int,Z_3515,W_3516) = plus_plus(int,W_3516,Z_3515) ),
inference(cnfTransformation,[status(thm)],[f_510]) ).
tff(c_6457,plain,
! [K_1_2111] : ( plus_plus(int,bit1(pls),K_1_2111) = succ(K_1_2111) ),
inference(superposition,[status(thm),theory(equality)],[c_5303,c_6400]) ).
tff(c_1448,plain,
! [V_1_1778] : ( nat_1(number_number_of(int,V_1_1778)) = number_number_of(nat,V_1_1778) ),
inference(cnfTransformation,[status(thm)],[f_2802]) ).
tff(c_106,plain,
! [B_1_1_130] : ( nat_1(ti(int,B_1_1_130)) = nat_1(B_1_1_130) ),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_4047,plain,
! [B_1_1_130] : ( number_number_of(nat,B_1_1_130) = nat_1(B_1_1_130) ),
inference(demodulation,[status(thm),theory(equality)],[c_1448,c_533,c_106]) ).
tff(c_3505,plain,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(cnfTransformation,[status(thm)],[f_6201]) ).
tff(c_3749,plain,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) = pls,
inference(demodulation,[status(thm),theory(equality)],[c_417,c_3505]) ).
tff(c_4126,plain,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),nat_1(bit0(bit1(pls)))) = pls,
inference(demodulation,[status(thm),theory(equality)],[c_4047,c_3749]) ).
tff(c_5175,plain,
hAPP(nat,int,power_power(int,plus_plus(int,bit1(pls),hAPP(nat,int,semiring_1_of_nat(int),n))),nat_1(bit0(bit1(pls)))) = pls,
inference(demodulation,[status(thm),theory(equality)],[c_5102,c_4126]) ).
tff(c_7190,plain,
hAPP(nat,int,power_power(int,succ(hAPP(nat,int,semiring_1_of_nat(int),n))),nat_1(bit0(bit1(pls)))) = pls,
inference(demodulation,[status(thm),theory(equality)],[c_6457,c_5175]) ).
tff(c_392156,plain,
! [X_a_356970,A_1_356971,N_356972] :
( ( hAPP(nat,X_a_356970,power_power(X_a_356970,A_1_356971),N_356972) != zero_zero(X_a_356970) )
| ( ti(X_a_356970,A_1_356971) = zero_zero(X_a_356970) )
| ~ ring_11004092258visors(X_a_356970) ),
inference(cnfTransformation,[status(thm)],[f_1073]) ).
tff(c_392260,plain,
( ( zero_zero(int) != pls )
| ( ti(int,succ(hAPP(nat,int,semiring_1_of_nat(int),n))) = zero_zero(int) )
| ~ ring_11004092258visors(int) ),
inference(superposition,[status(thm),theory(equality)],[c_7190,c_392156]) ).
tff(c_392313,plain,
succ(hAPP(nat,int,semiring_1_of_nat(int),n)) = pls,
inference(demodulation,[status(thm),theory(equality)],[c_3211,c_417,c_116,c_417,c_392260]) ).
tff(c_3257,plain,
ab_group_add(int),
inference(cnfTransformation,[status(thm)],[f_6067]) ).
tff(c_102,plain,
ti(int,min) = min,
inference(cnfTransformation,[status(thm)],[f_196]) ).
tff(c_4297,plain,
! [K_1_3453] : ( ti(int,K_1_3453) = number_number_of(int,K_1_3453) ),
inference(cnfTransformation,[status(thm)],[f_841]) ).
tff(c_4357,plain,
number_number_of(int,min) = min,
inference(superposition,[status(thm),theory(equality)],[c_102,c_4297]) ).
tff(c_2433,plain,
! [K_1_2781] : ( minus_minus(int,K_1_2781,min) = succ(K_1_2781) ),
inference(cnfTransformation,[status(thm)],[f_4597]) ).
tff(c_331773,plain,
! [X_a_356559,B_356560,A_2_356561] :
( ( ti(X_a_356559,B_356560) = ti(X_a_356559,A_2_356561) )
| ( minus_minus(X_a_356559,A_2_356561,B_356560) != zero_zero(X_a_356559) )
| ~ ab_group_add(X_a_356559) ),
inference(cnfTransformation,[status(thm)],[f_2154]) ).
tff(c_331873,plain,
! [K_1_2781] :
( ( ti(int,min) = ti(int,K_1_2781) )
| ( zero_zero(int) != succ(K_1_2781) )
| ~ ab_group_add(int) ),
inference(superposition,[status(thm),theory(equality)],[c_2433,c_331773]) ).
tff(c_331975,plain,
! [K_1_356562] :
( ( number_number_of(int,K_1_356562) = min )
| ( succ(K_1_356562) != pls ) ),
inference(demodulation,[status(thm),theory(equality)],[c_3257,c_417,c_533,c_4357,c_533,c_331873]) ).
tff(c_4049,plain,
! [V_1_1778] : ( nat_1(number_number_of(int,V_1_1778)) = nat_1(V_1_1778) ),
inference(demodulation,[status(thm),theory(equality)],[c_4047,c_1448]) ).
tff(c_332362,plain,
! [K_1_356562] :
( ( nat_1(min) = nat_1(K_1_356562) )
| ( succ(K_1_356562) != pls ) ),
inference(superposition,[status(thm),theory(equality)],[c_331975,c_4049]) ).
tff(c_392716,plain,
nat_1(hAPP(nat,int,semiring_1_of_nat(int),n)) = nat_1(min),
inference(superposition,[status(thm),theory(equality)],[c_392313,c_332362]) ).
tff(c_393369,plain,
nat_1(min) = n,
inference(demodulation,[status(thm),theory(equality)],[c_1202,c_392716]) ).
tff(c_2389,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min),pls)),
inference(cnfTransformation,[status(thm)],[f_4523]) ).
tff(c_1386,plain,
nat_1(zero_zero(int)) = zero_zero(nat),
inference(cnfTransformation,[status(thm)],[f_2640]) ).
tff(c_3726,plain,
zero_zero(nat) = nat_1(pls),
inference(demodulation,[status(thm),theory(equality)],[c_417,c_1386]) ).
tff(c_1116,plain,
! [I_1_1312] :
( ( zero_zero(nat) = nat_1(I_1_1312) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),I_1_1312),zero_zero(int))) ),
inference(cnfTransformation,[status(thm)],[f_2112]) ).
tff(c_3748,plain,
! [I_1_1312] :
( ( zero_zero(nat) = nat_1(I_1_1312) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),I_1_1312),pls)) ),
inference(demodulation,[status(thm),theory(equality)],[c_417,c_1116]) ).
tff(c_428109,plain,
! [I_1_357148] :
( ( nat_1(pls) = nat_1(I_1_357148) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),I_1_357148),pls)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3726,c_3748]) ).
tff(c_428116,plain,
nat_1(pls) = nat_1(min),
inference(resolution,[status(thm)],[c_2389,c_428109]) ).
tff(c_428123,plain,
nat_1(pls) = n,
inference(demodulation,[status(thm),theory(equality)],[c_393369,c_428116]) ).
tff(c_234,plain,
hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),zero_zero(nat)),n)),
inference(cnfTransformation,[status(thm)],[f_393]) ).
tff(c_4037,plain,
hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),nat_1(pls)),n)),
inference(demodulation,[status(thm),theory(equality)],[c_3726,c_234]) ).
tff(c_428128,plain,
hBOOL(hAPP(nat,bool,hAPP(nat,fun(nat,bool),ord_less(nat),n),n)),
inference(demodulation,[status(thm),theory(equality)],[c_428123,c_4037]) ).
tff(c_428170,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1978,c_428128]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : NUM925+7 : TPTP v9.0.0. Released v5.3.0.
% 0.08/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.14/0.34 % Computer : n029.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.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 15:50:19 EDT 2025
% 0.14/0.34 % CPUTime :
% 151.85/117.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 151.86/117.43
% 151.86/117.43 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------