%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM924_2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 : Tue Sep 29 12:26:06 PM UTC 2026
% Result : Theorem 1.41s 0.64s
% Output : Refutation 1.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 27
% Syntax : Number of formulae : 172 ( 168 unt; 0 typ; 0 def)
% Number of atoms : 178 ( 127 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 29 ( 23 ~; 4 |; 1 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 38 ( 38 usr; 16 con; 0-3 aty)
% Number of variables : 122 ( 122 !; 0 ?; 122 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
int: $tType ).
tff(type_def_6,type,
nat: $tType ).
tff(type_def_7,type,
real: $tType ).
tff(func_def_0,type,
minus_minus_int: ( int * int ) > int ).
tff(func_def_1,type,
minus_minus_nat: ( nat * nat ) > nat ).
tff(func_def_2,type,
minus_minus_real: ( real * real ) > real ).
tff(func_def_3,type,
one_one_int: int ).
tff(func_def_4,type,
one_one_nat: nat ).
tff(func_def_5,type,
one_one_real: real ).
tff(func_def_6,type,
plus_plus_int: ( int * int ) > int ).
tff(func_def_7,type,
plus_plus_nat: ( nat * nat ) > nat ).
tff(func_def_8,type,
plus_plus_real: ( real * real ) > real ).
tff(func_def_9,type,
times_times_int: ( int * int ) > int ).
tff(func_def_10,type,
times_times_nat: ( nat * nat ) > nat ).
tff(func_def_11,type,
times_times_real: ( real * real ) > real ).
tff(func_def_12,type,
zero_zero_int: int ).
tff(func_def_13,type,
zero_zero_nat: nat ).
tff(func_def_14,type,
zero_zero_real: real ).
tff(func_def_15,type,
bit0: int > int ).
tff(func_def_16,type,
bit1: int > int ).
tff(func_def_17,type,
min: int ).
tff(func_def_18,type,
pls: int ).
tff(func_def_19,type,
number_number_of_int: int > int ).
tff(func_def_20,type,
number_number_of_nat: int > nat ).
tff(func_def_21,type,
number267125858f_real: int > real ).
tff(func_def_22,type,
power_power_int: ( int * nat ) > int ).
tff(func_def_23,type,
power_power_nat: ( nat * nat ) > nat ).
tff(func_def_24,type,
power_power_real: ( real * nat ) > real ).
tff(func_def_25,type,
legendre: ( int * int ) > int ).
tff(func_def_26,type,
m: int ).
tff(func_def_27,type,
s1: int ).
tff(func_def_28,type,
s: int ).
tff(func_def_29,type,
t: int ).
tff(func_def_30,type,
sK0: int ).
tff(func_def_31,type,
sK1: int ).
tff(func_def_32,type,
sK2: int ).
tff(func_def_33,type,
sK3: int > int ).
tff(func_def_34,type,
sK4: int ).
tff(func_def_35,type,
sK5: ( int * int * int ) > int ).
tff(func_def_36,type,
sK6: ( int * int ) > int ).
tff(func_def_37,type,
sK7: ( real * nat ) > real ).
tff(pred_def_1,type,
zcong: ( int * int * int ) > $o ).
tff(pred_def_2,type,
zprime: int > $o ).
tff(pred_def_3,type,
ord_less_int: ( int * int ) > $o ).
tff(pred_def_4,type,
ord_less_nat: ( nat * nat ) > $o ).
tff(pred_def_5,type,
ord_less_real: ( real * real ) > $o ).
tff(pred_def_6,type,
ord_less_eq_int: ( int * int ) > $o ).
tff(pred_def_7,type,
ord_less_eq_nat: ( nat * nat ) > $o ).
tff(pred_def_8,type,
ord_less_eq_real: ( real * real ) > $o ).
tff(pred_def_9,type,
quadRes: ( int * int ) > $o ).
tff(pred_def_10,type,
dvd_dvd_int: ( int * int ) > $o ).
tff(pred_def_11,type,
dvd_dvd_nat: ( nat * nat ) > $o ).
tff(pred_def_12,type,
dvd_dvd_real: ( real * real ) > $o ).
tff(pred_def_13,type,
twoSqu512355103sum2sq: int > $o ).
tff(f3,axiom,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
tff(f4,axiom,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
tff(f29,axiom,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = number_number_of_int(plus_plus_int(X0,bit1(pls))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_add__special_I3_J) ).
tff(f35,axiom,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_number__of__is__id) ).
tff(f90,axiom,
! [X0: int,X1: int] : ( times_times_int(bit0(X0),X1) = bit0(times_times_int(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_mult__Bit0) ).
tff(f171,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_Pls__def) ).
tff(f180,axiom,
! [X0: int,X1: int] : ( plus_plus_int(bit0(X0),bit0(X1)) = bit0(plus_plus_int(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_179_add__Bit0__Bit0) ).
tff(f181,axiom,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_Bit0__def) ).
tff(f186,axiom,
! [X0: int] : ( times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(X0)) = number_number_of_int(bit0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_double__number__of__Bit0) ).
tff(f202,axiom,
! [X0: int] : ( power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_power2__eq__square) ).
tff(f235,axiom,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_Bit1__def) ).
tff(f261,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_260_semiring__one__add__one__is__two) ).
tff(f323,axiom,
! [X0: int,X1: int,X2: int] : ( times_times_int(X0,times_times_int(X1,X2)) = times_times_int(X1,times_times_int(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_322_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
tff(f326,axiom,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_325_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f329,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_328_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f332,axiom,
! [X0: int,X1: int,X2: int] : ( plus_plus_int(X0,plus_plus_int(X1,X2)) = plus_plus_int(X1,plus_plus_int(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_331_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
tff(f338,axiom,
! [X0: int,X1: int,X2: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_337_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f341,axiom,
! [X0: int,X1: int,X2: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(plus_plus_int(X0,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_340_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J) ).
tff(f344,axiom,
! [X0: int,X1: int,X2: int,X3: int] : ( plus_plus_int(plus_plus_int(X0,X1),plus_plus_int(X2,X3)) = plus_plus_int(plus_plus_int(X0,X2),plus_plus_int(X1,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_343_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J) ).
tff(f363,axiom,
! [X0: int] : ( times_times_int(X0,zero_zero_int) = zero_zero_int ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_362_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
tff(f366,axiom,
! [X0: int] : ( plus_plus_int(zero_zero_int,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_365_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J) ).
tff(f372,axiom,
! [X0: int,X1: int] :
( ( X0 = plus_plus_int(X0,X1) )
<=> ( X1 = zero_zero_int ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_371_add__0__iff) ).
tff(f375,axiom,
! [X0: int,X1: int,X2: int] : ( times_times_int(X0,plus_plus_int(X1,X2)) = plus_plus_int(times_times_int(X0,X1),times_times_int(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_374_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J) ).
tff(f411,axiom,
! [X0: int] : ( plus_plus_int(X0,X0) = times_times_int(plus_plus_int(one_one_int,one_one_int),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_410_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J) ).
tff(f417,axiom,
! [X0: int,X1: int] : ( plus_plus_int(times_times_int(X0,X1),X1) = times_times_int(plus_plus_int(X0,one_one_int),X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_416_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J) ).
tff(f439,axiom,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_438_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
tff(f699,conjecture,
ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f700,negated_conjecture,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
inference(negated_conjecture,[status(cth)],[f699]) ).
tff(f701,plain,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
inference(flattening,[],[f700]) ).
tff(f1138,plain,
! [X0: int,X1: int] :
( ( ( X0 = plus_plus_int(X0,X1) )
| ( zero_zero_int != X1 ) )
& ( ( X1 = zero_zero_int )
| ( plus_plus_int(X0,X1) != X0 ) ) ),
inference(nnf_transformation,[],[f372]) ).
tff(f1230,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(cnf_transformation,[],[f3]) ).
tff(f1231,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),
inference(cnf_transformation,[],[f4]) ).
tff(f1268,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = number_number_of_int(plus_plus_int(X0,bit1(pls))) ),
inference(cnf_transformation,[],[f29]) ).
tff(f1274,plain,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f1361,plain,
! [X0: int,X1: int] : ( times_times_int(bit0(X0),X1) = bit0(times_times_int(X0,X1)) ),
inference(cnf_transformation,[],[f90]) ).
tff(f1482,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f171]) ).
tff(f1495,plain,
! [X0: int,X1: int] : ( plus_plus_int(bit0(X0),bit0(X1)) = bit0(plus_plus_int(X0,X1)) ),
inference(cnf_transformation,[],[f180]) ).
tff(f1496,plain,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
inference(cnf_transformation,[],[f181]) ).
tff(f1501,plain,
! [X0: int] : ( times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(X0)) = number_number_of_int(bit0(X0)) ),
inference(cnf_transformation,[],[f186]) ).
tff(f1517,plain,
! [X0: int] : ( power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(X0,X0) ),
inference(cnf_transformation,[],[f202]) ).
tff(f1561,plain,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
inference(cnf_transformation,[],[f235]) ).
tff(f1594,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f261]) ).
tff(f1673,plain,
! [X2: int,X0: int,X1: int] : ( times_times_int(X0,times_times_int(X1,X2)) = times_times_int(X1,times_times_int(X0,X2)) ),
inference(cnf_transformation,[],[f323]) ).
tff(f1676,plain,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
inference(cnf_transformation,[],[f326]) ).
tff(f1679,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f329]) ).
tff(f1682,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus_int(X0,plus_plus_int(X1,X2)) = plus_plus_int(X1,plus_plus_int(X0,X2)) ),
inference(cnf_transformation,[],[f332]) ).
tff(f1688,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)) ),
inference(cnf_transformation,[],[f338]) ).
tff(f1691,plain,
! [X2: int,X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(plus_plus_int(X0,X2),X1) ),
inference(cnf_transformation,[],[f341]) ).
tff(f1694,plain,
! [X2: int,X3: int,X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X1),plus_plus_int(X2,X3)) = plus_plus_int(plus_plus_int(X0,X2),plus_plus_int(X1,X3)) ),
inference(cnf_transformation,[],[f344]) ).
tff(f1717,plain,
! [X0: int] : ( zero_zero_int = times_times_int(X0,zero_zero_int) ),
inference(cnf_transformation,[],[f363]) ).
tff(f1720,plain,
! [X0: int] : ( plus_plus_int(zero_zero_int,X0) = X0 ),
inference(cnf_transformation,[],[f366]) ).
tff(f1729,plain,
! [X0: int,X1: int] :
( ( plus_plus_int(X0,X1) = X0 )
| ( zero_zero_int != X1 ) ),
inference(cnf_transformation,[],[f1138]) ).
tff(f1732,plain,
! [X2: int,X0: int,X1: int] : ( times_times_int(X0,plus_plus_int(X1,X2)) = plus_plus_int(times_times_int(X0,X1),times_times_int(X0,X2)) ),
inference(cnf_transformation,[],[f375]) ).
tff(f1780,plain,
! [X0: int] : ( plus_plus_int(X0,X0) = times_times_int(plus_plus_int(one_one_int,one_one_int),X0) ),
inference(cnf_transformation,[],[f411]) ).
tff(f1786,plain,
! [X0: int,X1: int] : ( plus_plus_int(times_times_int(X0,X1),X1) = times_times_int(plus_plus_int(X0,one_one_int),X1) ),
inference(cnf_transformation,[],[f417]) ).
tff(f1817,plain,
! [X0: int] : ( power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(X0,X0) ),
inference(cnf_transformation,[],[f439]) ).
tff(f2158,plain,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int),zero_zero_int),
inference(cnf_transformation,[],[f701]) ).
tff(f2160,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),pls)),
inference(definition_unfolding,[],[f1230,f1496,f1496,f1561,f1496,f1496,f1561,f1482]) ).
tff(f2161,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t) = plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),one_one_int),
inference(definition_unfolding,[],[f1231,f1496,f1496,f1561,f1496,f1561]) ).
tff(f2197,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = number_number_of_int(plus_plus_int(X0,plus_plus_int(plus_plus_int(one_one_int,pls),pls))) ),
inference(definition_unfolding,[],[f1268,f1561]) ).
tff(f2237,plain,
! [X0: int,X1: int] : ( times_times_int(plus_plus_int(X0,X0),X1) = plus_plus_int(times_times_int(X0,X1),times_times_int(X0,X1)) ),
inference(definition_unfolding,[],[f1361,f1496,f1496]) ).
tff(f2316,plain,
! [X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X0),plus_plus_int(X1,X1)) = plus_plus_int(plus_plus_int(X0,X1),plus_plus_int(X0,X1)) ),
inference(definition_unfolding,[],[f1495,f1496,f1496,f1496]) ).
tff(f2320,plain,
! [X0: int] : ( times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(X0)) = number_number_of_int(plus_plus_int(X0,X0)) ),
inference(definition_unfolding,[],[f1501,f1496]) ).
tff(f2336,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))) ),
inference(definition_unfolding,[],[f1517,f1496,f1561]) ).
tff(f2385,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))),
inference(definition_unfolding,[],[f1594,f1496,f1561]) ).
tff(f2434,plain,
! [X0: int] : ( pls = times_times_int(X0,pls) ),
inference(definition_unfolding,[],[f1717,f1482,f1482]) ).
tff(f2435,plain,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
inference(definition_unfolding,[],[f1720,f1482]) ).
tff(f2437,plain,
! [X0: int,X1: int] :
( ( plus_plus_int(X0,X1) = X0 )
| ( pls != X1 ) ),
inference(definition_unfolding,[],[f1729,f1482]) ).
tff(f2463,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))) ),
inference(definition_unfolding,[],[f1817,f1496,f1561]) ).
tff(f2567,plain,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),one_one_int),pls),
inference(definition_unfolding,[],[f2158,f1496,f1561,f1482]) ).
tff(f2617,plain,
! [X0: int] : ( plus_plus_int(X0,pls) = X0 ),
inference(equality_resolution,[],[f2437]) ).
tff(f2748,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(plus_plus_int(one_one_int,pls),plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),
inference(forward_demodulation,[],[f2385,f1688]) ).
tff(f2780,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(one_one_int,pls),plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls))))) ),
inference(forward_demodulation,[],[f2336,f1688]) ).
tff(f2796,plain,
! [X0: int,X1: int] : ( plus_plus_int(plus_plus_int(X0,X0),plus_plus_int(X1,X1)) = plus_plus_int(X0,plus_plus_int(X1,plus_plus_int(X0,X1))) ),
inference(forward_demodulation,[],[f2316,f1688]) ).
tff(f2849,plain,
! [X0: int,X1: int] : ( times_times_int(plus_plus_int(X0,X0),X1) = times_times_int(X0,plus_plus_int(X1,X1)) ),
inference(forward_demodulation,[],[f2237,f1732]) ).
tff(f2875,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = plus_plus_int(X0,plus_plus_int(plus_plus_int(one_one_int,pls),pls)) ),
inference(forward_demodulation,[],[f2197,f1274]) ).
tff(f2911,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))),
inference(forward_demodulation,[],[f2161,f1679]) ).
tff(f2912,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t),plus_plus_int(times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),pls),pls)),
inference(forward_demodulation,[],[f2160,f1786]) ).
tff(f2966,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls))))),
inference(forward_demodulation,[],[f2748,f1688]) ).
tff(f2987,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))))) ),
inference(forward_demodulation,[],[f2780,f1688]) ).
tff(f3003,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,plus_plus_int(X1,plus_plus_int(X0,X1))) = plus_plus_int(X0,plus_plus_int(X0,plus_plus_int(X1,X1))) ),
inference(forward_demodulation,[],[f2796,f1688]) ).
tff(f3055,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = plus_plus_int(X0,plus_plus_int(one_one_int,plus_plus_int(pls,pls))) ),
inference(forward_demodulation,[],[f2875,f1688]) ).
tff(f3082,plain,
times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t) = plus_plus_int(one_one_int,times_times_int(s,s)),
inference(forward_demodulation,[],[f2911,f2463]) ).
tff(f3083,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t),times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),pls)),
inference(forward_demodulation,[],[f2912,f2617]) ).
tff(f3130,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls))))),
inference(forward_demodulation,[],[f2966,f1682]) ).
tff(f3150,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))))) ),
inference(forward_demodulation,[],[f2987,f1682]) ).
tff(f3205,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = plus_plus_int(X0,plus_plus_int(pls,plus_plus_int(one_one_int,pls))) ),
inference(forward_demodulation,[],[f3055,f1682]) ).
tff(f3229,plain,
plus_plus_int(times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),t),t) = plus_plus_int(one_one_int,times_times_int(s,s)),
inference(forward_demodulation,[],[f3082,f1786]) ).
tff(f3230,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),one_one_int),t),pls),
inference(forward_demodulation,[],[f3083,f2434]) ).
tff(f3275,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),
inference(forward_demodulation,[],[f3130,f2435]) ).
tff(f3294,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(plus_plus_int(one_one_int,pls),pls))))) ),
inference(forward_demodulation,[],[f3150,f2435]) ).
tff(f3349,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = plus_plus_int(X0,plus_plus_int(one_one_int,pls)) ),
inference(forward_demodulation,[],[f3205,f2435]) ).
tff(f3373,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),t)),
inference(forward_demodulation,[],[f3229,f1679]) ).
tff(f3374,plain,
ord_less_int(plus_plus_int(times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),t),t),pls),
inference(forward_demodulation,[],[f3230,f1786]) ).
tff(f3415,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),
inference(forward_demodulation,[],[f3275,f1682]) ).
tff(f3424,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(one_one_int,pls),pls))))) ),
inference(forward_demodulation,[],[f3294,f1682]) ).
tff(f3472,plain,
! [X0: int] : ( plus_plus_int(number_number_of_int(X0),one_one_int) = plus_plus_int(X0,one_one_int) ),
inference(forward_demodulation,[],[f3349,f2617]) ).
tff(f3494,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(t,times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m))),
inference(forward_demodulation,[],[f3373,f1676]) ).
tff(f3495,plain,
ord_less_int(plus_plus_int(t,times_times_int(times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m),t)),pls),
inference(forward_demodulation,[],[f3374,f1679]) ).
tff(f3532,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(one_one_int,pls),pls))),
inference(forward_demodulation,[],[f3415,f2435]) ).
tff(f3540,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(one_one_int,pls),pls)))) ),
inference(forward_demodulation,[],[f3424,f2435]) ).
tff(f3578,plain,
! [X0: int] : ( plus_plus_int(one_one_int,number_number_of_int(X0)) = plus_plus_int(X0,one_one_int) ),
inference(forward_demodulation,[],[f3472,f1679]) ).
tff(f3598,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(t,times_times_int(m,number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),
inference(forward_demodulation,[],[f3494,f1676]) ).
tff(f3599,plain,
ord_less_int(plus_plus_int(t,times_times_int(t,times_times_int(number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),m))),pls),
inference(forward_demodulation,[],[f3495,f1676]) ).
tff(f3636,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls)))),
inference(forward_demodulation,[],[f3532,f1688]) ).
tff(f3644,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))) ),
inference(forward_demodulation,[],[f3540,f1688]) ).
tff(f3682,plain,
! [X0: int] : ( plus_plus_int(X0,one_one_int) = plus_plus_int(one_one_int,X0) ),
inference(forward_demodulation,[],[f3578,f1274]) ).
tff(f3701,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),
inference(forward_demodulation,[],[f3598,f1673]) ).
tff(f3702,plain,
ord_less_int(plus_plus_int(t,times_times_int(t,times_times_int(m,number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),pls),
inference(forward_demodulation,[],[f3599,f1676]) ).
tff(f3739,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,pls)))),
inference(forward_demodulation,[],[f3636,f3003]) ).
tff(f3747,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,pls))))) ),
inference(forward_demodulation,[],[f3644,f3003]) ).
tff(f3802,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),
inference(forward_demodulation,[],[f3701,f2320]) ).
tff(f3803,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)),plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),pls),
inference(forward_demodulation,[],[f3702,f1673]) ).
tff(f3840,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))),
inference(forward_demodulation,[],[f3739,f1682]) ).
tff(f3848,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))))) ),
inference(forward_demodulation,[],[f3747,f1682]) ).
tff(f3903,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),
inference(forward_demodulation,[],[f3802,f2320]) ).
tff(f3904,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),pls),
inference(forward_demodulation,[],[f3803,f2320]) ).
tff(f3935,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))),
inference(forward_demodulation,[],[f3840,f2435]) ).
tff(f3943,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))) ),
inference(forward_demodulation,[],[f3848,f2435]) ).
tff(f3998,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))))),
inference(forward_demodulation,[],[f3903,f1274]) ).
tff(f3999,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),number_number_of_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls))))))),pls),
inference(forward_demodulation,[],[f3904,f2320]) ).
tff(f4028,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(one_one_int,one_one_int)),
inference(forward_demodulation,[],[f3935,f2617]) ).
tff(f4035,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))) ),
inference(forward_demodulation,[],[f3943,f2617]) ).
tff(f4090,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))),
inference(forward_demodulation,[],[f3998,f1688]) ).
tff(f4091,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))))),pls),
inference(forward_demodulation,[],[f3999,f1274]) ).
tff(f4123,plain,
! [X0: int] : ( times_times_int(X0,X0) = power_power_int(X0,plus_plus_nat(one_one_nat,one_one_nat)) ),
inference(forward_demodulation,[],[f4035,f4028]) ).
tff(f4173,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,pls))))))),
inference(forward_demodulation,[],[f4090,f1682]) ).
tff(f4174,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))),pls),
inference(forward_demodulation,[],[f4091,f1688]) ).
tff(f4209,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,pls)))))),
inference(forward_demodulation,[],[f4173,f2435]) ).
tff(f4210,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,pls))))))),pls),
inference(forward_demodulation,[],[f4174,f1682]) ).
tff(f4236,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(plus_plus_int(one_one_int,pls),plus_plus_int(one_one_int,pls)))))),
inference(forward_demodulation,[],[f4209,f1780]) ).
tff(f4237,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,pls)))))),pls),
inference(forward_demodulation,[],[f4210,f2435]) ).
tff(f4262,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,pls))))))),
inference(forward_demodulation,[],[f4236,f1688]) ).
tff(f4263,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(plus_plus_int(one_one_int,pls),plus_plus_int(one_one_int,pls)))))),pls),
inference(forward_demodulation,[],[f4237,f1780]) ).
tff(f4288,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))))))),
inference(forward_demodulation,[],[f4262,f1682]) ).
tff(f4289,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,pls))))))),pls),
inference(forward_demodulation,[],[f4263,f1688]) ).
tff(f4314,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))),
inference(forward_demodulation,[],[f4288,f2435]) ).
tff(f4315,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))))))),pls),
inference(forward_demodulation,[],[f4289,f1682]) ).
tff(f4340,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))))),
inference(forward_demodulation,[],[f4314,f3682]) ).
tff(f4341,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))),pls),
inference(forward_demodulation,[],[f4315,f2435]) ).
tff(f4356,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))),
inference(forward_demodulation,[],[f4340,f1682]) ).
tff(f4357,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))))),pls),
inference(forward_demodulation,[],[f4341,f3682]) ).
tff(f4370,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,one_one_int))))),
inference(forward_demodulation,[],[f4356,f2435]) ).
tff(f4371,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))),pls),
inference(forward_demodulation,[],[f4357,f1682]) ).
tff(f4384,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(t,plus_plus_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,one_one_int))))),
inference(forward_demodulation,[],[f4370,f1780]) ).
tff(f4385,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,one_one_int))))),pls),
inference(forward_demodulation,[],[f4371,f2435]) ).
tff(f4392,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(plus_plus_int(t,t),plus_plus_int(one_one_int,one_one_int)))),
inference(forward_demodulation,[],[f4384,f2849]) ).
tff(f4393,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(t,plus_plus_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(one_one_int,one_one_int))))),pls),
inference(forward_demodulation,[],[f4385,f1780]) ).
tff(f4399,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(t,t)))),
inference(forward_demodulation,[],[f4392,f1676]) ).
tff(f4400,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(plus_plus_int(t,t),plus_plus_int(one_one_int,one_one_int)))),pls),
inference(forward_demodulation,[],[f4393,f2849]) ).
tff(f4404,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(m,plus_plus_int(plus_plus_int(t,t),plus_plus_int(t,t)))),
inference(forward_demodulation,[],[f4399,f1780]) ).
tff(f4405,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,times_times_int(plus_plus_int(one_one_int,one_one_int),plus_plus_int(t,t)))),pls),
inference(forward_demodulation,[],[f4400,f1676]) ).
tff(f4409,plain,
plus_plus_int(one_one_int,times_times_int(s,s)) = plus_plus_int(t,times_times_int(plus_plus_int(m,m),plus_plus_int(t,t))),
inference(forward_demodulation,[],[f4404,f2849]) ).
tff(f4410,plain,
ord_less_int(plus_plus_int(t,times_times_int(m,plus_plus_int(plus_plus_int(t,t),plus_plus_int(t,t)))),pls),
inference(forward_demodulation,[],[f4405,f1780]) ).
tff(f4414,plain,
ord_less_int(plus_plus_int(t,times_times_int(plus_plus_int(m,m),plus_plus_int(t,t))),pls),
inference(forward_demodulation,[],[f4410,f2849]) ).
tff(f4417,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(s,s)),pls),
inference(forward_demodulation,[],[f4414,f4409]) ).
tff(f5554,plain,
~ ord_less_int(plus_plus_int(power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(pls,one_one_int),pls),plus_plus_int(plus_plus_int(pls,one_one_int),pls)))),one_one_int),pls),
inference(superposition,[],[f2567,f3682]) ).
tff(f5559,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(pls,one_one_int),pls),plus_plus_int(plus_plus_int(pls,one_one_int),pls))))),pls),
inference(forward_demodulation,[],[f5554,f1679]) ).
tff(f5561,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(pls,one_one_int),plus_plus_int(pls,plus_plus_int(plus_plus_int(pls,one_one_int),pls)))))),pls),
inference(forward_demodulation,[],[f5559,f1688]) ).
tff(f5562,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(plus_plus_int(pls,pls),plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(pls,one_one_int),pls)))))),pls),
inference(forward_demodulation,[],[f5561,f1694]) ).
tff(f5563,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(pls,one_one_int),pls))))))),pls),
inference(forward_demodulation,[],[f5562,f1688]) ).
tff(f5564,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(pls,one_one_int),pls)))))),pls),
inference(forward_demodulation,[],[f5563,f2435]) ).
tff(f5565,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(pls,one_one_int),pls))))),pls),
inference(forward_demodulation,[],[f5564,f2435]) ).
tff(f5566,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(plus_plus_int(pls,pls),one_one_int))))),pls),
inference(forward_demodulation,[],[f5565,f1691]) ).
tff(f5567,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,one_one_int)))))),pls),
inference(forward_demodulation,[],[f5566,f1688]) ).
tff(f5568,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))))),pls),
inference(forward_demodulation,[],[f5567,f1682]) ).
tff(f5569,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int))))),pls),
inference(forward_demodulation,[],[f5568,f2435]) ).
tff(f5570,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))),pls),
inference(forward_demodulation,[],[f5569,f1682]) ).
tff(f5571,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),pls),
inference(forward_demodulation,[],[f5570,f2435]) ).
tff(f5572,plain,
~ ord_less_int(plus_plus_int(one_one_int,power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat))),pls),
inference(forward_demodulation,[],[f5571,f4028]) ).
tff(f5573,plain,
~ ord_less_int(plus_plus_int(one_one_int,times_times_int(s,s)),pls),
inference(forward_demodulation,[],[f5572,f4123]) ).
tff(f5599,plain,
$false,
inference(resolution,[],[f4417,f5573]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924_2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 21:41:19 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.41/0.64 % (3435927)Will run a generic schedule for satisfiability detection.
% 1.41/0.64 % (3435936)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1437356924:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.41/0.64 % (3435933)% WARNING: option uhcvi not known.
% 1.41/0.64 % (3435932)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2174160215_2999 on theBenchmark for (2999ds/0Mi)
% 1.41/0.64 % (3435933)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2905600718:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.41/0.64 % (3435934)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2996575821:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.41/0.64 % (3435935)dis+10_1_sil=32000:sp=arity:random_seed=3357472296:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.41/0.64 % (3435937)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3615376680:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.41/0.64 % (3435938)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3955259532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.41/0.64 % (3435936)Instruction limit reached!
% 1.41/0.64 % (3435936)------------------------------
% 1.41/0.64 % (3435936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.64 % (3435936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.64 % (3435936)CaDiCaL version: 2.1.3
% 1.41/0.64 % (3435936)Termination reason: Instruction limit
% 1.41/0.64 % (3435936)Termination phase: Saturation
% 1.41/0.64 % (3435936)Time elapsed: 0.034 s
% 1.41/0.64 % (3435936)Peak memory usage: 14 MB
% 1.41/0.64 % (3435936)Instructions burned: 117 (million)
% 1.41/0.64 % (3435946)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=229864781:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.41/0.64 % (3435935)Instruction limit reached!
% 1.41/0.64 % (3435935)------------------------------
% 1.41/0.64 % (3435935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.64 % (3435935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.64 % (3435935)CaDiCaL version: 2.1.3
% 1.41/0.64 % (3435935)Termination reason: Instruction limit
% 1.41/0.64 % (3435935)Termination phase: Saturation
% 1.41/0.64 % (3435935)Time elapsed: 0.062 s
% 1.41/0.64 % (3435935)Peak memory usage: 13 MB
% 1.41/0.64 % (3435935)Instructions burned: 104 (million)
% 1.41/0.64 % (3435937)Instruction limit reached!
% 1.41/0.64 % (3435937)------------------------------
% 1.41/0.64 % (3435937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.64 % (3435937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.64 % (3435937)CaDiCaL version: 2.1.3
% 1.41/0.64 % (3435937)Termination reason: Instruction limit
% 1.41/0.64 % (3435937)Termination phase: Saturation
% 1.41/0.64 % (3435937)Time elapsed: 0.067 s
% 1.41/0.64 % (3435937)Peak memory usage: 13 MB
% 1.41/0.64 % (3435937)Instructions burned: 133 (million)
% 1.41/0.64 % (3435948)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2699140571:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.41/0.64 % (3435949)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1168680233:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.41/0.64 % (3435938)Instruction limit reached!
% 1.41/0.64 % (3435938)------------------------------
% 1.41/0.64 % (3435938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.64 % (3435938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.64 % (3435938)CaDiCaL version: 2.1.3
% 1.41/0.64 % (3435938)Termination reason: Instruction limit
% 1.41/0.64 % (3435938)Termination phase: Saturation
% 1.41/0.64 % (3435938)Time elapsed: 0.098 s
% 1.41/0.64 % (3435938)Peak memory usage: 14 MB
% 1.41/0.64 % (3435938)Instructions burned: 159 (million)
% 1.41/0.64 % (3435952)ott-21_1_sil=16000:fs=off:random_seed=897978479:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.41/0.64 % TRYING [1]
% 1.41/0.64 % TRYING [2]
% 1.41/0.64 % (3435948)Instruction limit reached!
% 1.41/0.64 % (3435948)------------------------------
% 1.41/0.64 % (3435948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.64 % (3435948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.64 % (3435948)CaDiCaL version: 2.1.3
% 1.41/0.64 % (3435948)Termination reason: Instruction limit
% 1.41/0.64 % (3435948)Termination phase: Saturation
% 1.41/0.64 % (3435948)Time elapsed: 0.075 s
% 1.41/0.64 % (3435948)Peak memory usage: 14 MB
% 1.41/0.64 % (3435948)Instructions burned: 132 (million)
% 1.41/0.64 % (3435954)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2011499325:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.41/0.64 % (3435952) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3435927-3435952"...
% 1.41/0.64 % TRYING [3]
% 1.41/0.64 % (3435952)...printing done.
% 1.41/0.64 % (3435952)Refutation found. Thanks to Tanya!
% 1.41/0.64 % SZS status Theorem for theBenchmark
% 1.41/0.64 % SZS output start Proof for theBenchmark
% See solution above
% 1.41/0.65 % (3435952)------------------------------
% 1.41/0.65 % (3435952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.41/0.65 % (3435952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.41/0.65 % (3435952)CaDiCaL version: 2.1.3
% 1.41/0.65 % (3435952)Termination reason: Refutation
% 1.41/0.65 % (3435952)Time elapsed: 0.063 s
% 1.41/0.65 % (3435952)Peak memory usage: 14 MB
% 1.41/0.65 % (3435952)Instructions burned: 129 (million)
% 1.41/0.65 % (3435927)Success in time 0.239 s
% 1.41/0.65 % Vampire exiting
%------------------------------------------------------------------------------