%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM924_2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.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 : Fri Sep 25 02:27:15 PM UTC 2026
% Result : Theorem 8.11s 1.71s
% Output : CNFRefutation 8.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 23
% Syntax : Number of formulae : 114 ( 114 unt; 0 typ; 0 def)
% Number of atoms : 973 ( 86 equ)
% Maximal formula atoms : 1 ( 8 avg)
% Number of connectives : 12 ( 12 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 859 ( 859 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 25 usr; 7 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 11 con; 0-3 aty)
% Number of variables : 114 ( 0 sgn 114 !; 0 ?; 114 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
minus_minus_int: ( int * int ) > int ).
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(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: ( nat * int ) > int ).
tff(func_def_23,type,
power_power_nat: ( nat * nat ) > nat ).
tff(func_def_24,type,
power_power_real: ( nat * real ) > 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: ( nat * real ) > real ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',fact_3_t) ).
tff(f35,axiom,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_number__of__is__id) ).
tff(f36,axiom,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_zmult__commute) ).
tff(f42,axiom,
! [X0: int,X1: int,X2: int] : ( times_times_int(times_times_int(X0,X1),X2) = times_times_int(X0,times_times_int(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_zmult__assoc) ).
tff(f88,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_nat__1__add__1) ).
tff(f131,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/sandbox/benchmark/theBenchmark.p',fact_130_zadd__assoc) ).
tff(f133,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_zadd__commute) ).
tff(f171,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_Pls__def) ).
tff(f179,axiom,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_add__Pls) ).
tff(f181,axiom,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_Bit0__def) ).
tff(f202,axiom,
! [X0: int] : ( power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))) = times_times_int(X0,X0) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',fact_234_Bit1__def) ).
tff(f315,axiom,
! [X0: real,X1: real,X2: real] : ( times_times_real(times_times_real(X0,X1),X2) = times_times_real(X0,times_times_real(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_314_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f316,axiom,
! [X0: nat,X1: nat,X2: nat] : ( times_times_nat(times_times_nat(X0,X1),X2) = times_times_nat(X0,times_times_nat(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_315_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f324,axiom,
! [X0: real,X1: real] : ( times_times_real(X0,X1) = times_times_real(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_323_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f325,axiom,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_324_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f327,axiom,
! [X0: real,X1: real] : ( plus_plus_real(X0,X1) = plus_plus_real(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_326_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f328,axiom,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_327_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f333,axiom,
! [X0: real,X1: real,X2: real] : ( plus_plus_real(X0,plus_plus_real(X1,X2)) = plus_plus_real(plus_plus_real(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_332_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
tff(f334,axiom,
! [X0: nat,X1: nat,X2: nat] : ( plus_plus_nat(X0,plus_plus_nat(X1,X2)) = plus_plus_nat(plus_plus_nat(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_333_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
tff(f363,axiom,
! [X0: int] : ( times_times_int(X0,zero_zero_int) = zero_zero_int ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_362_comm__semiring__1__class_Onormalizing__semiring__rules_I10_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/sandbox/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(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(f1274,plain,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f1275,plain,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f1284,plain,
! [X2: int,X0: int,X1: int] : ( times_times_int(times_times_int(X0,X1),X2) = times_times_int(X0,times_times_int(X1,X2)) ),
inference(cnf_transformation,[],[f42]) ).
tff(f1359,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f88]) ).
tff(f1428,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,[],[f131]) ).
tff(f1430,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f133]) ).
tff(f1482,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f171]) ).
tff(f1494,plain,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
inference(cnf_transformation,[],[f179]) ).
tff(f1496,plain,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
inference(cnf_transformation,[],[f181]) ).
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(f1665,plain,
! [X2: real,X0: real,X1: real] : ( times_times_real(times_times_real(X0,X1),X2) = times_times_real(X0,times_times_real(X1,X2)) ),
inference(cnf_transformation,[],[f315]) ).
tff(f1666,plain,
! [X2: nat,X0: nat,X1: nat] : ( times_times_nat(times_times_nat(X0,X1),X2) = times_times_nat(X0,times_times_nat(X1,X2)) ),
inference(cnf_transformation,[],[f316]) ).
tff(f1674,plain,
! [X0: real,X1: real] : ( times_times_real(X0,X1) = times_times_real(X1,X0) ),
inference(cnf_transformation,[],[f324]) ).
tff(f1675,plain,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
inference(cnf_transformation,[],[f325]) ).
tff(f1677,plain,
! [X0: real,X1: real] : ( plus_plus_real(X0,X1) = plus_plus_real(X1,X0) ),
inference(cnf_transformation,[],[f327]) ).
tff(f1678,plain,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
inference(cnf_transformation,[],[f328]) ).
tff(f1683,plain,
! [X2: real,X0: real,X1: real] : ( plus_plus_real(X0,plus_plus_real(X1,X2)) = plus_plus_real(plus_plus_real(X0,X1),X2) ),
inference(cnf_transformation,[],[f333]) ).
tff(f1684,plain,
! [X2: nat,X0: nat,X1: nat] : ( plus_plus_nat(X0,plus_plus_nat(X1,X2)) = plus_plus_nat(plus_plus_nat(X0,X1),X2) ),
inference(cnf_transformation,[],[f334]) ).
tff(f1717,plain,
! [X0: int] : ( zero_zero_int = times_times_int(X0,zero_zero_int) ),
inference(cnf_transformation,[],[f363]) ).
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(f2236,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,[],[f1359,f1496,f1561]) ).
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(f2434,plain,
! [X0: int] : ( pls = times_times_int(X0,pls) ),
inference(definition_unfolding,[],[f1717,f1482,f1482]) ).
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]) ).
tcf(c_51,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(cnf_transformation,[],[f2160]) ).
tcf(c_52,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(cnf_transformation,[],[f2161]) ).
tcf(c_95,plain,
! [X0_int: int] : number_number_of_int(X0_int) = X0_int,
inference(cnf_transformation,[],[f1274]) ).
tcf(c_96,plain,
! [X0_int: int,X1_int: int] : times_times_int(X0_int,X1_int) = times_times_int(X1_int,X0_int),
inference(cnf_transformation,[],[f1275]) ).
tcf(c_105,plain,
! [X0_int: int,X1_int: int,X2_int: int] : times_times_int(times_times_int(X0_int,X1_int),X2_int) = times_times_int(X0_int,times_times_int(X1_int,X2_int)),
inference(cnf_transformation,[],[f1284]) ).
tcf(c_180,plain,
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))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f2236]) ).
tcf(c_238,plain,
! [X0_int: int,X1_int: int,X2_int: int] : plus_plus_int(plus_plus_int(X0_int,X1_int),X2_int) = plus_plus_int(X0_int,plus_plus_int(X1_int,X2_int)),
inference(cnf_transformation,[],[f1428]) ).
tcf(c_240,plain,
! [X0_int: int,X1_int: int] : plus_plus_int(X0_int,X1_int) = plus_plus_int(X1_int,X0_int),
inference(cnf_transformation,[],[f1430]) ).
tcf(c_303,plain,
! [X0_int: int] : plus_plus_int(pls,X0_int) = X0_int,
inference(cnf_transformation,[],[f1494]) ).
tcf(c_325,plain,
! [X0_int: int] : power_power_int(X0_int,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)))) = times_times_int(X0_int,X0_int),
inference(cnf_transformation,[],[f2336]) ).
tcf(c_472,plain,
! [X0_real: real,X1_real: real,X2_real: real] : times_times_real(times_times_real(X0_real,X1_real),X2_real) = times_times_real(X0_real,times_times_real(X1_real,X2_real)),
inference(cnf_transformation,[],[f1665]) ).
tcf(c_473,plain,
! [X0_nat: nat,X1_nat: nat,X2_nat: nat] : times_times_nat(times_times_nat(X0_nat,X1_nat),X2_nat) = times_times_nat(X0_nat,times_times_nat(X1_nat,X2_nat)),
inference(cnf_transformation,[],[f1666]) ).
tcf(c_481,plain,
! [X0_real: real,X1_real: real] : times_times_real(X0_real,X1_real) = times_times_real(X1_real,X0_real),
inference(cnf_transformation,[],[f1674]) ).
tcf(c_482,plain,
! [X0_nat: nat,X1_nat: nat] : times_times_nat(X0_nat,X1_nat) = times_times_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f1675]) ).
tcf(c_484,plain,
! [X0_real: real,X1_real: real] : plus_plus_real(X0_real,X1_real) = plus_plus_real(X1_real,X0_real),
inference(cnf_transformation,[],[f1677]) ).
tcf(c_485,plain,
! [X0_nat: nat,X1_nat: nat] : plus_plus_nat(X0_nat,X1_nat) = plus_plus_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f1678]) ).
tcf(c_490,plain,
! [X0_real: real,X1_real: real,X2_real: real] : plus_plus_real(plus_plus_real(X0_real,X1_real),X2_real) = plus_plus_real(X0_real,plus_plus_real(X1_real,X2_real)),
inference(cnf_transformation,[],[f1683]) ).
tcf(c_491,plain,
! [X0_nat: nat,X1_nat: nat,X2_nat: nat] : plus_plus_nat(plus_plus_nat(X0_nat,X1_nat),X2_nat) = plus_plus_nat(X0_nat,plus_plus_nat(X1_nat,X2_nat)),
inference(cnf_transformation,[],[f1684]) ).
tcf(c_524,plain,
! [X0_int: int] : times_times_int(X0_int,pls) = pls,
inference(cnf_transformation,[],[f2434]) ).
tcf(c_954,negated_conjecture,
~ 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(cnf_transformation,[],[f2567]) ).
tcf(c_1409,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int))))))))))))))),times_times_int(pls,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))))))))))),
inference(theory_normalisation,[status(thm)],[c_51,c_472,c_481,c_473,c_482,c_105,c_96,c_490,c_484,c_491,c_485,c_238,c_240]) ).
tcf(c_1410,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_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(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))))),
inference(theory_normalisation,[status(thm)],[c_52,c_472,c_481,c_473,c_482,c_105,c_96,c_490,c_484,c_491,c_485,c_238,c_240]) ).
tcf(c_1463,plain,
number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(theory_normalisation,[status(thm)],[c_180,c_472,c_481,c_473,c_482,c_105,c_96,c_490,c_484,c_491,c_485,c_238,c_240]) ).
tcf(c_1514,plain,
! [X0_int: int] : power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))) = times_times_int(X0_int,X0_int),
inference(theory_normalisation,[status(thm)],[c_325,c_472,c_481,c_473,c_482,c_105,c_96,c_490,c_484,c_491,c_485,c_238,c_240]) ).
tcf(c_1619,negated_conjecture,
~ 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(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))))),pls),
inference(theory_normalisation,[status(thm)],[c_954,c_472,c_481,c_473,c_482,c_105,c_96,c_490,c_484,c_491,c_485,c_238,c_240]) ).
tcf(c_7348,plain,
number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_1463,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7349,plain,
number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls)))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_7348,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7350,plain,
number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_7349,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7351,plain,
number_number_of_nat(plus_plus_int(one_one_int,one_one_int)) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_7350,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7537,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(one_one_int,pls))))))),pls),
inference(ac_demodulation,[status(thm)],[c_1619,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7538,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(one_one_int,plus_plus_int(pls,pls)))))),pls),
inference(ac_demodulation,[status(thm)],[c_7537,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7539,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(ac_demodulation,[status(thm)],[c_7538,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7540,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(ac_demodulation,[status(thm)],[c_7539,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7541,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(light_normalisation,[status(thm)],[c_7540,c_7351]) ).
tcf(c_7554,plain,
! [X0_int: int] : power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))) = times_times_int(X0_int,X0_int),
inference(ac_demodulation,[status(thm)],[c_1514,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7555,plain,
! [X0_int: int] : power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))) = times_times_int(X0_int,X0_int),
inference(ac_demodulation,[status(thm)],[c_7554,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7556,plain,
! [X0_int: int] : power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))) = times_times_int(X0_int,X0_int),
inference(ac_demodulation,[status(thm)],[c_7555,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7557,plain,
! [X0_int: int] : power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))) = times_times_int(X0_int,X0_int),
inference(ac_demodulation,[status(thm)],[c_7556,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_7558,plain,
! [X0_int: int] : power_power_int(X0_int,plus_plus_nat(one_one_nat,one_one_nat)) = times_times_int(X0_int,X0_int),
inference(light_normalisation,[status(thm)],[c_7557,c_7351]) ).
tcf(c_7560,plain,
~ ord_less_int(plus_plus_int(one_one_int,times_times_int(s,s)),pls),
inference(demodulation,[status(thm)],[c_7541,c_7558]) ).
tcf(c_8527,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))))))))))) = 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(one_one_int,pls))))))),
inference(ac_demodulation,[status(thm)],[c_1410,c_303,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8528,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls)))))),
inference(ac_demodulation,[status(thm)],[c_8527,c_303,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8529,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,pls)))))))))))) = 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))))),
inference(ac_demodulation,[status(thm)],[c_8528,c_303,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8530,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,pls))))))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),
inference(ac_demodulation,[status(thm)],[c_8529,c_303,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8531,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,one_one_int)))))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),
inference(ac_demodulation,[status(thm)],[c_8530,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8532,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),
inference(ac_demodulation,[status(thm)],[c_8531,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8533,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),
inference(ac_demodulation,[status(thm)],[c_8532,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8534,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int))))))) = plus_plus_int(one_one_int,power_power_int(s,number_number_of_nat(plus_plus_int(one_one_int,one_one_int)))),
inference(ac_demodulation,[status(thm)],[c_8533,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8535,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int))))))) = plus_plus_int(one_one_int,power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat))),
inference(light_normalisation,[status(thm)],[c_8534,c_7351]) ).
tcf(c_8536,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))) = plus_plus_int(one_one_int,times_times_int(s,s)),
inference(demodulation,[status(thm)],[c_8535,c_95,c_7558]) ).
tcf(c_8559,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_1409,c_524,c_303,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8560,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8559,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8561,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,pls)))))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8560,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8562,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,pls))))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8561,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8563,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,one_one_int)))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8562,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8564,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8563,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8565,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int)))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8564,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8566,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(one_one_int,one_one_int))))))),pls),
inference(ac_demodulation,[status(thm)],[c_8565,c_303,c_238,c_240,c_491,c_485,c_490,c_484,c_105,c_96,c_473,c_482,c_472,c_481]) ).
tcf(c_8567,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(s,s)),pls),
inference(demodulation,[status(thm)],[c_8566,c_95,c_8536]) ).
tcf(c_8568,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_8567,c_7560]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924_2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 05:47:07 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 8.11/1.71 % SZS status Started for theBenchmark.p
% 8.11/1.71 % SZS status Theorem for theBenchmark.p
% 8.11/1.71
% 8.11/1.71 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.11/1.71
% 8.11/1.71 % ------ iProver source info
% 8.11/1.71
% 8.11/1.71 % git: date: 2026-07-19 20:42:38 +0200
% 8.11/1.71 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.11/1.71 % git: non_committed_changes: false
% 8.11/1.71
% 8.11/1.71 % ------ Parsing...
% 8.11/1.71 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 8.11/1.71 %
% 8.11/1.71
% 8.11/1.71 % ------ Preprocessing...%
% 8.11/1.71
% 8.11/1.71 % SZS status Theorem for theBenchmark.p
% 8.11/1.71
% 8.11/1.71 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.11/1.71
% 8.11/1.71
%------------------------------------------------------------------------------