%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM925+1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:53:34 AM UTC 2026
% Result : Theorem 20.06s 20.34s
% Output : Proof 20.23s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(fact_0_n1pos,axiom,
ord_less_int(zero_zero_int,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
file('theBenchmark.p',fact_0_n1pos) ).
fof(fact_1_t1,axiom,
ord_less_int(one_one_int,t),
file('theBenchmark.p',fact_1_t1) ).
fof(fact_2_sum__power2__eq__zero__iff,axiom,
! [Xa,Ya] :
( plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int
<=> ( Ya = zero_zero_int
& Xa = zero_zero_int ) ),
file('theBenchmark.p',fact_2_sum__power2__eq__zero__iff) ).
fof(fact_3_one__power2,axiom,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
file('theBenchmark.p',fact_3_one__power2) ).
fof(fact_4_one__power2,axiom,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
file('theBenchmark.p',fact_4_one__power2) ).
fof(fact_5_zero__power2,axiom,
power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
file('theBenchmark.p',fact_5_zero__power2) ).
fof(fact_6_zero__power2,axiom,
power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_nat,
file('theBenchmark.p',fact_6_zero__power2) ).
fof(fact_7_zero__eq__power2,axiom,
! [A_1] :
( power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
<=> A_1 = zero_zero_int ),
file('theBenchmark.p',fact_7_zero__eq__power2) ).
fof(fact_8_add__special_I2_J,axiom,
! [W_5] : plus_plus_int(one_one_int,number_number_of_int(W_5)) = number_number_of_int(plus_plus_int(bit1(pls),W_5)),
file('theBenchmark.p',fact_8_add__special_I2_J) ).
fof(fact_9_add__special_I3_J,axiom,
! [V_5] : plus_plus_int(number_number_of_int(V_5),one_one_int) = number_number_of_int(plus_plus_int(V_5,bit1(pls))),
file('theBenchmark.p',fact_9_add__special_I3_J) ).
fof(fact_10_one__add__one__is__two,axiom,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
file('theBenchmark.p',fact_10_one__add__one__is__two) ).
fof(fact_11_semiring__one__add__one__is__two,axiom,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
file('theBenchmark.p',fact_11_semiring__one__add__one__is__two) ).
fof(fact_12_semiring__one__add__one__is__two,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('theBenchmark.p',fact_12_semiring__one__add__one__is__two) ).
fof(fact_13_quartic__square__square,axiom,
! [X] : power_power_int(power_power_int(X,number_number_of_nat(bit0(bit1(pls)))),number_number_of_nat(bit0(bit1(pls)))) = power_power_int(X,number_number_of_nat(bit0(bit0(bit1(pls))))),
file('theBenchmark.p',fact_13_quartic__square__square) ).
fof(fact_14_power__0__left__number__of,axiom,
! [W_4] :
( ( number_number_of_nat(W_4) != zero_zero_nat
=> power_power_int(zero_zero_int,number_number_of_nat(W_4)) = zero_zero_int )
& ( number_number_of_nat(W_4) = zero_zero_nat
=> power_power_int(zero_zero_int,number_number_of_nat(W_4)) = one_one_int ) ),
file('theBenchmark.p',fact_14_power__0__left__number__of) ).
fof(fact_15_power__0__left__number__of,axiom,
! [W_4] :
( ( number_number_of_nat(W_4) != zero_zero_nat
=> power_power_nat(zero_zero_nat,number_number_of_nat(W_4)) = zero_zero_nat )
& ( number_number_of_nat(W_4) = zero_zero_nat
=> power_power_nat(zero_zero_nat,number_number_of_nat(W_4)) = one_one_nat ) ),
file('theBenchmark.p',fact_15_power__0__left__number__of) ).
fof(fact_16_semiring__norm_I110_J,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('theBenchmark.p',fact_16_semiring__norm_I110_J) ).
fof(fact_17_numeral__1__eq__1,axiom,
number_number_of_int(bit1(pls)) = one_one_int,
file('theBenchmark.p',fact_17_numeral__1__eq__1) ).
fof(fact_18_n0,axiom,
ord_less_nat(zero_zero_nat,n),
file('theBenchmark.p',fact_18_n0) ).
fof(fact_19_zless__linear,axiom,
! [X,Y] :
( ord_less_int(Y,X)
| X = Y
| ord_less_int(X,Y) ),
file('theBenchmark.p',fact_19_zless__linear) ).
fof(fact_20_less__number__of__int__code,axiom,
! [K_1,L_1] :
( ord_less_int(number_number_of_int(K_1),number_number_of_int(L_1))
<=> ord_less_int(K_1,L_1) ),
file('theBenchmark.p',fact_20_less__number__of__int__code) ).
fof(fact_21_plus__numeral__code_I9_J,axiom,
! [V_3,W_3] : plus_plus_int(number_number_of_int(V_3),number_number_of_int(W_3)) = number_number_of_int(plus_plus_int(V_3,W_3)),
file('theBenchmark.p',fact_21_plus__numeral__code_I9_J) ).
fof(fact_22_less__number__of,axiom,
! [Xa,Ya] :
( ord_less_int(number_number_of_int(Xa),number_number_of_int(Ya))
<=> ord_less_int(Xa,Ya) ),
file('theBenchmark.p',fact_22_less__number__of) ).
fof(fact_23_zero__is__num__zero,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_23_zero__is__num__zero) ).
fof(fact_24_zpower__int,axiom,
! [M,N_1] : power_power_int(semiri1621563631at_int(M),N_1) = semiri1621563631at_int(power_power_nat(M,N_1)),
file('theBenchmark.p',fact_24_zpower__int) ).
fof(fact_25_int__power,axiom,
! [M,N_1] : semiri1621563631at_int(power_power_nat(M,N_1)) = power_power_int(semiri1621563631at_int(M),N_1),
file('theBenchmark.p',fact_25_int__power) ).
fof(fact_26_zadd__int__left,axiom,
! [M,N_1,Z] : plus_plus_int(semiri1621563631at_int(M),plus_plus_int(semiri1621563631at_int(N_1),Z)) = plus_plus_int(semiri1621563631at_int(plus_plus_nat(M,N_1)),Z),
file('theBenchmark.p',fact_26_zadd__int__left) ).
fof(fact_27_zadd__int,axiom,
! [M,N_1] : plus_plus_int(semiri1621563631at_int(M),semiri1621563631at_int(N_1)) = semiri1621563631at_int(plus_plus_nat(M,N_1)),
file('theBenchmark.p',fact_27_zadd__int) ).
fof(fact_28_int__1,axiom,
semiri1621563631at_int(one_one_nat) = one_one_int,
file('theBenchmark.p',fact_28_int__1) ).
fof(fact_29_nat__number__of__Pls,axiom,
number_number_of_nat(pls) = zero_zero_nat,
file('theBenchmark.p',fact_29_nat__number__of__Pls) ).
fof(fact_30_semiring__norm_I113_J,axiom,
zero_zero_nat = number_number_of_nat(pls),
file('theBenchmark.p',fact_30_semiring__norm_I113_J) ).
fof(fact_31_int__eq__0__conv,axiom,
! [Na] :
( semiri1621563631at_int(Na) = zero_zero_int
<=> Na = zero_zero_nat ),
file('theBenchmark.p',fact_31_int__eq__0__conv) ).
fof(fact_32_int__0,axiom,
semiri1621563631at_int(zero_zero_nat) = zero_zero_int,
file('theBenchmark.p',fact_32_int__0) ).
fof(fact_33_nat__1__add__1,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('theBenchmark.p',fact_33_nat__1__add__1) ).
fof(fact_34_less__int__code_I16_J,axiom,
! [K1,K2] :
( ord_less_int(bit1(K1),bit1(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_34_less__int__code_I16_J) ).
fof(fact_35_rel__simps_I17_J,axiom,
! [K_1,L_1] :
( ord_less_int(bit1(K_1),bit1(L_1))
<=> ord_less_int(K_1,L_1) ),
file('theBenchmark.p',fact_35_rel__simps_I17_J) ).
fof(fact_36_rel__simps_I2_J,axiom,
~ ord_less_int(pls,pls),
file('theBenchmark.p',fact_36_rel__simps_I2_J) ).
fof(fact_37_less__int__code_I13_J,axiom,
! [K1,K2] :
( ord_less_int(bit0(K1),bit0(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_37_less__int__code_I13_J) ).
fof(fact_38_rel__simps_I14_J,axiom,
! [K_1,L_1] :
( ord_less_int(bit0(K_1),bit0(L_1))
<=> ord_less_int(K_1,L_1) ),
file('theBenchmark.p',fact_38_rel__simps_I14_J) ).
fof(fact_39_zadd__strict__right__mono,axiom,
! [K,I,J] :
( ord_less_int(I,J)
=> ord_less_int(plus_plus_int(I,K),plus_plus_int(J,K)) ),
file('theBenchmark.p',fact_39_zadd__strict__right__mono) ).
fof(fact_40_add__nat__number__of,axiom,
! [V_4,V_3] :
( ( ~ ord_less_int(V_3,pls)
=> ( ( ~ ord_less_int(V_4,pls)
=> plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(plus_plus_int(V_3,V_4)) )
& ( ord_less_int(V_4,pls)
=> plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(V_3) ) ) )
& ( ord_less_int(V_3,pls)
=> plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(V_4) ) ),
file('theBenchmark.p',fact_40_add__nat__number__of) ).
fof(fact_41_one__is__num__one,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('theBenchmark.p',fact_41_one__is__num__one) ).
fof(fact_42_nat__numeral__1__eq__1,axiom,
number_number_of_nat(bit1(pls)) = one_one_nat,
file('theBenchmark.p',fact_42_nat__numeral__1__eq__1) ).
fof(fact_43_Numeral1__eq1__nat,axiom,
one_one_nat = number_number_of_nat(bit1(pls)),
file('theBenchmark.p',fact_43_Numeral1__eq1__nat) ).
fof(fact_44_eq__number__of,axiom,
! [Xa,Ya] :
( number_number_of_int(Xa) = number_number_of_int(Ya)
<=> Xa = Ya ),
file('theBenchmark.p',fact_44_eq__number__of) ).
fof(fact_45_number__of__reorient,axiom,
! [Wa,Xa] :
( number_number_of_nat(Wa) = Xa
<=> Xa = number_number_of_nat(Wa) ),
file('theBenchmark.p',fact_45_number__of__reorient) ).
fof(fact_46_number__of__reorient,axiom,
! [Wa,Xa] :
( number_number_of_int(Wa) = Xa
<=> Xa = number_number_of_int(Wa) ),
file('theBenchmark.p',fact_46_number__of__reorient) ).
fof(fact_47_rel__simps_I51_J,axiom,
! [K_1,L_1] :
( bit1(K_1) = bit1(L_1)
<=> K_1 = L_1 ),
file('theBenchmark.p',fact_47_rel__simps_I51_J) ).
fof(fact_48_rel__simps_I48_J,axiom,
! [K_1,L_1] :
( bit0(K_1) = bit0(L_1)
<=> K_1 = L_1 ),
file('theBenchmark.p',fact_48_rel__simps_I48_J) ).
fof(fact_49_even__less__0__iff,axiom,
! [A_1] :
( ord_less_int(plus_plus_int(A_1,A_1),zero_zero_int)
<=> ord_less_int(A_1,zero_zero_int) ),
file('theBenchmark.p',fact_49_even__less__0__iff) ).
fof(fact_50_zadd__assoc,axiom,
! [Z1,Z2,Z3] : plus_plus_int(plus_plus_int(Z1,Z2),Z3) = plus_plus_int(Z1,plus_plus_int(Z2,Z3)),
file('theBenchmark.p',fact_50_zadd__assoc) ).
fof(fact_51_zadd__left__commute,axiom,
! [X,Y,Z] : plus_plus_int(X,plus_plus_int(Y,Z)) = plus_plus_int(Y,plus_plus_int(X,Z)),
file('theBenchmark.p',fact_51_zadd__left__commute) ).
fof(fact_52_zadd__commute,axiom,
! [Z,W_3] : plus_plus_int(Z,W_3) = plus_plus_int(W_3,Z),
file('theBenchmark.p',fact_52_zadd__commute) ).
fof(fact_53_int__int__eq,axiom,
! [Ma,Na] :
( semiri1621563631at_int(Ma) = semiri1621563631at_int(Na)
<=> Ma = Na ),
file('theBenchmark.p',fact_53_int__int__eq) ).
fof(fact_54_less__special_I3_J,axiom,
! [Xa] :
( ord_less_int(number_number_of_int(Xa),zero_zero_int)
<=> ord_less_int(Xa,pls) ),
file('theBenchmark.p',fact_54_less__special_I3_J) ).
fof(fact_55_less__special_I1_J,axiom,
! [Ya] :
( ord_less_int(zero_zero_int,number_number_of_int(Ya))
<=> ord_less_int(pls,Ya) ),
file('theBenchmark.p',fact_55_less__special_I1_J) ).
fof(fact_56_rel__simps_I12_J,axiom,
! [K_1] :
( ord_less_int(bit1(K_1),pls)
<=> ord_less_int(K_1,pls) ),
file('theBenchmark.p',fact_56_rel__simps_I12_J) ).
fof(fact_57_less__int__code_I15_J,axiom,
! [K1,K2] :
( ord_less_int(bit1(K1),bit0(K2))
<=> ord_less_int(K1,K2) ),
file('theBenchmark.p',fact_57_less__int__code_I15_J) ).
fof(fact_58_rel__simps_I16_J,axiom,
! [K_1,L_1] :
( ord_less_int(bit1(K_1),bit0(L_1))
<=> ord_less_int(K_1,L_1) ),
file('theBenchmark.p',fact_58_rel__simps_I16_J) ).
fof(fact_59_rel__simps_I10_J,axiom,
! [K_1] :
( ord_less_int(bit0(K_1),pls)
<=> ord_less_int(K_1,pls) ),
file('theBenchmark.p',fact_59_rel__simps_I10_J) ).
fof(fact_60_rel__simps_I4_J,axiom,
! [K_1] :
( ord_less_int(pls,bit0(K_1))
<=> ord_less_int(pls,K_1) ),
file('theBenchmark.p',fact_60_rel__simps_I4_J) ).
fof(fact_61_bin__less__0__simps_I4_J,axiom,
! [Wa] :
( ord_less_int(bit1(Wa),zero_zero_int)
<=> ord_less_int(Wa,zero_zero_int) ),
file('theBenchmark.p',fact_61_bin__less__0__simps_I4_J) ).
fof(fact_62_bin__less__0__simps_I1_J,axiom,
~ ord_less_int(pls,zero_zero_int),
file('theBenchmark.p',fact_62_bin__less__0__simps_I1_J) ).
fof(fact_63_bin__less__0__simps_I3_J,axiom,
! [Wa] :
( ord_less_int(bit0(Wa),zero_zero_int)
<=> ord_less_int(Wa,zero_zero_int) ),
file('theBenchmark.p',fact_63_bin__less__0__simps_I3_J) ).
fof(fact_64_int__0__less__1,axiom,
ord_less_int(zero_zero_int,one_one_int),
file('theBenchmark.p',fact_64_int__0__less__1) ).
fof(fact_65_zless__add1__eq,axiom,
! [Wa,Z_2] :
( ord_less_int(Wa,plus_plus_int(Z_2,one_one_int))
<=> ( Wa = Z_2
| ord_less_int(Wa,Z_2) ) ),
file('theBenchmark.p',fact_65_zless__add1__eq) ).
fof(fact_66_int__less__0__conv,axiom,
! [K] : ~ ord_less_int(semiri1621563631at_int(K),zero_zero_int),
file('theBenchmark.p',fact_66_int__less__0__conv) ).
fof(fact_67_less__special_I4_J,axiom,
! [Xa] :
( ord_less_int(number_number_of_int(Xa),one_one_int)
<=> ord_less_int(Xa,bit1(pls)) ),
file('theBenchmark.p',fact_67_less__special_I4_J) ).
fof(fact_68_less__special_I2_J,axiom,
! [Ya] :
( ord_less_int(one_one_int,number_number_of_int(Ya))
<=> ord_less_int(bit1(pls),Ya) ),
file('theBenchmark.p',fact_68_less__special_I2_J) ).
fof(fact_69_odd__less__0,axiom,
! [Z_2] :
( ord_less_int(plus_plus_int(plus_plus_int(one_one_int,Z_2),Z_2),zero_zero_int)
<=> ord_less_int(Z_2,zero_zero_int) ),
file('theBenchmark.p',fact_69_odd__less__0) ).
fof(fact_70_double__eq__0__iff,axiom,
! [A_1] :
( plus_plus_int(A_1,A_1) = zero_zero_int
<=> A_1 = zero_zero_int ),
file('theBenchmark.p',fact_70_double__eq__0__iff) ).
fof(fact_71_rel__simps_I46_J,axiom,
! [K] : bit1(K) != pls,
file('theBenchmark.p',fact_71_rel__simps_I46_J) ).
fof(fact_72_rel__simps_I39_J,axiom,
! [L] : pls != bit1(L),
file('theBenchmark.p',fact_72_rel__simps_I39_J) ).
fof(fact_73_rel__simps_I50_J,axiom,
! [K,L] : bit1(K) != bit0(L),
file('theBenchmark.p',fact_73_rel__simps_I50_J) ).
fof(fact_74_rel__simps_I49_J,axiom,
! [K,L] : bit0(K) != bit1(L),
file('theBenchmark.p',fact_74_rel__simps_I49_J) ).
fof(fact_75_rel__simps_I44_J,axiom,
! [K_1] :
( bit0(K_1) = pls
<=> K_1 = pls ),
file('theBenchmark.p',fact_75_rel__simps_I44_J) ).
fof(fact_76_rel__simps_I38_J,axiom,
! [L_1] :
( pls = bit0(L_1)
<=> pls = L_1 ),
file('theBenchmark.p',fact_76_rel__simps_I38_J) ).
fof(fact_77_Bit0__Pls,axiom,
bit0(pls) = pls,
file('theBenchmark.p',fact_77_Bit0__Pls) ).
fof(fact_78_Pls__def,axiom,
pls = zero_zero_int,
file('theBenchmark.p',fact_78_Pls__def) ).
fof(fact_79_int__0__neq__1,axiom,
zero_zero_int != one_one_int,
file('theBenchmark.p',fact_79_int__0__neq__1) ).
fof(fact_80_add__Pls__right,axiom,
! [K] : plus_plus_int(K,pls) = K,
file('theBenchmark.p',fact_80_add__Pls__right) ).
fof(fact_81_add__Pls,axiom,
! [K] : plus_plus_int(pls,K) = K,
file('theBenchmark.p',fact_81_add__Pls) ).
fof(fact_82_add__Bit0__Bit0,axiom,
! [K,L] : plus_plus_int(bit0(K),bit0(L)) = bit0(plus_plus_int(K,L)),
file('theBenchmark.p',fact_82_add__Bit0__Bit0) ).
fof(fact_83_Bit0__def,axiom,
! [K] : bit0(K) = plus_plus_int(K,K),
file('theBenchmark.p',fact_83_Bit0__def) ).
fof(fact_84_zadd__0__right,axiom,
! [Z] : plus_plus_int(Z,zero_zero_int) = Z,
file('theBenchmark.p',fact_84_zadd__0__right) ).
fof(fact_85_zadd__0,axiom,
! [Z] : plus_plus_int(zero_zero_int,Z) = Z,
file('theBenchmark.p',fact_85_zadd__0) ).
fof(fact_86_semiring__numeral__0__eq__0,axiom,
number_number_of_int(pls) = zero_zero_int,
file('theBenchmark.p',fact_86_semiring__numeral__0__eq__0) ).
fof(fact_87_semiring__numeral__0__eq__0,axiom,
number_number_of_nat(pls) = zero_zero_nat,
file('theBenchmark.p',fact_87_semiring__numeral__0__eq__0) ).
fof(fact_88_number__of__Pls,axiom,
number_number_of_int(pls) = zero_zero_int,
file('theBenchmark.p',fact_88_number__of__Pls) ).
fof(fact_89_semiring__norm_I112_J,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_89_semiring__norm_I112_J) ).
fof(fact_90_add__numeral__0,axiom,
! [A_3] : plus_plus_int(number_number_of_int(pls),A_3) = A_3,
file('theBenchmark.p',fact_90_add__numeral__0) ).
fof(fact_91_add__numeral__0__right,axiom,
! [A_2] : plus_plus_int(A_2,number_number_of_int(pls)) = A_2,
file('theBenchmark.p',fact_91_add__numeral__0__right) ).
fof(fact_92_power__eq__0__iff__number__of,axiom,
! [A_1,Wa] :
( power_power_int(A_1,number_number_of_nat(Wa)) = zero_zero_int
<=> ( number_number_of_nat(Wa) != zero_zero_nat
& A_1 = zero_zero_int ) ),
file('theBenchmark.p',fact_92_power__eq__0__iff__number__of) ).
fof(fact_93_power__eq__0__iff__number__of,axiom,
! [A_1,Wa] :
( power_power_nat(A_1,number_number_of_nat(Wa)) = zero_zero_nat
<=> ( number_number_of_nat(Wa) != zero_zero_nat
& A_1 = zero_zero_nat ) ),
file('theBenchmark.p',fact_93_power__eq__0__iff__number__of) ).
fof(fact_94_add__number__of__left,axiom,
! [V_2,W_2,Z_1] : plus_plus_int(number_number_of_int(V_2),plus_plus_int(number_number_of_int(W_2),Z_1)) = plus_plus_int(number_number_of_int(plus_plus_int(V_2,W_2)),Z_1),
file('theBenchmark.p',fact_94_add__number__of__left) ).
fof(fact_95_add__number__of__eq,axiom,
! [V_1,W_1] : plus_plus_int(number_number_of_int(V_1),number_number_of_int(W_1)) = number_number_of_int(plus_plus_int(V_1,W_1)),
file('theBenchmark.p',fact_95_add__number__of__eq) ).
fof(fact_96_number__of__add,axiom,
! [V,W] : number_number_of_int(plus_plus_int(V,W)) = plus_plus_int(number_number_of_int(V),number_number_of_int(W)),
file('theBenchmark.p',fact_96_number__of__add) ).
fof(fact_97_add__Bit1__Bit0,axiom,
! [K,L] : plus_plus_int(bit1(K),bit0(L)) = bit1(plus_plus_int(K,L)),
file('theBenchmark.p',fact_97_add__Bit1__Bit0) ).
fof(fact_98_add__Bit0__Bit1,axiom,
! [K,L] : plus_plus_int(bit0(K),bit1(L)) = bit1(plus_plus_int(K,L)),
file('theBenchmark.p',fact_98_add__Bit0__Bit1) ).
fof(fact_99_Bit1__def,axiom,
! [K] : bit1(K) = plus_plus_int(plus_plus_int(one_one_int,K),K),
file('theBenchmark.p',fact_99_Bit1__def) ).
fof(fact_100_odd__nonzero,axiom,
! [Z] : plus_plus_int(plus_plus_int(one_one_int,Z),Z) != zero_zero_int,
file('theBenchmark.p',fact_100_odd__nonzero) ).
fof(fact_101_number__of__int,axiom,
! [N] : number_number_of_nat(semiri1621563631at_int(N)) = semiri984289939at_nat(N),
file('theBenchmark.p',fact_101_number__of__int) ).
fof(fact_102_number__of__int,axiom,
! [N] : number_number_of_int(semiri1621563631at_int(N)) = semiri1621563631at_int(N),
file('theBenchmark.p',fact_102_number__of__int) ).
fof(fact_103_zero__less__power2,axiom,
! [A_1] :
( ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))
<=> A_1 != zero_zero_int ),
file('theBenchmark.p',fact_103_zero__less__power2) ).
fof(fact_104_power2__less__0,axiom,
! [A] : ~ ord_less_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
file('theBenchmark.p',fact_104_power2__less__0) ).
fof(fact_105_sum__power2__gt__zero__iff,axiom,
! [Xa,Ya] :
( ord_less_int(zero_zero_int,plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls))))))
<=> ( Ya != zero_zero_int
| Xa != zero_zero_int ) ),
file('theBenchmark.p',fact_105_sum__power2__gt__zero__iff) ).
fof(conj_0,conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('theBenchmark.p',conj_0) ).
fof(f_1_1,plain,
ord_less_int(zero_zero_int,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
inference(fof_nnf,[status(thm)],[fact_0_n1pos]) ).
cnf(f_1_2,plain,
ord_less_int(zero_zero_int,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
inference(clausify,[status(thm)],[f_1_1]) ).
fof(f_2_1,plain,
ord_less_int(one_one_int,t),
inference(fof_nnf,[status(thm)],[fact_1_t1]) ).
cnf(f_2_2,plain,
ord_less_int(one_one_int,t),
inference(clausify,[status(thm)],[f_2_1]) ).
fof(f_3_1,plain,
! [Xa,Ya] :
( ( plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int
| Ya != zero_zero_int
| Xa != zero_zero_int )
& ( ( Ya = zero_zero_int
& Xa = zero_zero_int )
| plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[fact_2_sum__power2__eq__zero__iff]) ).
fof(f_3_2,plain,
! [U_1,U_0] :
( ( plus_plus_int(power_power_int(U_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_0,number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int
| U_0 != zero_zero_int
| U_1 != zero_zero_int )
& ( ( U_0 = zero_zero_int
& U_1 = zero_zero_int )
| plus_plus_int(power_power_int(U_1,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_0,number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_5,U_3] :
( plus_plus_int(power_power_int(U_5,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_3,number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int
| U_3 != zero_zero_int
| U_5 != zero_zero_int )
& ! [U_4,U_2] :
( ( U_2 = zero_zero_int
& U_4 = zero_zero_int )
| plus_plus_int(power_power_int(U_4,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_2,number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( U_4 = zero_zero_int
| plus_plus_int(power_power_int(U_4,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_2,number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_5,plain,
( U_2 = zero_zero_int
| plus_plus_int(power_power_int(U_4,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_2,number_number_of_nat(bit0(bit1(pls))))) != zero_zero_int ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_6,plain,
( plus_plus_int(power_power_int(U_5,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_3,number_number_of_nat(bit0(bit1(pls))))) = zero_zero_int
| U_3 != zero_zero_int
| U_5 != zero_zero_int ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
inference(fof_nnf,[status(thm)],[fact_3_one__power2]) ).
cnf(f_4_2,plain,
power_power_int(one_one_int,number_number_of_nat(bit0(bit1(pls)))) = one_one_int,
inference(clausify,[status(thm)],[f_4_1]) ).
fof(f_5_1,plain,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
inference(fof_nnf,[status(thm)],[fact_4_one__power2]) ).
cnf(f_5_2,plain,
power_power_nat(one_one_nat,number_number_of_nat(bit0(bit1(pls)))) = one_one_nat,
inference(clausify,[status(thm)],[f_5_1]) ).
fof(f_6_1,plain,
power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_5_zero__power2]) ).
cnf(f_6_2,plain,
power_power_int(zero_zero_int,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(clausify,[status(thm)],[f_6_1]) ).
fof(f_7_1,plain,
power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_nat,
inference(fof_nnf,[status(thm)],[fact_6_zero__power2]) ).
cnf(f_7_2,plain,
power_power_nat(zero_zero_nat,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_nat,
inference(clausify,[status(thm)],[f_7_1]) ).
fof(f_8_1,plain,
! [A_1] :
( ( power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
| A_1 != zero_zero_int )
& ( A_1 = zero_zero_int
| power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[fact_7_zero__eq__power2]) ).
fof(f_8_2,plain,
! [U_6] :
( ( power_power_int(U_6,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
| U_6 != zero_zero_int )
& ( U_6 = zero_zero_int
| power_power_int(U_6,number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_8] :
( power_power_int(U_8,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
| U_8 != zero_zero_int )
& ! [U_7] :
( U_7 = zero_zero_int
| power_power_int(U_7,number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( U_7 = zero_zero_int
| power_power_int(U_7,number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( power_power_int(U_8,number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int
| U_8 != zero_zero_int ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [W_5] : plus_plus_int(one_one_int,number_number_of_int(W_5)) = number_number_of_int(plus_plus_int(bit1(pls),W_5)),
inference(fof_nnf,[status(thm)],[fact_8_add__special_I2_J]) ).
fof(f_9_2,plain,
! [U_9] : plus_plus_int(one_one_int,number_number_of_int(U_9)) = number_number_of_int(plus_plus_int(bit1(pls),U_9)),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
plus_plus_int(one_one_int,number_number_of_int(U_9)) = number_number_of_int(plus_plus_int(bit1(pls),U_9)),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [V_5] : plus_plus_int(number_number_of_int(V_5),one_one_int) = number_number_of_int(plus_plus_int(V_5,bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_9_add__special_I3_J]) ).
fof(f_10_2,plain,
! [U_10] : plus_plus_int(number_number_of_int(U_10),one_one_int) = number_number_of_int(plus_plus_int(U_10,bit1(pls))),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
plus_plus_int(number_number_of_int(U_10),one_one_int) = number_number_of_int(plus_plus_int(U_10,bit1(pls))),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_10_one__add__one__is__two]) ).
cnf(f_11_2,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_11_semiring__one__add__one__is__two]) ).
cnf(f_12_2,plain,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_13_1,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_12_semiring__one__add__one__is__two]) ).
cnf(f_13_2,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_13_1]) ).
fof(f_14_1,plain,
! [X] : power_power_int(power_power_int(X,number_number_of_nat(bit0(bit1(pls)))),number_number_of_nat(bit0(bit1(pls)))) = power_power_int(X,number_number_of_nat(bit0(bit0(bit1(pls))))),
inference(fof_nnf,[status(thm)],[fact_13_quartic__square__square]) ).
fof(f_14_2,plain,
! [U_11] : power_power_int(power_power_int(U_11,number_number_of_nat(bit0(bit1(pls)))),number_number_of_nat(bit0(bit1(pls)))) = power_power_int(U_11,number_number_of_nat(bit0(bit0(bit1(pls))))),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
power_power_int(power_power_int(U_11,number_number_of_nat(bit0(bit1(pls)))),number_number_of_nat(bit0(bit1(pls)))) = power_power_int(U_11,number_number_of_nat(bit0(bit0(bit1(pls))))),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [W_4] :
( ( power_power_int(zero_zero_int,number_number_of_nat(W_4)) = zero_zero_int
| number_number_of_nat(W_4) = zero_zero_nat )
& ( power_power_int(zero_zero_int,number_number_of_nat(W_4)) = one_one_int
| number_number_of_nat(W_4) != zero_zero_nat ) ),
inference(fof_nnf,[status(thm)],[fact_14_power__0__left__number__of]) ).
fof(f_15_2,plain,
! [U_12] :
( ( power_power_int(zero_zero_int,number_number_of_nat(U_12)) = zero_zero_int
| number_number_of_nat(U_12) = zero_zero_nat )
& ( power_power_int(zero_zero_int,number_number_of_nat(U_12)) = one_one_int
| number_number_of_nat(U_12) != zero_zero_nat ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_14] :
( power_power_int(zero_zero_int,number_number_of_nat(U_14)) = zero_zero_int
| number_number_of_nat(U_14) = zero_zero_nat )
& ! [U_13] :
( power_power_int(zero_zero_int,number_number_of_nat(U_13)) = one_one_int
| number_number_of_nat(U_13) != zero_zero_nat ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
cnf(f_15_4,plain,
( power_power_int(zero_zero_int,number_number_of_nat(U_13)) = one_one_int
| number_number_of_nat(U_13) != zero_zero_nat ),
inference(clausify,[status(thm)],[f_15_3]) ).
cnf(f_15_5,plain,
( power_power_int(zero_zero_int,number_number_of_nat(U_14)) = zero_zero_int
| number_number_of_nat(U_14) = zero_zero_nat ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [W_4] :
( ( power_power_nat(zero_zero_nat,number_number_of_nat(W_4)) = zero_zero_nat
| number_number_of_nat(W_4) = zero_zero_nat )
& ( power_power_nat(zero_zero_nat,number_number_of_nat(W_4)) = one_one_nat
| number_number_of_nat(W_4) != zero_zero_nat ) ),
inference(fof_nnf,[status(thm)],[fact_15_power__0__left__number__of]) ).
fof(f_16_2,plain,
! [U_15] :
( ( power_power_nat(zero_zero_nat,number_number_of_nat(U_15)) = zero_zero_nat
| number_number_of_nat(U_15) = zero_zero_nat )
& ( power_power_nat(zero_zero_nat,number_number_of_nat(U_15)) = one_one_nat
| number_number_of_nat(U_15) != zero_zero_nat ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_17] :
( power_power_nat(zero_zero_nat,number_number_of_nat(U_17)) = zero_zero_nat
| number_number_of_nat(U_17) = zero_zero_nat )
& ! [U_16] :
( power_power_nat(zero_zero_nat,number_number_of_nat(U_16)) = one_one_nat
| number_number_of_nat(U_16) != zero_zero_nat ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( power_power_nat(zero_zero_nat,number_number_of_nat(U_16)) = one_one_nat
| number_number_of_nat(U_16) != zero_zero_nat ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( power_power_nat(zero_zero_nat,number_number_of_nat(U_17)) = zero_zero_nat
| number_number_of_nat(U_17) = zero_zero_nat ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(fof_nnf,[status(thm)],[fact_16_semiring__norm_I110_J]) ).
cnf(f_17_2,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(clausify,[status(thm)],[f_17_1]) ).
fof(f_18_1,plain,
number_number_of_int(bit1(pls)) = one_one_int,
inference(fof_nnf,[status(thm)],[fact_17_numeral__1__eq__1]) ).
cnf(f_18_2,plain,
number_number_of_int(bit1(pls)) = one_one_int,
inference(clausify,[status(thm)],[f_18_1]) ).
fof(f_19_1,plain,
ord_less_nat(zero_zero_nat,n),
inference(fof_nnf,[status(thm)],[fact_18_n0]) ).
cnf(f_19_2,plain,
ord_less_nat(zero_zero_nat,n),
inference(clausify,[status(thm)],[f_19_1]) ).
fof(f_20_1,plain,
! [X,Y] :
( ord_less_int(Y,X)
| X = Y
| ord_less_int(X,Y) ),
inference(fof_nnf,[status(thm)],[fact_19_zless__linear]) ).
fof(f_20_2,plain,
! [U_19,U_18] :
( ord_less_int(U_18,U_19)
| U_19 = U_18
| ord_less_int(U_19,U_18) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( ord_less_int(U_18,U_19)
| U_19 = U_18
| ord_less_int(U_19,U_18) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [K_1,L_1] :
( ( ord_less_int(number_number_of_int(K_1),number_number_of_int(L_1))
| ~ ord_less_int(K_1,L_1) )
& ( ord_less_int(K_1,L_1)
| ~ ord_less_int(number_number_of_int(K_1),number_number_of_int(L_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_20_less__number__of__int__code]) ).
fof(f_21_2,plain,
! [U_21,U_20] :
( ( ord_less_int(number_number_of_int(U_21),number_number_of_int(U_20))
| ~ ord_less_int(U_21,U_20) )
& ( ord_less_int(U_21,U_20)
| ~ ord_less_int(number_number_of_int(U_21),number_number_of_int(U_20)) ) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
fof(f_21_3,plain,
( ! [U_25,U_23] :
( ord_less_int(number_number_of_int(U_25),number_number_of_int(U_23))
| ~ ord_less_int(U_25,U_23) )
& ! [U_24,U_22] :
( ord_less_int(U_24,U_22)
| ~ ord_less_int(number_number_of_int(U_24),number_number_of_int(U_22)) ) ),
inference(miniscope,[status(thm)],[f_21_2]) ).
cnf(f_21_4,plain,
( ord_less_int(U_24,U_22)
| ~ ord_less_int(number_number_of_int(U_24),number_number_of_int(U_22)) ),
inference(clausify,[status(thm)],[f_21_3]) ).
cnf(f_21_5,plain,
( ord_less_int(number_number_of_int(U_25),number_number_of_int(U_23))
| ~ ord_less_int(U_25,U_23) ),
inference(clausify,[status(thm)],[f_21_3]) ).
fof(f_22_1,plain,
! [V_3,W_3] : plus_plus_int(number_number_of_int(V_3),number_number_of_int(W_3)) = number_number_of_int(plus_plus_int(V_3,W_3)),
inference(fof_nnf,[status(thm)],[fact_21_plus__numeral__code_I9_J]) ).
fof(f_22_2,plain,
! [U_27,U_26] : plus_plus_int(number_number_of_int(U_27),number_number_of_int(U_26)) = number_number_of_int(plus_plus_int(U_27,U_26)),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
plus_plus_int(number_number_of_int(U_27),number_number_of_int(U_26)) = number_number_of_int(plus_plus_int(U_27,U_26)),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [Xa,Ya] :
( ( ord_less_int(number_number_of_int(Xa),number_number_of_int(Ya))
| ~ ord_less_int(Xa,Ya) )
& ( ord_less_int(Xa,Ya)
| ~ ord_less_int(number_number_of_int(Xa),number_number_of_int(Ya)) ) ),
inference(fof_nnf,[status(thm)],[fact_22_less__number__of]) ).
fof(f_23_2,plain,
! [U_29,U_28] :
( ( ord_less_int(number_number_of_int(U_29),number_number_of_int(U_28))
| ~ ord_less_int(U_29,U_28) )
& ( ord_less_int(U_29,U_28)
| ~ ord_less_int(number_number_of_int(U_29),number_number_of_int(U_28)) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_33,U_31] :
( ord_less_int(number_number_of_int(U_33),number_number_of_int(U_31))
| ~ ord_less_int(U_33,U_31) )
& ! [U_32,U_30] :
( ord_less_int(U_32,U_30)
| ~ ord_less_int(number_number_of_int(U_32),number_number_of_int(U_30)) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
cnf(f_23_4,plain,
( ord_less_int(U_32,U_30)
| ~ ord_less_int(number_number_of_int(U_32),number_number_of_int(U_30)) ),
inference(clausify,[status(thm)],[f_23_3]) ).
cnf(f_23_5,plain,
( ord_less_int(number_number_of_int(U_33),number_number_of_int(U_31))
| ~ ord_less_int(U_33,U_31) ),
inference(clausify,[status(thm)],[f_23_3]) ).
fof(f_24_1,plain,
zero_zero_int = number_number_of_int(pls),
inference(fof_nnf,[status(thm)],[fact_23_zero__is__num__zero]) ).
cnf(f_24_2,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_25_1,plain,
! [M,N_1] : power_power_int(semiri1621563631at_int(M),N_1) = semiri1621563631at_int(power_power_nat(M,N_1)),
inference(fof_nnf,[status(thm)],[fact_24_zpower__int]) ).
fof(f_25_2,plain,
! [U_35,U_34] : power_power_int(semiri1621563631at_int(U_35),U_34) = semiri1621563631at_int(power_power_nat(U_35,U_34)),
inference(variable_rename,[status(thm)],[f_25_1]) ).
cnf(f_25_3,plain,
power_power_int(semiri1621563631at_int(U_35),U_34) = semiri1621563631at_int(power_power_nat(U_35,U_34)),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
! [M,N_1] : semiri1621563631at_int(power_power_nat(M,N_1)) = power_power_int(semiri1621563631at_int(M),N_1),
inference(fof_nnf,[status(thm)],[fact_25_int__power]) ).
fof(f_26_2,plain,
! [U_37,U_36] : semiri1621563631at_int(power_power_nat(U_37,U_36)) = power_power_int(semiri1621563631at_int(U_37),U_36),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
semiri1621563631at_int(power_power_nat(U_37,U_36)) = power_power_int(semiri1621563631at_int(U_37),U_36),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
! [M,N_1,Z] : plus_plus_int(semiri1621563631at_int(M),plus_plus_int(semiri1621563631at_int(N_1),Z)) = plus_plus_int(semiri1621563631at_int(plus_plus_nat(M,N_1)),Z),
inference(fof_nnf,[status(thm)],[fact_26_zadd__int__left]) ).
fof(f_27_2,plain,
! [U_40,U_39,U_38] : plus_plus_int(semiri1621563631at_int(U_40),plus_plus_int(semiri1621563631at_int(U_39),U_38)) = plus_plus_int(semiri1621563631at_int(plus_plus_nat(U_40,U_39)),U_38),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
plus_plus_int(semiri1621563631at_int(U_40),plus_plus_int(semiri1621563631at_int(U_39),U_38)) = plus_plus_int(semiri1621563631at_int(plus_plus_nat(U_40,U_39)),U_38),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
! [M,N_1] : plus_plus_int(semiri1621563631at_int(M),semiri1621563631at_int(N_1)) = semiri1621563631at_int(plus_plus_nat(M,N_1)),
inference(fof_nnf,[status(thm)],[fact_27_zadd__int]) ).
fof(f_28_2,plain,
! [U_42,U_41] : plus_plus_int(semiri1621563631at_int(U_42),semiri1621563631at_int(U_41)) = semiri1621563631at_int(plus_plus_nat(U_42,U_41)),
inference(variable_rename,[status(thm)],[f_28_1]) ).
cnf(f_28_3,plain,
plus_plus_int(semiri1621563631at_int(U_42),semiri1621563631at_int(U_41)) = semiri1621563631at_int(plus_plus_nat(U_42,U_41)),
inference(clausify,[status(thm)],[f_28_2]) ).
fof(f_29_1,plain,
semiri1621563631at_int(one_one_nat) = one_one_int,
inference(fof_nnf,[status(thm)],[fact_28_int__1]) ).
cnf(f_29_2,plain,
semiri1621563631at_int(one_one_nat) = one_one_int,
inference(clausify,[status(thm)],[f_29_1]) ).
fof(f_30_1,plain,
number_number_of_nat(pls) = zero_zero_nat,
inference(fof_nnf,[status(thm)],[fact_29_nat__number__of__Pls]) ).
cnf(f_30_2,plain,
number_number_of_nat(pls) = zero_zero_nat,
inference(clausify,[status(thm)],[f_30_1]) ).
fof(f_31_1,plain,
zero_zero_nat = number_number_of_nat(pls),
inference(fof_nnf,[status(thm)],[fact_30_semiring__norm_I113_J]) ).
cnf(f_31_2,plain,
zero_zero_nat = number_number_of_nat(pls),
inference(clausify,[status(thm)],[f_31_1]) ).
fof(f_32_1,plain,
! [Na] :
( ( semiri1621563631at_int(Na) = zero_zero_int
| Na != zero_zero_nat )
& ( Na = zero_zero_nat
| semiri1621563631at_int(Na) != zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[fact_31_int__eq__0__conv]) ).
fof(f_32_2,plain,
! [U_43] :
( ( semiri1621563631at_int(U_43) = zero_zero_int
| U_43 != zero_zero_nat )
& ( U_43 = zero_zero_nat
| semiri1621563631at_int(U_43) != zero_zero_int ) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
( ! [U_45] :
( semiri1621563631at_int(U_45) = zero_zero_int
| U_45 != zero_zero_nat )
& ! [U_44] :
( U_44 = zero_zero_nat
| semiri1621563631at_int(U_44) != zero_zero_int ) ),
inference(miniscope,[status(thm)],[f_32_2]) ).
cnf(f_32_4,plain,
( U_44 = zero_zero_nat
| semiri1621563631at_int(U_44) != zero_zero_int ),
inference(clausify,[status(thm)],[f_32_3]) ).
cnf(f_32_5,plain,
( semiri1621563631at_int(U_45) = zero_zero_int
| U_45 != zero_zero_nat ),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
semiri1621563631at_int(zero_zero_nat) = zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_32_int__0]) ).
cnf(f_33_2,plain,
semiri1621563631at_int(zero_zero_nat) = zero_zero_int,
inference(clausify,[status(thm)],[f_33_1]) ).
fof(f_34_1,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(fof_nnf,[status(thm)],[fact_33_nat__1__add__1]) ).
cnf(f_34_2,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
! [K1,K2] :
( ( ord_less_int(bit1(K1),bit1(K2))
| ~ ord_less_int(K1,K2) )
& ( ord_less_int(K1,K2)
| ~ ord_less_int(bit1(K1),bit1(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_34_less__int__code_I16_J]) ).
fof(f_35_2,plain,
! [U_47,U_46] :
( ( ord_less_int(bit1(U_47),bit1(U_46))
| ~ ord_less_int(U_47,U_46) )
& ( ord_less_int(U_47,U_46)
| ~ ord_less_int(bit1(U_47),bit1(U_46)) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_51,U_49] :
( ord_less_int(bit1(U_51),bit1(U_49))
| ~ ord_less_int(U_51,U_49) )
& ! [U_50,U_48] :
( ord_less_int(U_50,U_48)
| ~ ord_less_int(bit1(U_50),bit1(U_48)) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
cnf(f_35_4,plain,
( ord_less_int(U_50,U_48)
| ~ ord_less_int(bit1(U_50),bit1(U_48)) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_5,plain,
( ord_less_int(bit1(U_51),bit1(U_49))
| ~ ord_less_int(U_51,U_49) ),
inference(clausify,[status(thm)],[f_35_3]) ).
fof(f_36_1,plain,
! [K_1,L_1] :
( ( ord_less_int(bit1(K_1),bit1(L_1))
| ~ ord_less_int(K_1,L_1) )
& ( ord_less_int(K_1,L_1)
| ~ ord_less_int(bit1(K_1),bit1(L_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_35_rel__simps_I17_J]) ).
fof(f_36_2,plain,
! [U_53,U_52] :
( ( ord_less_int(bit1(U_53),bit1(U_52))
| ~ ord_less_int(U_53,U_52) )
& ( ord_less_int(U_53,U_52)
| ~ ord_less_int(bit1(U_53),bit1(U_52)) ) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
( ! [U_57,U_55] :
( ord_less_int(bit1(U_57),bit1(U_55))
| ~ ord_less_int(U_57,U_55) )
& ! [U_56,U_54] :
( ord_less_int(U_56,U_54)
| ~ ord_less_int(bit1(U_56),bit1(U_54)) ) ),
inference(miniscope,[status(thm)],[f_36_2]) ).
cnf(f_36_4,plain,
( ord_less_int(U_56,U_54)
| ~ ord_less_int(bit1(U_56),bit1(U_54)) ),
inference(clausify,[status(thm)],[f_36_3]) ).
cnf(f_36_5,plain,
( ord_less_int(bit1(U_57),bit1(U_55))
| ~ ord_less_int(U_57,U_55) ),
inference(clausify,[status(thm)],[f_36_3]) ).
fof(f_37_1,plain,
~ ord_less_int(pls,pls),
inference(fof_nnf,[status(thm)],[fact_36_rel__simps_I2_J]) ).
cnf(f_37_2,plain,
~ ord_less_int(pls,pls),
inference(clausify,[status(thm)],[f_37_1]) ).
fof(f_38_1,plain,
! [K1,K2] :
( ( ord_less_int(bit0(K1),bit0(K2))
| ~ ord_less_int(K1,K2) )
& ( ord_less_int(K1,K2)
| ~ ord_less_int(bit0(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_37_less__int__code_I13_J]) ).
fof(f_38_2,plain,
! [U_59,U_58] :
( ( ord_less_int(bit0(U_59),bit0(U_58))
| ~ ord_less_int(U_59,U_58) )
& ( ord_less_int(U_59,U_58)
| ~ ord_less_int(bit0(U_59),bit0(U_58)) ) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
fof(f_38_3,plain,
( ! [U_63,U_61] :
( ord_less_int(bit0(U_63),bit0(U_61))
| ~ ord_less_int(U_63,U_61) )
& ! [U_62,U_60] :
( ord_less_int(U_62,U_60)
| ~ ord_less_int(bit0(U_62),bit0(U_60)) ) ),
inference(miniscope,[status(thm)],[f_38_2]) ).
cnf(f_38_4,plain,
( ord_less_int(U_62,U_60)
| ~ ord_less_int(bit0(U_62),bit0(U_60)) ),
inference(clausify,[status(thm)],[f_38_3]) ).
cnf(f_38_5,plain,
( ord_less_int(bit0(U_63),bit0(U_61))
| ~ ord_less_int(U_63,U_61) ),
inference(clausify,[status(thm)],[f_38_3]) ).
fof(f_39_1,plain,
! [K_1,L_1] :
( ( ord_less_int(bit0(K_1),bit0(L_1))
| ~ ord_less_int(K_1,L_1) )
& ( ord_less_int(K_1,L_1)
| ~ ord_less_int(bit0(K_1),bit0(L_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_38_rel__simps_I14_J]) ).
fof(f_39_2,plain,
! [U_65,U_64] :
( ( ord_less_int(bit0(U_65),bit0(U_64))
| ~ ord_less_int(U_65,U_64) )
& ( ord_less_int(U_65,U_64)
| ~ ord_less_int(bit0(U_65),bit0(U_64)) ) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
fof(f_39_3,plain,
( ! [U_69,U_67] :
( ord_less_int(bit0(U_69),bit0(U_67))
| ~ ord_less_int(U_69,U_67) )
& ! [U_68,U_66] :
( ord_less_int(U_68,U_66)
| ~ ord_less_int(bit0(U_68),bit0(U_66)) ) ),
inference(miniscope,[status(thm)],[f_39_2]) ).
cnf(f_39_4,plain,
( ord_less_int(U_68,U_66)
| ~ ord_less_int(bit0(U_68),bit0(U_66)) ),
inference(clausify,[status(thm)],[f_39_3]) ).
cnf(f_39_5,plain,
( ord_less_int(bit0(U_69),bit0(U_67))
| ~ ord_less_int(U_69,U_67) ),
inference(clausify,[status(thm)],[f_39_3]) ).
fof(f_40_1,plain,
! [K,I,J] :
( ord_less_int(plus_plus_int(I,K),plus_plus_int(J,K))
| ~ ord_less_int(I,J) ),
inference(fof_nnf,[status(thm)],[fact_39_zadd__strict__right__mono]) ).
fof(f_40_2,plain,
! [U_72,U_71,U_70] :
( ord_less_int(plus_plus_int(U_71,U_72),plus_plus_int(U_70,U_72))
| ~ ord_less_int(U_71,U_70) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( ord_less_int(plus_plus_int(U_71,U_72),plus_plus_int(U_70,U_72))
| ~ ord_less_int(U_71,U_70) ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_41_1,plain,
! [V_4,V_3] :
( ( ( ( plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(plus_plus_int(V_3,V_4))
| ord_less_int(V_4,pls) )
& ( plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(V_3)
| ~ ord_less_int(V_4,pls) ) )
| ord_less_int(V_3,pls) )
& ( plus_plus_nat(number_number_of_nat(V_3),number_number_of_nat(V_4)) = number_number_of_nat(V_4)
| ~ ord_less_int(V_3,pls) ) ),
inference(fof_nnf,[status(thm)],[fact_40_add__nat__number__of]) ).
fof(f_41_2,plain,
! [U_74,U_73] :
( ( ( ( plus_plus_nat(number_number_of_nat(U_73),number_number_of_nat(U_74)) = number_number_of_nat(plus_plus_int(U_73,U_74))
| ord_less_int(U_74,pls) )
& ( plus_plus_nat(number_number_of_nat(U_73),number_number_of_nat(U_74)) = number_number_of_nat(U_73)
| ~ ord_less_int(U_74,pls) ) )
| ord_less_int(U_73,pls) )
& ( plus_plus_nat(number_number_of_nat(U_73),number_number_of_nat(U_74)) = number_number_of_nat(U_74)
| ~ ord_less_int(U_73,pls) ) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
( ! [U_78,U_76] :
( ( ( plus_plus_nat(number_number_of_nat(U_76),number_number_of_nat(U_78)) = number_number_of_nat(plus_plus_int(U_76,U_78))
| ord_less_int(U_78,pls) )
& ( plus_plus_nat(number_number_of_nat(U_76),number_number_of_nat(U_78)) = number_number_of_nat(U_76)
| ~ ord_less_int(U_78,pls) ) )
| ord_less_int(U_76,pls) )
& ! [U_77,U_75] :
( plus_plus_nat(number_number_of_nat(U_75),number_number_of_nat(U_77)) = number_number_of_nat(U_77)
| ~ ord_less_int(U_75,pls) ) ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( plus_plus_nat(number_number_of_nat(U_75),number_number_of_nat(U_77)) = number_number_of_nat(U_77)
| ~ ord_less_int(U_75,pls) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_5,plain,
( plus_plus_nat(number_number_of_nat(U_76),number_number_of_nat(U_78)) = number_number_of_nat(U_76)
| ~ ord_less_int(U_78,pls)
| ord_less_int(U_76,pls) ),
inference(clausify,[status(thm)],[f_41_3]) ).
cnf(f_41_6,plain,
( plus_plus_nat(number_number_of_nat(U_76),number_number_of_nat(U_78)) = number_number_of_nat(plus_plus_int(U_76,U_78))
| ord_less_int(U_78,pls)
| ord_less_int(U_76,pls) ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(fof_nnf,[status(thm)],[fact_41_one__is__num__one]) ).
cnf(f_42_2,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,plain,
number_number_of_nat(bit1(pls)) = one_one_nat,
inference(fof_nnf,[status(thm)],[fact_42_nat__numeral__1__eq__1]) ).
cnf(f_43_2,plain,
number_number_of_nat(bit1(pls)) = one_one_nat,
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
one_one_nat = number_number_of_nat(bit1(pls)),
inference(fof_nnf,[status(thm)],[fact_43_Numeral1__eq1__nat]) ).
cnf(f_44_2,plain,
one_one_nat = number_number_of_nat(bit1(pls)),
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_45_1,plain,
! [Xa,Ya] :
( ( number_number_of_int(Xa) = number_number_of_int(Ya)
| Xa != Ya )
& ( Xa = Ya
| number_number_of_int(Xa) != number_number_of_int(Ya) ) ),
inference(fof_nnf,[status(thm)],[fact_44_eq__number__of]) ).
fof(f_45_2,plain,
! [U_80,U_79] :
( ( number_number_of_int(U_80) = number_number_of_int(U_79)
| U_80 != U_79 )
& ( U_80 = U_79
| number_number_of_int(U_80) != number_number_of_int(U_79) ) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
( ! [U_84,U_82] :
( number_number_of_int(U_84) = number_number_of_int(U_82)
| U_84 != U_82 )
& ! [U_83,U_81] :
( U_83 = U_81
| number_number_of_int(U_83) != number_number_of_int(U_81) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( U_83 = U_81
| number_number_of_int(U_83) != number_number_of_int(U_81) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( number_number_of_int(U_84) = number_number_of_int(U_82)
| U_84 != U_82 ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [Wa,Xa] :
( ( number_number_of_nat(Wa) = Xa
| Xa != number_number_of_nat(Wa) )
& ( Xa = number_number_of_nat(Wa)
| number_number_of_nat(Wa) != Xa ) ),
inference(fof_nnf,[status(thm)],[fact_45_number__of__reorient]) ).
fof(f_46_2,plain,
! [U_86,U_85] :
( ( number_number_of_nat(U_86) = U_85
| U_85 != number_number_of_nat(U_86) )
& ( U_85 = number_number_of_nat(U_86)
| number_number_of_nat(U_86) != U_85 ) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
( ! [U_90,U_88] :
( number_number_of_nat(U_90) = U_88
| U_88 != number_number_of_nat(U_90) )
& ! [U_89,U_87] :
( U_87 = number_number_of_nat(U_89)
| number_number_of_nat(U_89) != U_87 ) ),
inference(miniscope,[status(thm)],[f_46_2]) ).
cnf(f_46_4,plain,
( U_87 = number_number_of_nat(U_89)
| number_number_of_nat(U_89) != U_87 ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( number_number_of_nat(U_90) = U_88
| U_88 != number_number_of_nat(U_90) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [Wa,Xa] :
( ( number_number_of_int(Wa) = Xa
| Xa != number_number_of_int(Wa) )
& ( Xa = number_number_of_int(Wa)
| number_number_of_int(Wa) != Xa ) ),
inference(fof_nnf,[status(thm)],[fact_46_number__of__reorient]) ).
fof(f_47_2,plain,
! [U_92,U_91] :
( ( number_number_of_int(U_92) = U_91
| U_91 != number_number_of_int(U_92) )
& ( U_91 = number_number_of_int(U_92)
| number_number_of_int(U_92) != U_91 ) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
( ! [U_96,U_94] :
( number_number_of_int(U_96) = U_94
| U_94 != number_number_of_int(U_96) )
& ! [U_95,U_93] :
( U_93 = number_number_of_int(U_95)
| number_number_of_int(U_95) != U_93 ) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
cnf(f_47_4,plain,
( U_93 = number_number_of_int(U_95)
| number_number_of_int(U_95) != U_93 ),
inference(clausify,[status(thm)],[f_47_3]) ).
cnf(f_47_5,plain,
( number_number_of_int(U_96) = U_94
| U_94 != number_number_of_int(U_96) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [K_1,L_1] :
( ( bit1(K_1) = bit1(L_1)
| K_1 != L_1 )
& ( K_1 = L_1
| bit1(K_1) != bit1(L_1) ) ),
inference(fof_nnf,[status(thm)],[fact_47_rel__simps_I51_J]) ).
fof(f_48_2,plain,
! [U_98,U_97] :
( ( bit1(U_98) = bit1(U_97)
| U_98 != U_97 )
& ( U_98 = U_97
| bit1(U_98) != bit1(U_97) ) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
( ! [U_102,U_100] :
( bit1(U_102) = bit1(U_100)
| U_102 != U_100 )
& ! [U_101,U_99] :
( U_101 = U_99
| bit1(U_101) != bit1(U_99) ) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( U_101 = U_99
| bit1(U_101) != bit1(U_99) ),
inference(clausify,[status(thm)],[f_48_3]) ).
cnf(f_48_5,plain,
( bit1(U_102) = bit1(U_100)
| U_102 != U_100 ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [K_1,L_1] :
( ( bit0(K_1) = bit0(L_1)
| K_1 != L_1 )
& ( K_1 = L_1
| bit0(K_1) != bit0(L_1) ) ),
inference(fof_nnf,[status(thm)],[fact_48_rel__simps_I48_J]) ).
fof(f_49_2,plain,
! [U_104,U_103] :
( ( bit0(U_104) = bit0(U_103)
| U_104 != U_103 )
& ( U_104 = U_103
| bit0(U_104) != bit0(U_103) ) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
fof(f_49_3,plain,
( ! [U_108,U_106] :
( bit0(U_108) = bit0(U_106)
| U_108 != U_106 )
& ! [U_107,U_105] :
( U_107 = U_105
| bit0(U_107) != bit0(U_105) ) ),
inference(miniscope,[status(thm)],[f_49_2]) ).
cnf(f_49_4,plain,
( U_107 = U_105
| bit0(U_107) != bit0(U_105) ),
inference(clausify,[status(thm)],[f_49_3]) ).
cnf(f_49_5,plain,
( bit0(U_108) = bit0(U_106)
| U_108 != U_106 ),
inference(clausify,[status(thm)],[f_49_3]) ).
fof(f_50_1,plain,
! [A_1] :
( ( ord_less_int(plus_plus_int(A_1,A_1),zero_zero_int)
| ~ ord_less_int(A_1,zero_zero_int) )
& ( ord_less_int(A_1,zero_zero_int)
| ~ ord_less_int(plus_plus_int(A_1,A_1),zero_zero_int) ) ),
inference(fof_nnf,[status(thm)],[fact_49_even__less__0__iff]) ).
fof(f_50_2,plain,
! [U_109] :
( ( ord_less_int(plus_plus_int(U_109,U_109),zero_zero_int)
| ~ ord_less_int(U_109,zero_zero_int) )
& ( ord_less_int(U_109,zero_zero_int)
| ~ ord_less_int(plus_plus_int(U_109,U_109),zero_zero_int) ) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
( ! [U_111] :
( ord_less_int(plus_plus_int(U_111,U_111),zero_zero_int)
| ~ ord_less_int(U_111,zero_zero_int) )
& ! [U_110] :
( ord_less_int(U_110,zero_zero_int)
| ~ ord_less_int(plus_plus_int(U_110,U_110),zero_zero_int) ) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( ord_less_int(U_110,zero_zero_int)
| ~ ord_less_int(plus_plus_int(U_110,U_110),zero_zero_int) ),
inference(clausify,[status(thm)],[f_50_3]) ).
cnf(f_50_5,plain,
( ord_less_int(plus_plus_int(U_111,U_111),zero_zero_int)
| ~ ord_less_int(U_111,zero_zero_int) ),
inference(clausify,[status(thm)],[f_50_3]) ).
fof(f_51_1,plain,
! [Z1,Z2,Z3] : plus_plus_int(plus_plus_int(Z1,Z2),Z3) = plus_plus_int(Z1,plus_plus_int(Z2,Z3)),
inference(fof_nnf,[status(thm)],[fact_50_zadd__assoc]) ).
fof(f_51_2,plain,
! [U_114,U_113,U_112] : plus_plus_int(plus_plus_int(U_114,U_113),U_112) = plus_plus_int(U_114,plus_plus_int(U_113,U_112)),
inference(variable_rename,[status(thm)],[f_51_1]) ).
cnf(f_51_3,plain,
plus_plus_int(plus_plus_int(U_114,U_113),U_112) = plus_plus_int(U_114,plus_plus_int(U_113,U_112)),
inference(clausify,[status(thm)],[f_51_2]) ).
fof(f_52_1,plain,
! [X,Y,Z] : plus_plus_int(X,plus_plus_int(Y,Z)) = plus_plus_int(Y,plus_plus_int(X,Z)),
inference(fof_nnf,[status(thm)],[fact_51_zadd__left__commute]) ).
fof(f_52_2,plain,
! [U_117,U_116,U_115] : plus_plus_int(U_117,plus_plus_int(U_116,U_115)) = plus_plus_int(U_116,plus_plus_int(U_117,U_115)),
inference(variable_rename,[status(thm)],[f_52_1]) ).
cnf(f_52_3,plain,
plus_plus_int(U_117,plus_plus_int(U_116,U_115)) = plus_plus_int(U_116,plus_plus_int(U_117,U_115)),
inference(clausify,[status(thm)],[f_52_2]) ).
fof(f_53_1,plain,
! [Z,W_3] : plus_plus_int(Z,W_3) = plus_plus_int(W_3,Z),
inference(fof_nnf,[status(thm)],[fact_52_zadd__commute]) ).
fof(f_53_2,plain,
! [U_119,U_118] : plus_plus_int(U_119,U_118) = plus_plus_int(U_118,U_119),
inference(variable_rename,[status(thm)],[f_53_1]) ).
cnf(f_53_3,plain,
plus_plus_int(U_119,U_118) = plus_plus_int(U_118,U_119),
inference(clausify,[status(thm)],[f_53_2]) ).
fof(f_54_1,plain,
! [Ma,Na] :
( ( semiri1621563631at_int(Ma) = semiri1621563631at_int(Na)
| Ma != Na )
& ( Ma = Na
| semiri1621563631at_int(Ma) != semiri1621563631at_int(Na) ) ),
inference(fof_nnf,[status(thm)],[fact_53_int__int__eq]) ).
fof(f_54_2,plain,
! [U_121,U_120] :
( ( semiri1621563631at_int(U_121) = semiri1621563631at_int(U_120)
| U_121 != U_120 )
& ( U_121 = U_120
| semiri1621563631at_int(U_121) != semiri1621563631at_int(U_120) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_125,U_123] :
( semiri1621563631at_int(U_125) = semiri1621563631at_int(U_123)
| U_125 != U_123 )
& ! [U_124,U_122] :
( U_124 = U_122
| semiri1621563631at_int(U_124) != semiri1621563631at_int(U_122) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( U_124 = U_122
| semiri1621563631at_int(U_124) != semiri1621563631at_int(U_122) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( semiri1621563631at_int(U_125) = semiri1621563631at_int(U_123)
| U_125 != U_123 ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [Xa] :
( ( ord_less_int(number_number_of_int(Xa),zero_zero_int)
| ~ ord_less_int(Xa,pls) )
& ( ord_less_int(Xa,pls)
| ~ ord_less_int(number_number_of_int(Xa),zero_zero_int) ) ),
inference(fof_nnf,[status(thm)],[fact_54_less__special_I3_J]) ).
fof(f_55_2,plain,
! [U_126] :
( ( ord_less_int(number_number_of_int(U_126),zero_zero_int)
| ~ ord_less_int(U_126,pls) )
& ( ord_less_int(U_126,pls)
| ~ ord_less_int(number_number_of_int(U_126),zero_zero_int) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_128] :
( ord_less_int(number_number_of_int(U_128),zero_zero_int)
| ~ ord_less_int(U_128,pls) )
& ! [U_127] :
( ord_less_int(U_127,pls)
| ~ ord_less_int(number_number_of_int(U_127),zero_zero_int) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
cnf(f_55_4,plain,
( ord_less_int(U_127,pls)
| ~ ord_less_int(number_number_of_int(U_127),zero_zero_int) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_5,plain,
( ord_less_int(number_number_of_int(U_128),zero_zero_int)
| ~ ord_less_int(U_128,pls) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_1,plain,
! [Ya] :
( ( ord_less_int(zero_zero_int,number_number_of_int(Ya))
| ~ ord_less_int(pls,Ya) )
& ( ord_less_int(pls,Ya)
| ~ ord_less_int(zero_zero_int,number_number_of_int(Ya)) ) ),
inference(fof_nnf,[status(thm)],[fact_55_less__special_I1_J]) ).
fof(f_56_2,plain,
! [U_129] :
( ( ord_less_int(zero_zero_int,number_number_of_int(U_129))
| ~ ord_less_int(pls,U_129) )
& ( ord_less_int(pls,U_129)
| ~ ord_less_int(zero_zero_int,number_number_of_int(U_129)) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_131] :
( ord_less_int(zero_zero_int,number_number_of_int(U_131))
| ~ ord_less_int(pls,U_131) )
& ! [U_130] :
( ord_less_int(pls,U_130)
| ~ ord_less_int(zero_zero_int,number_number_of_int(U_130)) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( ord_less_int(pls,U_130)
| ~ ord_less_int(zero_zero_int,number_number_of_int(U_130)) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_5,plain,
( ord_less_int(zero_zero_int,number_number_of_int(U_131))
| ~ ord_less_int(pls,U_131) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
! [K_1] :
( ( ord_less_int(bit1(K_1),pls)
| ~ ord_less_int(K_1,pls) )
& ( ord_less_int(K_1,pls)
| ~ ord_less_int(bit1(K_1),pls) ) ),
inference(fof_nnf,[status(thm)],[fact_56_rel__simps_I12_J]) ).
fof(f_57_2,plain,
! [U_132] :
( ( ord_less_int(bit1(U_132),pls)
| ~ ord_less_int(U_132,pls) )
& ( ord_less_int(U_132,pls)
| ~ ord_less_int(bit1(U_132),pls) ) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
( ! [U_134] :
( ord_less_int(bit1(U_134),pls)
| ~ ord_less_int(U_134,pls) )
& ! [U_133] :
( ord_less_int(U_133,pls)
| ~ ord_less_int(bit1(U_133),pls) ) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( ord_less_int(U_133,pls)
| ~ ord_less_int(bit1(U_133),pls) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( ord_less_int(bit1(U_134),pls)
| ~ ord_less_int(U_134,pls) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [K1,K2] :
( ( ord_less_int(bit1(K1),bit0(K2))
| ~ ord_less_int(K1,K2) )
& ( ord_less_int(K1,K2)
| ~ ord_less_int(bit1(K1),bit0(K2)) ) ),
inference(fof_nnf,[status(thm)],[fact_57_less__int__code_I15_J]) ).
fof(f_58_2,plain,
! [U_136,U_135] :
( ( ord_less_int(bit1(U_136),bit0(U_135))
| ~ ord_less_int(U_136,U_135) )
& ( ord_less_int(U_136,U_135)
| ~ ord_less_int(bit1(U_136),bit0(U_135)) ) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
( ! [U_140,U_138] :
( ord_less_int(bit1(U_140),bit0(U_138))
| ~ ord_less_int(U_140,U_138) )
& ! [U_139,U_137] :
( ord_less_int(U_139,U_137)
| ~ ord_less_int(bit1(U_139),bit0(U_137)) ) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
cnf(f_58_4,plain,
( ord_less_int(U_139,U_137)
| ~ ord_less_int(bit1(U_139),bit0(U_137)) ),
inference(clausify,[status(thm)],[f_58_3]) ).
cnf(f_58_5,plain,
( ord_less_int(bit1(U_140),bit0(U_138))
| ~ ord_less_int(U_140,U_138) ),
inference(clausify,[status(thm)],[f_58_3]) ).
fof(f_59_1,plain,
! [K_1,L_1] :
( ( ord_less_int(bit1(K_1),bit0(L_1))
| ~ ord_less_int(K_1,L_1) )
& ( ord_less_int(K_1,L_1)
| ~ ord_less_int(bit1(K_1),bit0(L_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_58_rel__simps_I16_J]) ).
fof(f_59_2,plain,
! [U_142,U_141] :
( ( ord_less_int(bit1(U_142),bit0(U_141))
| ~ ord_less_int(U_142,U_141) )
& ( ord_less_int(U_142,U_141)
| ~ ord_less_int(bit1(U_142),bit0(U_141)) ) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
fof(f_59_3,plain,
( ! [U_146,U_144] :
( ord_less_int(bit1(U_146),bit0(U_144))
| ~ ord_less_int(U_146,U_144) )
& ! [U_145,U_143] :
( ord_less_int(U_145,U_143)
| ~ ord_less_int(bit1(U_145),bit0(U_143)) ) ),
inference(miniscope,[status(thm)],[f_59_2]) ).
cnf(f_59_4,plain,
( ord_less_int(U_145,U_143)
| ~ ord_less_int(bit1(U_145),bit0(U_143)) ),
inference(clausify,[status(thm)],[f_59_3]) ).
cnf(f_59_5,plain,
( ord_less_int(bit1(U_146),bit0(U_144))
| ~ ord_less_int(U_146,U_144) ),
inference(clausify,[status(thm)],[f_59_3]) ).
fof(f_60_1,plain,
! [K_1] :
( ( ord_less_int(bit0(K_1),pls)
| ~ ord_less_int(K_1,pls) )
& ( ord_less_int(K_1,pls)
| ~ ord_less_int(bit0(K_1),pls) ) ),
inference(fof_nnf,[status(thm)],[fact_59_rel__simps_I10_J]) ).
fof(f_60_2,plain,
! [U_147] :
( ( ord_less_int(bit0(U_147),pls)
| ~ ord_less_int(U_147,pls) )
& ( ord_less_int(U_147,pls)
| ~ ord_less_int(bit0(U_147),pls) ) ),
inference(variable_rename,[status(thm)],[f_60_1]) ).
fof(f_60_3,plain,
( ! [U_149] :
( ord_less_int(bit0(U_149),pls)
| ~ ord_less_int(U_149,pls) )
& ! [U_148] :
( ord_less_int(U_148,pls)
| ~ ord_less_int(bit0(U_148),pls) ) ),
inference(miniscope,[status(thm)],[f_60_2]) ).
cnf(f_60_4,plain,
( ord_less_int(U_148,pls)
| ~ ord_less_int(bit0(U_148),pls) ),
inference(clausify,[status(thm)],[f_60_3]) ).
cnf(f_60_5,plain,
( ord_less_int(bit0(U_149),pls)
| ~ ord_less_int(U_149,pls) ),
inference(clausify,[status(thm)],[f_60_3]) ).
fof(f_61_1,plain,
! [K_1] :
( ( ord_less_int(pls,bit0(K_1))
| ~ ord_less_int(pls,K_1) )
& ( ord_less_int(pls,K_1)
| ~ ord_less_int(pls,bit0(K_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_60_rel__simps_I4_J]) ).
fof(f_61_2,plain,
! [U_150] :
( ( ord_less_int(pls,bit0(U_150))
| ~ ord_less_int(pls,U_150) )
& ( ord_less_int(pls,U_150)
| ~ ord_less_int(pls,bit0(U_150)) ) ),
inference(variable_rename,[status(thm)],[f_61_1]) ).
fof(f_61_3,plain,
( ! [U_152] :
( ord_less_int(pls,bit0(U_152))
| ~ ord_less_int(pls,U_152) )
& ! [U_151] :
( ord_less_int(pls,U_151)
| ~ ord_less_int(pls,bit0(U_151)) ) ),
inference(miniscope,[status(thm)],[f_61_2]) ).
cnf(f_61_4,plain,
( ord_less_int(pls,U_151)
| ~ ord_less_int(pls,bit0(U_151)) ),
inference(clausify,[status(thm)],[f_61_3]) ).
cnf(f_61_5,plain,
( ord_less_int(pls,bit0(U_152))
| ~ ord_less_int(pls,U_152) ),
inference(clausify,[status(thm)],[f_61_3]) ).
fof(f_62_1,plain,
! [Wa] :
( ( ord_less_int(bit1(Wa),zero_zero_int)
| ~ ord_less_int(Wa,zero_zero_int) )
& ( ord_less_int(Wa,zero_zero_int)
| ~ ord_less_int(bit1(Wa),zero_zero_int) ) ),
inference(fof_nnf,[status(thm)],[fact_61_bin__less__0__simps_I4_J]) ).
fof(f_62_2,plain,
! [U_153] :
( ( ord_less_int(bit1(U_153),zero_zero_int)
| ~ ord_less_int(U_153,zero_zero_int) )
& ( ord_less_int(U_153,zero_zero_int)
| ~ ord_less_int(bit1(U_153),zero_zero_int) ) ),
inference(variable_rename,[status(thm)],[f_62_1]) ).
fof(f_62_3,plain,
( ! [U_155] :
( ord_less_int(bit1(U_155),zero_zero_int)
| ~ ord_less_int(U_155,zero_zero_int) )
& ! [U_154] :
( ord_less_int(U_154,zero_zero_int)
| ~ ord_less_int(bit1(U_154),zero_zero_int) ) ),
inference(miniscope,[status(thm)],[f_62_2]) ).
cnf(f_62_4,plain,
( ord_less_int(U_154,zero_zero_int)
| ~ ord_less_int(bit1(U_154),zero_zero_int) ),
inference(clausify,[status(thm)],[f_62_3]) ).
cnf(f_62_5,plain,
( ord_less_int(bit1(U_155),zero_zero_int)
| ~ ord_less_int(U_155,zero_zero_int) ),
inference(clausify,[status(thm)],[f_62_3]) ).
fof(f_63_1,plain,
~ ord_less_int(pls,zero_zero_int),
inference(fof_nnf,[status(thm)],[fact_62_bin__less__0__simps_I1_J]) ).
cnf(f_63_2,plain,
~ ord_less_int(pls,zero_zero_int),
inference(clausify,[status(thm)],[f_63_1]) ).
fof(f_64_1,plain,
! [Wa] :
( ( ord_less_int(bit0(Wa),zero_zero_int)
| ~ ord_less_int(Wa,zero_zero_int) )
& ( ord_less_int(Wa,zero_zero_int)
| ~ ord_less_int(bit0(Wa),zero_zero_int) ) ),
inference(fof_nnf,[status(thm)],[fact_63_bin__less__0__simps_I3_J]) ).
fof(f_64_2,plain,
! [U_156] :
( ( ord_less_int(bit0(U_156),zero_zero_int)
| ~ ord_less_int(U_156,zero_zero_int) )
& ( ord_less_int(U_156,zero_zero_int)
| ~ ord_less_int(bit0(U_156),zero_zero_int) ) ),
inference(variable_rename,[status(thm)],[f_64_1]) ).
fof(f_64_3,plain,
( ! [U_158] :
( ord_less_int(bit0(U_158),zero_zero_int)
| ~ ord_less_int(U_158,zero_zero_int) )
& ! [U_157] :
( ord_less_int(U_157,zero_zero_int)
| ~ ord_less_int(bit0(U_157),zero_zero_int) ) ),
inference(miniscope,[status(thm)],[f_64_2]) ).
cnf(f_64_4,plain,
( ord_less_int(U_157,zero_zero_int)
| ~ ord_less_int(bit0(U_157),zero_zero_int) ),
inference(clausify,[status(thm)],[f_64_3]) ).
cnf(f_64_5,plain,
( ord_less_int(bit0(U_158),zero_zero_int)
| ~ ord_less_int(U_158,zero_zero_int) ),
inference(clausify,[status(thm)],[f_64_3]) ).
fof(f_65_1,plain,
ord_less_int(zero_zero_int,one_one_int),
inference(fof_nnf,[status(thm)],[fact_64_int__0__less__1]) ).
cnf(f_65_2,plain,
ord_less_int(zero_zero_int,one_one_int),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_1,plain,
! [Wa,Z_2] :
( ( ord_less_int(Wa,plus_plus_int(Z_2,one_one_int))
| ( Wa != Z_2
& ~ ord_less_int(Wa,Z_2) ) )
& ( Wa = Z_2
| ord_less_int(Wa,Z_2)
| ~ ord_less_int(Wa,plus_plus_int(Z_2,one_one_int)) ) ),
inference(fof_nnf,[status(thm)],[fact_65_zless__add1__eq]) ).
fof(f_66_2,plain,
! [U_160,U_159] :
( ( ord_less_int(U_160,plus_plus_int(U_159,one_one_int))
| ( U_160 != U_159
& ~ ord_less_int(U_160,U_159) ) )
& ( U_160 = U_159
| ord_less_int(U_160,U_159)
| ~ ord_less_int(U_160,plus_plus_int(U_159,one_one_int)) ) ),
inference(variable_rename,[status(thm)],[f_66_1]) ).
fof(f_66_3,plain,
( ! [U_164,U_162] :
( ord_less_int(U_164,plus_plus_int(U_162,one_one_int))
| ( U_164 != U_162
& ~ ord_less_int(U_164,U_162) ) )
& ! [U_163,U_161] :
( U_163 = U_161
| ord_less_int(U_163,U_161)
| ~ ord_less_int(U_163,plus_plus_int(U_161,one_one_int)) ) ),
inference(miniscope,[status(thm)],[f_66_2]) ).
cnf(f_66_4,plain,
( U_163 = U_161
| ord_less_int(U_163,U_161)
| ~ ord_less_int(U_163,plus_plus_int(U_161,one_one_int)) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_5,plain,
( ~ ord_less_int(U_164,U_162)
| ord_less_int(U_164,plus_plus_int(U_162,one_one_int)) ),
inference(clausify,[status(thm)],[f_66_3]) ).
cnf(f_66_6,plain,
( U_164 != U_162
| ord_less_int(U_164,plus_plus_int(U_162,one_one_int)) ),
inference(clausify,[status(thm)],[f_66_3]) ).
fof(f_67_1,plain,
! [K] : ~ ord_less_int(semiri1621563631at_int(K),zero_zero_int),
inference(fof_nnf,[status(thm)],[fact_66_int__less__0__conv]) ).
fof(f_67_2,plain,
! [U_165] : ~ ord_less_int(semiri1621563631at_int(U_165),zero_zero_int),
inference(variable_rename,[status(thm)],[f_67_1]) ).
cnf(f_67_3,plain,
~ ord_less_int(semiri1621563631at_int(U_165),zero_zero_int),
inference(clausify,[status(thm)],[f_67_2]) ).
fof(f_68_1,plain,
! [Xa] :
( ( ord_less_int(number_number_of_int(Xa),one_one_int)
| ~ ord_less_int(Xa,bit1(pls)) )
& ( ord_less_int(Xa,bit1(pls))
| ~ ord_less_int(number_number_of_int(Xa),one_one_int) ) ),
inference(fof_nnf,[status(thm)],[fact_67_less__special_I4_J]) ).
fof(f_68_2,plain,
! [U_166] :
( ( ord_less_int(number_number_of_int(U_166),one_one_int)
| ~ ord_less_int(U_166,bit1(pls)) )
& ( ord_less_int(U_166,bit1(pls))
| ~ ord_less_int(number_number_of_int(U_166),one_one_int) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_168] :
( ord_less_int(number_number_of_int(U_168),one_one_int)
| ~ ord_less_int(U_168,bit1(pls)) )
& ! [U_167] :
( ord_less_int(U_167,bit1(pls))
| ~ ord_less_int(number_number_of_int(U_167),one_one_int) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ord_less_int(U_167,bit1(pls))
| ~ ord_less_int(number_number_of_int(U_167),one_one_int) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( ord_less_int(number_number_of_int(U_168),one_one_int)
| ~ ord_less_int(U_168,bit1(pls)) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
! [Ya] :
( ( ord_less_int(one_one_int,number_number_of_int(Ya))
| ~ ord_less_int(bit1(pls),Ya) )
& ( ord_less_int(bit1(pls),Ya)
| ~ ord_less_int(one_one_int,number_number_of_int(Ya)) ) ),
inference(fof_nnf,[status(thm)],[fact_68_less__special_I2_J]) ).
fof(f_69_2,plain,
! [U_169] :
( ( ord_less_int(one_one_int,number_number_of_int(U_169))
| ~ ord_less_int(bit1(pls),U_169) )
& ( ord_less_int(bit1(pls),U_169)
| ~ ord_less_int(one_one_int,number_number_of_int(U_169)) ) ),
inference(variable_rename,[status(thm)],[f_69_1]) ).
fof(f_69_3,plain,
( ! [U_171] :
( ord_less_int(one_one_int,number_number_of_int(U_171))
| ~ ord_less_int(bit1(pls),U_171) )
& ! [U_170] :
( ord_less_int(bit1(pls),U_170)
| ~ ord_less_int(one_one_int,number_number_of_int(U_170)) ) ),
inference(miniscope,[status(thm)],[f_69_2]) ).
cnf(f_69_4,plain,
( ord_less_int(bit1(pls),U_170)
| ~ ord_less_int(one_one_int,number_number_of_int(U_170)) ),
inference(clausify,[status(thm)],[f_69_3]) ).
cnf(f_69_5,plain,
( ord_less_int(one_one_int,number_number_of_int(U_171))
| ~ ord_less_int(bit1(pls),U_171) ),
inference(clausify,[status(thm)],[f_69_3]) ).
fof(f_70_1,plain,
! [Z_2] :
( ( ord_less_int(plus_plus_int(plus_plus_int(one_one_int,Z_2),Z_2),zero_zero_int)
| ~ ord_less_int(Z_2,zero_zero_int) )
& ( ord_less_int(Z_2,zero_zero_int)
| ~ ord_less_int(plus_plus_int(plus_plus_int(one_one_int,Z_2),Z_2),zero_zero_int) ) ),
inference(fof_nnf,[status(thm)],[fact_69_odd__less__0]) ).
fof(f_70_2,plain,
! [U_172] :
( ( ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_172),U_172),zero_zero_int)
| ~ ord_less_int(U_172,zero_zero_int) )
& ( ord_less_int(U_172,zero_zero_int)
| ~ ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_172),U_172),zero_zero_int) ) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
fof(f_70_3,plain,
( ! [U_174] :
( ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_174),U_174),zero_zero_int)
| ~ ord_less_int(U_174,zero_zero_int) )
& ! [U_173] :
( ord_less_int(U_173,zero_zero_int)
| ~ ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_173),U_173),zero_zero_int) ) ),
inference(miniscope,[status(thm)],[f_70_2]) ).
cnf(f_70_4,plain,
( ord_less_int(U_173,zero_zero_int)
| ~ ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_173),U_173),zero_zero_int) ),
inference(clausify,[status(thm)],[f_70_3]) ).
cnf(f_70_5,plain,
( ord_less_int(plus_plus_int(plus_plus_int(one_one_int,U_174),U_174),zero_zero_int)
| ~ ord_less_int(U_174,zero_zero_int) ),
inference(clausify,[status(thm)],[f_70_3]) ).
fof(f_71_1,plain,
! [A_1] :
( ( plus_plus_int(A_1,A_1) = zero_zero_int
| A_1 != zero_zero_int )
& ( A_1 = zero_zero_int
| plus_plus_int(A_1,A_1) != zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[fact_70_double__eq__0__iff]) ).
fof(f_71_2,plain,
! [U_175] :
( ( plus_plus_int(U_175,U_175) = zero_zero_int
| U_175 != zero_zero_int )
& ( U_175 = zero_zero_int
| plus_plus_int(U_175,U_175) != zero_zero_int ) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
fof(f_71_3,plain,
( ! [U_177] :
( plus_plus_int(U_177,U_177) = zero_zero_int
| U_177 != zero_zero_int )
& ! [U_176] :
( U_176 = zero_zero_int
| plus_plus_int(U_176,U_176) != zero_zero_int ) ),
inference(miniscope,[status(thm)],[f_71_2]) ).
cnf(f_71_4,plain,
( U_176 = zero_zero_int
| plus_plus_int(U_176,U_176) != zero_zero_int ),
inference(clausify,[status(thm)],[f_71_3]) ).
cnf(f_71_5,plain,
( plus_plus_int(U_177,U_177) = zero_zero_int
| U_177 != zero_zero_int ),
inference(clausify,[status(thm)],[f_71_3]) ).
fof(f_72_1,plain,
! [K] : bit1(K) != pls,
inference(fof_nnf,[status(thm)],[fact_71_rel__simps_I46_J]) ).
fof(f_72_2,plain,
! [U_178] : bit1(U_178) != pls,
inference(variable_rename,[status(thm)],[f_72_1]) ).
cnf(f_72_3,plain,
bit1(U_178) != pls,
inference(clausify,[status(thm)],[f_72_2]) ).
fof(f_73_1,plain,
! [L] : pls != bit1(L),
inference(fof_nnf,[status(thm)],[fact_72_rel__simps_I39_J]) ).
fof(f_73_2,plain,
! [U_179] : pls != bit1(U_179),
inference(variable_rename,[status(thm)],[f_73_1]) ).
cnf(f_73_3,plain,
pls != bit1(U_179),
inference(clausify,[status(thm)],[f_73_2]) ).
fof(f_74_1,plain,
! [K,L] : bit1(K) != bit0(L),
inference(fof_nnf,[status(thm)],[fact_73_rel__simps_I50_J]) ).
fof(f_74_2,plain,
! [U_181,U_180] : bit1(U_181) != bit0(U_180),
inference(variable_rename,[status(thm)],[f_74_1]) ).
cnf(f_74_3,plain,
bit1(U_181) != bit0(U_180),
inference(clausify,[status(thm)],[f_74_2]) ).
fof(f_75_1,plain,
! [K,L] : bit0(K) != bit1(L),
inference(fof_nnf,[status(thm)],[fact_74_rel__simps_I49_J]) ).
fof(f_75_2,plain,
! [U_183,U_182] : bit0(U_183) != bit1(U_182),
inference(variable_rename,[status(thm)],[f_75_1]) ).
cnf(f_75_3,plain,
bit0(U_183) != bit1(U_182),
inference(clausify,[status(thm)],[f_75_2]) ).
fof(f_76_1,plain,
! [K_1] :
( ( bit0(K_1) = pls
| K_1 != pls )
& ( K_1 = pls
| bit0(K_1) != pls ) ),
inference(fof_nnf,[status(thm)],[fact_75_rel__simps_I44_J]) ).
fof(f_76_2,plain,
! [U_184] :
( ( bit0(U_184) = pls
| U_184 != pls )
& ( U_184 = pls
| bit0(U_184) != pls ) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
fof(f_76_3,plain,
( ! [U_186] :
( bit0(U_186) = pls
| U_186 != pls )
& ! [U_185] :
( U_185 = pls
| bit0(U_185) != pls ) ),
inference(miniscope,[status(thm)],[f_76_2]) ).
cnf(f_76_4,plain,
( U_185 = pls
| bit0(U_185) != pls ),
inference(clausify,[status(thm)],[f_76_3]) ).
cnf(f_76_5,plain,
( bit0(U_186) = pls
| U_186 != pls ),
inference(clausify,[status(thm)],[f_76_3]) ).
fof(f_77_1,plain,
! [L_1] :
( ( pls = bit0(L_1)
| pls != L_1 )
& ( pls = L_1
| pls != bit0(L_1) ) ),
inference(fof_nnf,[status(thm)],[fact_76_rel__simps_I38_J]) ).
fof(f_77_2,plain,
! [U_187] :
( ( pls = bit0(U_187)
| pls != U_187 )
& ( pls = U_187
| pls != bit0(U_187) ) ),
inference(variable_rename,[status(thm)],[f_77_1]) ).
fof(f_77_3,plain,
( ! [U_189] :
( pls = bit0(U_189)
| pls != U_189 )
& ! [U_188] :
( pls = U_188
| pls != bit0(U_188) ) ),
inference(miniscope,[status(thm)],[f_77_2]) ).
cnf(f_77_4,plain,
( pls = U_188
| pls != bit0(U_188) ),
inference(clausify,[status(thm)],[f_77_3]) ).
cnf(f_77_5,plain,
( pls = bit0(U_189)
| pls != U_189 ),
inference(clausify,[status(thm)],[f_77_3]) ).
fof(f_78_1,plain,
bit0(pls) = pls,
inference(fof_nnf,[status(thm)],[fact_77_Bit0__Pls]) ).
cnf(f_78_2,plain,
bit0(pls) = pls,
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
pls = zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_78_Pls__def]) ).
cnf(f_79_2,plain,
pls = zero_zero_int,
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
zero_zero_int != one_one_int,
inference(fof_nnf,[status(thm)],[fact_79_int__0__neq__1]) ).
cnf(f_80_2,plain,
zero_zero_int != one_one_int,
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,plain,
! [K] : plus_plus_int(K,pls) = K,
inference(fof_nnf,[status(thm)],[fact_80_add__Pls__right]) ).
fof(f_81_2,plain,
! [U_190] : plus_plus_int(U_190,pls) = U_190,
inference(variable_rename,[status(thm)],[f_81_1]) ).
cnf(f_81_3,plain,
plus_plus_int(U_190,pls) = U_190,
inference(clausify,[status(thm)],[f_81_2]) ).
fof(f_82_1,plain,
! [K] : plus_plus_int(pls,K) = K,
inference(fof_nnf,[status(thm)],[fact_81_add__Pls]) ).
fof(f_82_2,plain,
! [U_191] : plus_plus_int(pls,U_191) = U_191,
inference(variable_rename,[status(thm)],[f_82_1]) ).
cnf(f_82_3,plain,
plus_plus_int(pls,U_191) = U_191,
inference(clausify,[status(thm)],[f_82_2]) ).
fof(f_83_1,plain,
! [K,L] : plus_plus_int(bit0(K),bit0(L)) = bit0(plus_plus_int(K,L)),
inference(fof_nnf,[status(thm)],[fact_82_add__Bit0__Bit0]) ).
fof(f_83_2,plain,
! [U_193,U_192] : plus_plus_int(bit0(U_193),bit0(U_192)) = bit0(plus_plus_int(U_193,U_192)),
inference(variable_rename,[status(thm)],[f_83_1]) ).
cnf(f_83_3,plain,
plus_plus_int(bit0(U_193),bit0(U_192)) = bit0(plus_plus_int(U_193,U_192)),
inference(clausify,[status(thm)],[f_83_2]) ).
fof(f_84_1,plain,
! [K] : bit0(K) = plus_plus_int(K,K),
inference(fof_nnf,[status(thm)],[fact_83_Bit0__def]) ).
fof(f_84_2,plain,
! [U_194] : bit0(U_194) = plus_plus_int(U_194,U_194),
inference(variable_rename,[status(thm)],[f_84_1]) ).
cnf(f_84_3,plain,
bit0(U_194) = plus_plus_int(U_194,U_194),
inference(clausify,[status(thm)],[f_84_2]) ).
fof(f_85_1,plain,
! [Z] : plus_plus_int(Z,zero_zero_int) = Z,
inference(fof_nnf,[status(thm)],[fact_84_zadd__0__right]) ).
fof(f_85_2,plain,
! [U_195] : plus_plus_int(U_195,zero_zero_int) = U_195,
inference(variable_rename,[status(thm)],[f_85_1]) ).
cnf(f_85_3,plain,
plus_plus_int(U_195,zero_zero_int) = U_195,
inference(clausify,[status(thm)],[f_85_2]) ).
fof(f_86_1,plain,
! [Z] : plus_plus_int(zero_zero_int,Z) = Z,
inference(fof_nnf,[status(thm)],[fact_85_zadd__0]) ).
fof(f_86_2,plain,
! [U_196] : plus_plus_int(zero_zero_int,U_196) = U_196,
inference(variable_rename,[status(thm)],[f_86_1]) ).
cnf(f_86_3,plain,
plus_plus_int(zero_zero_int,U_196) = U_196,
inference(clausify,[status(thm)],[f_86_2]) ).
fof(f_87_1,plain,
number_number_of_int(pls) = zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_86_semiring__numeral__0__eq__0]) ).
cnf(f_87_2,plain,
number_number_of_int(pls) = zero_zero_int,
inference(clausify,[status(thm)],[f_87_1]) ).
fof(f_88_1,plain,
number_number_of_nat(pls) = zero_zero_nat,
inference(fof_nnf,[status(thm)],[fact_87_semiring__numeral__0__eq__0]) ).
cnf(f_88_2,plain,
number_number_of_nat(pls) = zero_zero_nat,
inference(clausify,[status(thm)],[f_88_1]) ).
fof(f_89_1,plain,
number_number_of_int(pls) = zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_88_number__of__Pls]) ).
cnf(f_89_2,plain,
number_number_of_int(pls) = zero_zero_int,
inference(clausify,[status(thm)],[f_89_1]) ).
fof(f_90_1,plain,
zero_zero_int = number_number_of_int(pls),
inference(fof_nnf,[status(thm)],[fact_89_semiring__norm_I112_J]) ).
cnf(f_90_2,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[f_90_1]) ).
fof(f_91_1,plain,
! [A_3] : plus_plus_int(number_number_of_int(pls),A_3) = A_3,
inference(fof_nnf,[status(thm)],[fact_90_add__numeral__0]) ).
fof(f_91_2,plain,
! [U_197] : plus_plus_int(number_number_of_int(pls),U_197) = U_197,
inference(variable_rename,[status(thm)],[f_91_1]) ).
cnf(f_91_3,plain,
plus_plus_int(number_number_of_int(pls),U_197) = U_197,
inference(clausify,[status(thm)],[f_91_2]) ).
fof(f_92_1,plain,
! [A_2] : plus_plus_int(A_2,number_number_of_int(pls)) = A_2,
inference(fof_nnf,[status(thm)],[fact_91_add__numeral__0__right]) ).
fof(f_92_2,plain,
! [U_198] : plus_plus_int(U_198,number_number_of_int(pls)) = U_198,
inference(variable_rename,[status(thm)],[f_92_1]) ).
cnf(f_92_3,plain,
plus_plus_int(U_198,number_number_of_int(pls)) = U_198,
inference(clausify,[status(thm)],[f_92_2]) ).
fof(f_93_1,plain,
! [A_1,Wa] :
( ( power_power_int(A_1,number_number_of_nat(Wa)) = zero_zero_int
| number_number_of_nat(Wa) = zero_zero_nat
| A_1 != zero_zero_int )
& ( ( number_number_of_nat(Wa) != zero_zero_nat
& A_1 = zero_zero_int )
| power_power_int(A_1,number_number_of_nat(Wa)) != zero_zero_int ) ),
inference(fof_nnf,[status(thm)],[fact_92_power__eq__0__iff__number__of]) ).
fof(f_93_2,plain,
! [U_200,U_199] :
( ( power_power_int(U_200,number_number_of_nat(U_199)) = zero_zero_int
| number_number_of_nat(U_199) = zero_zero_nat
| U_200 != zero_zero_int )
& ( ( number_number_of_nat(U_199) != zero_zero_nat
& U_200 = zero_zero_int )
| power_power_int(U_200,number_number_of_nat(U_199)) != zero_zero_int ) ),
inference(variable_rename,[status(thm)],[f_93_1]) ).
fof(f_93_3,plain,
( ! [U_204,U_202] :
( power_power_int(U_204,number_number_of_nat(U_202)) = zero_zero_int
| number_number_of_nat(U_202) = zero_zero_nat
| U_204 != zero_zero_int )
& ! [U_203,U_201] :
( ( number_number_of_nat(U_201) != zero_zero_nat
& U_203 = zero_zero_int )
| power_power_int(U_203,number_number_of_nat(U_201)) != zero_zero_int ) ),
inference(miniscope,[status(thm)],[f_93_2]) ).
cnf(f_93_4,plain,
( U_203 = zero_zero_int
| power_power_int(U_203,number_number_of_nat(U_201)) != zero_zero_int ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_5,plain,
( number_number_of_nat(U_201) != zero_zero_nat
| power_power_int(U_203,number_number_of_nat(U_201)) != zero_zero_int ),
inference(clausify,[status(thm)],[f_93_3]) ).
cnf(f_93_6,plain,
( power_power_int(U_204,number_number_of_nat(U_202)) = zero_zero_int
| number_number_of_nat(U_202) = zero_zero_nat
| U_204 != zero_zero_int ),
inference(clausify,[status(thm)],[f_93_3]) ).
fof(f_94_1,plain,
! [A_1,Wa] :
( ( power_power_nat(A_1,number_number_of_nat(Wa)) = zero_zero_nat
| number_number_of_nat(Wa) = zero_zero_nat
| A_1 != zero_zero_nat )
& ( ( number_number_of_nat(Wa) != zero_zero_nat
& A_1 = zero_zero_nat )
| power_power_nat(A_1,number_number_of_nat(Wa)) != zero_zero_nat ) ),
inference(fof_nnf,[status(thm)],[fact_93_power__eq__0__iff__number__of]) ).
fof(f_94_2,plain,
! [U_206,U_205] :
( ( power_power_nat(U_206,number_number_of_nat(U_205)) = zero_zero_nat
| number_number_of_nat(U_205) = zero_zero_nat
| U_206 != zero_zero_nat )
& ( ( number_number_of_nat(U_205) != zero_zero_nat
& U_206 = zero_zero_nat )
| power_power_nat(U_206,number_number_of_nat(U_205)) != zero_zero_nat ) ),
inference(variable_rename,[status(thm)],[f_94_1]) ).
fof(f_94_3,plain,
( ! [U_210,U_208] :
( power_power_nat(U_210,number_number_of_nat(U_208)) = zero_zero_nat
| number_number_of_nat(U_208) = zero_zero_nat
| U_210 != zero_zero_nat )
& ! [U_209,U_207] :
( ( number_number_of_nat(U_207) != zero_zero_nat
& U_209 = zero_zero_nat )
| power_power_nat(U_209,number_number_of_nat(U_207)) != zero_zero_nat ) ),
inference(miniscope,[status(thm)],[f_94_2]) ).
cnf(f_94_4,plain,
( U_209 = zero_zero_nat
| power_power_nat(U_209,number_number_of_nat(U_207)) != zero_zero_nat ),
inference(clausify,[status(thm)],[f_94_3]) ).
cnf(f_94_5,plain,
( number_number_of_nat(U_207) != zero_zero_nat
| power_power_nat(U_209,number_number_of_nat(U_207)) != zero_zero_nat ),
inference(clausify,[status(thm)],[f_94_3]) ).
cnf(f_94_6,plain,
( power_power_nat(U_210,number_number_of_nat(U_208)) = zero_zero_nat
| number_number_of_nat(U_208) = zero_zero_nat
| U_210 != zero_zero_nat ),
inference(clausify,[status(thm)],[f_94_3]) ).
fof(f_95_1,plain,
! [V_2,W_2,Z_1] : plus_plus_int(number_number_of_int(V_2),plus_plus_int(number_number_of_int(W_2),Z_1)) = plus_plus_int(number_number_of_int(plus_plus_int(V_2,W_2)),Z_1),
inference(fof_nnf,[status(thm)],[fact_94_add__number__of__left]) ).
fof(f_95_2,plain,
! [U_213,U_212,U_211] : plus_plus_int(number_number_of_int(U_213),plus_plus_int(number_number_of_int(U_212),U_211)) = plus_plus_int(number_number_of_int(plus_plus_int(U_213,U_212)),U_211),
inference(variable_rename,[status(thm)],[f_95_1]) ).
cnf(f_95_3,plain,
plus_plus_int(number_number_of_int(U_213),plus_plus_int(number_number_of_int(U_212),U_211)) = plus_plus_int(number_number_of_int(plus_plus_int(U_213,U_212)),U_211),
inference(clausify,[status(thm)],[f_95_2]) ).
fof(f_96_1,plain,
! [V_1,W_1] : plus_plus_int(number_number_of_int(V_1),number_number_of_int(W_1)) = number_number_of_int(plus_plus_int(V_1,W_1)),
inference(fof_nnf,[status(thm)],[fact_95_add__number__of__eq]) ).
fof(f_96_2,plain,
! [U_215,U_214] : plus_plus_int(number_number_of_int(U_215),number_number_of_int(U_214)) = number_number_of_int(plus_plus_int(U_215,U_214)),
inference(variable_rename,[status(thm)],[f_96_1]) ).
cnf(f_96_3,plain,
plus_plus_int(number_number_of_int(U_215),number_number_of_int(U_214)) = number_number_of_int(plus_plus_int(U_215,U_214)),
inference(clausify,[status(thm)],[f_96_2]) ).
fof(f_97_1,plain,
! [V,W] : number_number_of_int(plus_plus_int(V,W)) = plus_plus_int(number_number_of_int(V),number_number_of_int(W)),
inference(fof_nnf,[status(thm)],[fact_96_number__of__add]) ).
fof(f_97_2,plain,
! [U_217,U_216] : number_number_of_int(plus_plus_int(U_217,U_216)) = plus_plus_int(number_number_of_int(U_217),number_number_of_int(U_216)),
inference(variable_rename,[status(thm)],[f_97_1]) ).
cnf(f_97_3,plain,
number_number_of_int(plus_plus_int(U_217,U_216)) = plus_plus_int(number_number_of_int(U_217),number_number_of_int(U_216)),
inference(clausify,[status(thm)],[f_97_2]) ).
fof(f_98_1,plain,
! [K,L] : plus_plus_int(bit1(K),bit0(L)) = bit1(plus_plus_int(K,L)),
inference(fof_nnf,[status(thm)],[fact_97_add__Bit1__Bit0]) ).
fof(f_98_2,plain,
! [U_219,U_218] : plus_plus_int(bit1(U_219),bit0(U_218)) = bit1(plus_plus_int(U_219,U_218)),
inference(variable_rename,[status(thm)],[f_98_1]) ).
cnf(f_98_3,plain,
plus_plus_int(bit1(U_219),bit0(U_218)) = bit1(plus_plus_int(U_219,U_218)),
inference(clausify,[status(thm)],[f_98_2]) ).
fof(f_99_1,plain,
! [K,L] : plus_plus_int(bit0(K),bit1(L)) = bit1(plus_plus_int(K,L)),
inference(fof_nnf,[status(thm)],[fact_98_add__Bit0__Bit1]) ).
fof(f_99_2,plain,
! [U_221,U_220] : plus_plus_int(bit0(U_221),bit1(U_220)) = bit1(plus_plus_int(U_221,U_220)),
inference(variable_rename,[status(thm)],[f_99_1]) ).
cnf(f_99_3,plain,
plus_plus_int(bit0(U_221),bit1(U_220)) = bit1(plus_plus_int(U_221,U_220)),
inference(clausify,[status(thm)],[f_99_2]) ).
fof(f_100_1,plain,
! [K] : bit1(K) = plus_plus_int(plus_plus_int(one_one_int,K),K),
inference(fof_nnf,[status(thm)],[fact_99_Bit1__def]) ).
fof(f_100_2,plain,
! [U_222] : bit1(U_222) = plus_plus_int(plus_plus_int(one_one_int,U_222),U_222),
inference(variable_rename,[status(thm)],[f_100_1]) ).
cnf(f_100_3,plain,
bit1(U_222) = plus_plus_int(plus_plus_int(one_one_int,U_222),U_222),
inference(clausify,[status(thm)],[f_100_2]) ).
fof(f_101_1,plain,
! [Z] : plus_plus_int(plus_plus_int(one_one_int,Z),Z) != zero_zero_int,
inference(fof_nnf,[status(thm)],[fact_100_odd__nonzero]) ).
fof(f_101_2,plain,
! [U_223] : plus_plus_int(plus_plus_int(one_one_int,U_223),U_223) != zero_zero_int,
inference(variable_rename,[status(thm)],[f_101_1]) ).
cnf(f_101_3,plain,
plus_plus_int(plus_plus_int(one_one_int,U_223),U_223) != zero_zero_int,
inference(clausify,[status(thm)],[f_101_2]) ).
fof(f_102_1,plain,
! [N] : number_number_of_nat(semiri1621563631at_int(N)) = semiri984289939at_nat(N),
inference(fof_nnf,[status(thm)],[fact_101_number__of__int]) ).
fof(f_102_2,plain,
! [U_224] : number_number_of_nat(semiri1621563631at_int(U_224)) = semiri984289939at_nat(U_224),
inference(variable_rename,[status(thm)],[f_102_1]) ).
cnf(f_102_3,plain,
number_number_of_nat(semiri1621563631at_int(U_224)) = semiri984289939at_nat(U_224),
inference(clausify,[status(thm)],[f_102_2]) ).
fof(f_103_1,plain,
! [N] : number_number_of_int(semiri1621563631at_int(N)) = semiri1621563631at_int(N),
inference(fof_nnf,[status(thm)],[fact_102_number__of__int]) ).
fof(f_103_2,plain,
! [U_225] : number_number_of_int(semiri1621563631at_int(U_225)) = semiri1621563631at_int(U_225),
inference(variable_rename,[status(thm)],[f_103_1]) ).
cnf(f_103_3,plain,
number_number_of_int(semiri1621563631at_int(U_225)) = semiri1621563631at_int(U_225),
inference(clausify,[status(thm)],[f_103_2]) ).
fof(f_104_1,plain,
! [A_1] :
( ( ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))
| A_1 = zero_zero_int )
& ( A_1 != zero_zero_int
| ~ ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(fof_nnf,[status(thm)],[fact_103_zero__less__power2]) ).
fof(f_104_2,plain,
! [U_226] :
( ( ord_less_int(zero_zero_int,power_power_int(U_226,number_number_of_nat(bit0(bit1(pls)))))
| U_226 = zero_zero_int )
& ( U_226 != zero_zero_int
| ~ ord_less_int(zero_zero_int,power_power_int(U_226,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
fof(f_104_3,plain,
( ! [U_228] :
( ord_less_int(zero_zero_int,power_power_int(U_228,number_number_of_nat(bit0(bit1(pls)))))
| U_228 = zero_zero_int )
& ! [U_227] :
( U_227 != zero_zero_int
| ~ ord_less_int(zero_zero_int,power_power_int(U_227,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(miniscope,[status(thm)],[f_104_2]) ).
cnf(f_104_4,plain,
( U_227 != zero_zero_int
| ~ ord_less_int(zero_zero_int,power_power_int(U_227,number_number_of_nat(bit0(bit1(pls))))) ),
inference(clausify,[status(thm)],[f_104_3]) ).
cnf(f_104_5,plain,
( ord_less_int(zero_zero_int,power_power_int(U_228,number_number_of_nat(bit0(bit1(pls)))))
| U_228 = zero_zero_int ),
inference(clausify,[status(thm)],[f_104_3]) ).
fof(f_105_1,plain,
! [A] : ~ ord_less_int(power_power_int(A,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(fof_nnf,[status(thm)],[fact_104_power2__less__0]) ).
fof(f_105_2,plain,
! [U_229] : ~ ord_less_int(power_power_int(U_229,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(variable_rename,[status(thm)],[f_105_1]) ).
cnf(f_105_3,plain,
~ ord_less_int(power_power_int(U_229,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(clausify,[status(thm)],[f_105_2]) ).
fof(f_106_1,plain,
! [Xa,Ya] :
( ( ord_less_int(zero_zero_int,plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls))))))
| ( Ya = zero_zero_int
& Xa = zero_zero_int ) )
& ( Ya != zero_zero_int
| Xa != zero_zero_int
| ~ ord_less_int(zero_zero_int,plus_plus_int(power_power_int(Xa,number_number_of_nat(bit0(bit1(pls)))),power_power_int(Ya,number_number_of_nat(bit0(bit1(pls)))))) ) ),
inference(fof_nnf,[status(thm)],[fact_105_sum__power2__gt__zero__iff]) ).
fof(f_106_2,plain,
! [U_231,U_230] :
( ( ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_231,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_230,number_number_of_nat(bit0(bit1(pls))))))
| ( U_230 = zero_zero_int
& U_231 = zero_zero_int ) )
& ( U_230 != zero_zero_int
| U_231 != zero_zero_int
| ~ ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_231,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_230,number_number_of_nat(bit0(bit1(pls)))))) ) ),
inference(variable_rename,[status(thm)],[f_106_1]) ).
fof(f_106_3,plain,
( ! [U_235,U_233] :
( ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_235,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_233,number_number_of_nat(bit0(bit1(pls))))))
| ( U_233 = zero_zero_int
& U_235 = zero_zero_int ) )
& ! [U_234,U_232] :
( U_232 != zero_zero_int
| U_234 != zero_zero_int
| ~ ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_234,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_232,number_number_of_nat(bit0(bit1(pls)))))) ) ),
inference(miniscope,[status(thm)],[f_106_2]) ).
cnf(f_106_4,plain,
( U_232 != zero_zero_int
| U_234 != zero_zero_int
| ~ ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_234,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_232,number_number_of_nat(bit0(bit1(pls)))))) ),
inference(clausify,[status(thm)],[f_106_3]) ).
cnf(f_106_5,plain,
( U_235 = zero_zero_int
| ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_235,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_233,number_number_of_nat(bit0(bit1(pls)))))) ),
inference(clausify,[status(thm)],[f_106_3]) ).
cnf(f_106_6,plain,
( U_233 = zero_zero_int
| ord_less_int(zero_zero_int,plus_plus_int(power_power_int(U_235,number_number_of_nat(bit0(bit1(pls)))),power_power_int(U_233,number_number_of_nat(bit0(bit1(pls)))))) ),
inference(clausify,[status(thm)],[f_106_3]) ).
fof(f_107_1,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(negate,[status(cth)],[conj_0]) ).
fof(f_107_2,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(definitional_conversion,[status(esa)],[f_107_1]) ).
cnf(f_107_3,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(clausify,[status(thm)],[f_107_2]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( semiri1621563631at_int(Eq_x_0) = semiri1621563631at_int(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( plus_plus_int(Eq_x_0,Eq_x_1) = plus_plus_int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( bit1(Eq_x_0) = bit1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( bit0(Eq_x_0) = bit0(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( number_number_of_nat(Eq_x_0) = number_number_of_nat(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( power_power_int(Eq_x_0,Eq_x_1) = power_power_int(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( power_power_nat(Eq_x_0,Eq_x_1) = power_power_nat(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( number_number_of_int(Eq_x_0) = number_number_of_int(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( plus_plus_nat(Eq_x_0,Eq_x_1) = plus_plus_nat(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( semiri984289939at_nat(Eq_x_0) = semiri984289939at_nat(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( ord_less_int(Eq_y_0,Eq_y_1)
| ~ ord_less_int(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( ord_less_nat(Eq_y_0,Eq_y_1)
| ~ ord_less_nat(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n010.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 19 19:24:38 UTC 2026
% 0.08/0.36 % CPUTime :
% 20.06/20.34 % SZS status Theorem for theBenchmark
% 20.06/20.34 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------