%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM926_1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n008.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:20 PM UTC 2026
% Result : Theorem 1.91s 1.29s
% Output : CNFRefutation 1.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 28
% Syntax : Number of formulae : 144 ( 78 unt; 0 typ; 2 def)
% Number of atoms : 559 ( 97 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 153 ( 73 ~; 70 |; 4 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of FOOLs : 335 ( 335 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 17 ( 15 usr; 5 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 236 ( 0 sgn 224 !; 12 ?; 236 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
one_one_int: int ).
tff(pred_def_1,type,
zprime: int > $o ).
tff(pred_def_2,type,
ord_less_int: ( int * int ) > $o ).
tff(pred_def_3,type,
ord_less_nat: ( nat * nat ) > $o ).
tff(pred_def_4,type,
ord_less_eq_int: ( int * int ) > $o ).
tff(pred_def_5,type,
ord_less_eq_nat: ( nat * nat ) > $o ).
tff(pred_def_6,type,
twoSqu1431725154sum2sq: int > $o ).
tff(func_def_7,type,
bit1: int > int ).
tff(func_def_8,type,
pls: int ).
tff(func_def_9,type,
number_number_of_int: int > int ).
tff(func_def_10,type,
number_number_of_nat: int > nat ).
tff(func_def_11,type,
power_power_int: ( nat * int ) > int ).
tff(func_def_12,type,
power_power_nat: ( nat * nat ) > nat ).
tff(func_def_13,type,
m: int ).
tff(func_def_14,type,
s: int ).
tff(func_def_15,type,
t: int ).
tff(func_def_16,type,
sK0: int ).
tff(func_def_17,type,
sK1: int ).
tff(func_def_18,type,
sK2: int ).
tff(func_def_19,type,
sK3: int ).
tff(func_def_20,type,
sK4: int ).
tff(f1,axiom,
ord_less_eq_int(one_one_int,t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tpos) ).
tff(f2,axiom,
( ( t = one_one_int )
=> ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
tff(f3,axiom,
( ord_less_int(one_one_int,t)
=> ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
tff(f24,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_23_add__special_I3_J) ).
tff(f25,axiom,
plus_plus_int(one_one_int,one_one_int) = number_number_of_int(bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_one__add__one__is__two) ).
tff(f30,axiom,
! [X0: int,X1: int] :
( ord_less_int(X1,X0)
| ( X0 = X1 )
| ord_less_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_zless__linear) ).
tff(f39,axiom,
! [X0: int,X1: int] :
( ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_le__number__of__eq__not__less) ).
tff(f59,axiom,
! [X0: int,X1: int] :
( ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ord_less_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_less__number__of__int__code) ).
tff(f60,axiom,
! [X0: int,X1: int] :
( ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
<=> ord_less_eq_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_less__eq__number__of__int__code) ).
tff(f74,axiom,
! [X0: int,X1: int] :
( ord_less_int(X0,plus_plus_int(X1,one_one_int))
<=> ord_less_eq_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_zle__add1__eq__le) ).
tff(f85,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/sandbox2/benchmark/theBenchmark.p',fact_84_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f86,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/sandbox2/benchmark/theBenchmark.p',fact_85_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J) ).
tff(f88,axiom,
! [X0: nat,X1: nat,X2: nat] : ( times_times_nat(X0,times_times_nat(X1,X2)) = times_times_nat(times_times_nat(X0,X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J) ).
tff(f91,axiom,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f92,axiom,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_91_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J) ).
tff(f97,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_96_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f98,axiom,
! [X0: nat,X1: nat,X2: nat] : ( plus_plus_nat(plus_plus_nat(X0,X1),X2) = plus_plus_nat(X0,plus_plus_nat(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J) ).
tff(f100,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/sandbox2/benchmark/theBenchmark.p',fact_99_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
tff(f103,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f104,axiom,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J) ).
tff(f110,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/sandbox2/benchmark/theBenchmark.p',fact_109_zmult__assoc) ).
tff(f111,axiom,
! [X0: int,X1: int] : ( times_times_int(X0,X1) = times_times_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_zmult__commute) ).
tff(f112,axiom,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_number__of__is__id) ).
tff(f113,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_112_zadd__assoc) ).
tff(f115,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_zadd__commute) ).
tff(f124,conjecture,
? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f125,negated_conjecture,
~ ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(negated_conjecture,[status(cth)],[f124]) ).
tff(f128,plain,
( ( one_one_int != t )
| ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
inference(ennf_transformation,[],[f2]) ).
tff(f129,plain,
( ~ ord_less_int(one_one_int,t)
| ? [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ) ),
inference(ennf_transformation,[],[f3]) ).
tff(f143,plain,
! [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(ennf_transformation,[],[f125]) ).
tff(f144,plain,
( ( one_one_int != t )
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f128]) ).
tff(f145,plain,
( ~ ord_less_int(one_one_int,t)
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X1,sK3)],[f129]) ).
tff(f150,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) )
& ( ord_less_int(number_number_of_int(X1),number_number_of_int(X0))
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f39]) ).
tff(f161,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_int(X0,X1) )
& ( ~ ord_less_int(X0,X1)
| ord_less_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f59]) ).
tff(f162,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_eq_int(X0,X1) )
& ( ~ ord_less_eq_int(X0,X1)
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ) ),
inference(nnf_transformation,[],[f60]) ).
tff(f170,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_int(X0,plus_plus_int(X1,one_one_int))
| ord_less_eq_int(X0,X1) )
& ( ~ ord_less_eq_int(X0,X1)
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ) ),
inference(nnf_transformation,[],[f74]) ).
tff(f184,plain,
ord_less_eq_int(one_one_int,t),
inference(cnf_transformation,[],[f1]) ).
tff(f185,plain,
( ( one_one_int != t )
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(cnf_transformation,[],[f144]) ).
tff(f186,plain,
( ~ ord_less_int(one_one_int,t)
| ( plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) = plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(cnf_transformation,[],[f145]) ).
tff(f206,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,[],[f24]) ).
tff(f207,plain,
number_number_of_int(bit0(bit1(pls))) = plus_plus_int(one_one_int,one_one_int),
inference(cnf_transformation,[],[f25]) ).
tff(f214,plain,
! [X0: int,X1: int] :
( ord_less_int(X1,X0)
| ( X0 = X1 )
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f30]) ).
tff(f224,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ~ ord_less_int(number_number_of_int(X1),number_number_of_int(X0)) ),
inference(cnf_transformation,[],[f150]) ).
tff(f225,plain,
! [X0: int,X1: int] :
( ord_less_int(number_number_of_int(X1),number_number_of_int(X0))
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f150]) ).
tff(f255,plain,
! [X0: int,X1: int] :
( ~ ord_less_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f161]) ).
tff(f256,plain,
! [X0: int,X1: int] :
( ~ ord_less_int(X0,X1)
| ord_less_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f161]) ).
tff(f257,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1))
| ord_less_eq_int(X0,X1) ),
inference(cnf_transformation,[],[f162]) ).
tff(f258,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(X0,X1)
| ord_less_eq_int(number_number_of_int(X0),number_number_of_int(X1)) ),
inference(cnf_transformation,[],[f162]) ).
tff(f281,plain,
! [X0: int,X1: int] :
( ~ ord_less_int(X0,plus_plus_int(X1,one_one_int))
| ord_less_eq_int(X0,X1) ),
inference(cnf_transformation,[],[f170]) ).
tff(f282,plain,
! [X0: int,X1: int] :
( ~ ord_less_eq_int(X0,X1)
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ),
inference(cnf_transformation,[],[f170]) ).
tff(f292,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,[],[f85]) ).
tff(f293,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,[],[f86]) ).
tff(f295,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,[],[f88]) ).
tff(f298,plain,
! [X0: int,X1: int] : ( times_times_int(X1,X0) = times_times_int(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
tff(f299,plain,
! [X0: nat,X1: nat] : ( times_times_nat(X0,X1) = times_times_nat(X1,X0) ),
inference(cnf_transformation,[],[f92]) ).
tff(f304,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,[],[f97]) ).
tff(f305,plain,
! [X2: nat,X0: nat,X1: nat] : ( plus_plus_nat(plus_plus_nat(X0,X1),X2) = plus_plus_nat(X0,plus_plus_nat(X1,X2)) ),
inference(cnf_transformation,[],[f98]) ).
tff(f307,plain,
! [X2: nat,X0: nat,X1: nat] : ( plus_plus_nat(plus_plus_nat(X0,X1),X2) = plus_plus_nat(X0,plus_plus_nat(X1,X2)) ),
inference(cnf_transformation,[],[f100]) ).
tff(f310,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f311,plain,
! [X0: nat,X1: nat] : ( plus_plus_nat(X0,X1) = plus_plus_nat(X1,X0) ),
inference(cnf_transformation,[],[f104]) ).
tff(f322,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,[],[f110]) ).
tff(f323,plain,
! [X0: int,X1: int] : ( times_times_int(X1,X0) = times_times_int(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tff(f324,plain,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
inference(cnf_transformation,[],[f112]) ).
tff(f325,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,[],[f113]) ).
tff(f327,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f115]) ).
tff(f344,plain,
! [X0: int,X1: int] : ( plus_plus_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_49,plain,
ord_less_eq_int(one_one_int,t),
inference(cnf_transformation,[],[f184]) ).
tcf(c_50,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) )
| ( one_one_int != t ) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_51,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int) )
| ~ ord_less_int(one_one_int,t) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_71,plain,
! [X0_int: int] : number_number_of_int(plus_plus_int(X0_int,bit1(pls))) = plus_plus_int(number_number_of_int(X0_int),one_one_int),
inference(cnf_transformation,[],[f206]) ).
tcf(c_72,plain,
number_number_of_int(bit0(bit1(pls))) = plus_plus_int(one_one_int,one_one_int),
inference(cnf_transformation,[],[f207]) ).
tcf(c_79,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int)
| ( X0_int = X1_int ) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_89,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_90,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ~ ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_120,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_int(X0_int,X1_int) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_121,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ~ ord_less_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_122,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_123,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_146,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,plus_plus_int(X1_int,one_one_int))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_147,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_int(X0_int,plus_plus_int(X1_int,one_one_int)) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_157,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,[],[f292]) ).
tcf(c_158,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,[],[f293]) ).
tcf(c_160,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,[],[f295]) ).
tcf(c_163,plain,
! [X0_int: int,X1_int: int] : times_times_int(X0_int,X1_int) = times_times_int(X1_int,X0_int),
inference(cnf_transformation,[],[f298]) ).
tcf(c_164,plain,
! [X0_nat: nat,X1_nat: nat] : times_times_nat(X0_nat,X1_nat) = times_times_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f299]) ).
tcf(c_169,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,[],[f304]) ).
tcf(c_170,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,[],[f305]) ).
tcf(c_172,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,[],[f307]) ).
tcf(c_175,plain,
! [X0_int: int,X1_int: int] : plus_plus_int(X0_int,X1_int) = plus_plus_int(X1_int,X0_int),
inference(cnf_transformation,[],[f310]) ).
tcf(c_176,plain,
! [X0_nat: nat,X1_nat: nat] : plus_plus_nat(X0_nat,X1_nat) = plus_plus_nat(X1_nat,X0_nat),
inference(cnf_transformation,[],[f311]) ).
tcf(c_180,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,[],[f322]) ).
tcf(c_181,plain,
! [X0_int: int,X1_int: int] : times_times_int(X0_int,X1_int) = times_times_int(X1_int,X0_int),
inference(cnf_transformation,[],[f323]) ).
tcf(c_182,plain,
! [X0_int: int] : number_number_of_int(X0_int) = X0_int,
inference(cnf_transformation,[],[f324]) ).
tcf(c_183,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,[],[f325]) ).
tcf(c_185,plain,
! [X0_int: int,X1_int: int] : plus_plus_int(X0_int,X1_int) = plus_plus_int(X1_int,X0_int),
inference(cnf_transformation,[],[f327]) ).
tcf(c_202,negated_conjecture,
! [X0_int: int,X1_int: int] : plus_plus_int(power_power_int(X0_int,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1_int,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),
inference(cnf_transformation,[],[f344]) ).
tcf(c_281,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(bit0(bit0(bit1(pls)))))) )
| ( one_one_int != t ) ),
inference(theory_normalisation,[status(thm)],[c_50,c_158,c_164,c_157,c_163,c_170,c_176,c_169,c_175]) ).
tcf(c_282,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(bit0(bit0(bit1(pls)))))) )
| ~ ord_less_int(one_one_int,t) ),
inference(theory_normalisation,[status(thm)],[c_51,c_158,c_164,c_157,c_163,c_170,c_176,c_169,c_175]) ).
tcf(c_290,plain,
! [X0_int: int] : number_number_of_int(plus_plus_int(X0_int,bit1(pls))) = plus_plus_int(one_one_int,number_number_of_int(X0_int)),
inference(theory_normalisation,[status(thm)],[c_71,c_158,c_164,c_157,c_163,c_170,c_176,c_169,c_175]) ).
tcf(c_292,negated_conjecture,
! [X0_int: int,X1_int: int] : plus_plus_int(power_power_int(X0_int,number_number_of_nat(bit0(bit1(pls)))),power_power_int(X1_int,number_number_of_nat(bit0(bit1(pls))))) != plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(bit0(bit0(bit1(pls)))))),
inference(theory_normalisation,[status(thm)],[c_202,c_158,c_164,c_157,c_163,c_170,c_176,c_169,c_175]) ).
tcf(c_297,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ord_less_eq_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_123]) ).
tcf(c_298,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_297]) ).
tcf(c_299,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_122]) ).
tcf(c_305,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ~ ord_less_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_120,c_90]) ).
tcf(c_306,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X1_int,X0_int)
| ~ ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_305]) ).
tcf(c_307,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(number_number_of_int(X1_int),number_number_of_int(X0_int))
| ord_less_int(X0_int,X1_int) ),
inference(prop_impl_just,[status(thm)],[c_121,c_89]) ).
tcf(c_308,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X1_int,X0_int)
| ord_less_eq_int(number_number_of_int(X0_int),number_number_of_int(X1_int)) ),
inference(renaming,[status(thm)],[c_307]) ).
tcf(c_373,plain,
( ( plus_plus_int(power_power_int(sK0,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK1,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(bit0(bit0(bit1(pls)))))) )
| ( one_one_int != t ) ),
inference(prop_impl_just,[status(thm)],[c_281]) ).
tcf(c_375,plain,
( ( plus_plus_int(power_power_int(sK2,number_number_of_nat(bit0(bit1(pls)))),power_power_int(sK3,number_number_of_nat(bit0(bit1(pls))))) = plus_plus_int(one_one_int,times_times_int(m,number_number_of_int(bit0(bit0(bit1(pls)))))) )
| ~ ord_less_int(one_one_int,t) ),
inference(prop_impl_just,[status(thm)],[c_282]) ).
tcf(c_572,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_306,c_299]) ).
tcf(c_573,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_308,c_298]) ).
tcf(c_653,plain,
~ ord_less_int(one_one_int,t),
inference(backward_subsumption_resolution,[status(thm)],[c_375,c_292]) ).
tcf(c_654,plain,
one_one_int != t,
inference(backward_subsumption_resolution,[status(thm)],[c_373,c_292]) ).
tcf(c_1055,plain,
plus_plus_int(one_one_int,one_one_int) = bit0(bit1(pls)),
inference(demodulation,[status(thm)],[c_72,c_182]) ).
tcf(c_1074,plain,
! [X0_int: int] : number_number_of_int(plus_plus_int(X0_int,bit1(pls))) = plus_plus_int(one_one_int,X0_int),
inference(light_normalisation,[status(thm)],[c_290,c_182]) ).
tcf(c_1075,plain,
! [X0_int: int] : plus_plus_int(X0_int,bit1(pls)) = plus_plus_int(one_one_int,X0_int),
inference(demodulation,[status(thm)],[c_1074,c_182]) ).
tcf(c_1212,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X0_int,X1_int)
| ~ ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_572]) ).
tcf(c_1213,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_1212]) ).
tcf(c_1452,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ( X1_int = X0_int )
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_79,c_1213]) ).
tcf(c_1993,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_int(X0_int,X1_int)
| ~ ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_572]) ).
tcf(c_1994,plain,
! [X0_int: int,X1_int: int] :
( ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_1993]) ).
tcf(c_2232,plain,
! [X0_int: int,X1_int: int] :
( ( X1_int = X0_int )
| ~ ord_less_eq_int(X1_int,X0_int)
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(bin_hyper_res,[status(thm)],[c_1452,c_1994]) ).
tcf(c_2757,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,X1_int)
| ord_less_eq_int(X1_int,X0_int) ),
inference(prop_impl_just,[status(thm)],[c_573]) ).
tcf(c_2758,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X1_int,X0_int)
| ord_less_int(X0_int,X1_int) ),
inference(renaming,[status(thm)],[c_2757]) ).
tcf(c_3517,definition,
iPr_def_11 = bit1(pls),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_3518,definition,
iPr_def_12 = bit0(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_3524,plain,
~ ord_less_int(one_one_int,t),
inference(demodulation,[status(thm)],[c_653]) ).
tcf(c_4245,plain,
plus_plus_int(one_one_int,one_one_int) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_1055,c_3517,c_3518]) ).
tcf(c_4281,plain,
! [X0_int: int] : plus_plus_int(X0_int,iPr_def_11) = plus_plus_int(one_one_int,X0_int),
inference(light_normalisation,[status(thm)],[c_1075,c_3517]) ).
tcf(c_4282,plain,
plus_plus_int(one_one_int,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_4245,c_4281]) ).
tcf(c_4283,plain,
plus_plus_int(iPr_def_11,one_one_int) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_4282,c_183,c_185,c_172,c_176,c_180,c_181,c_160,c_164]) ).
tcf(c_4315,plain,
! [X0_int: int] : plus_plus_int(X0_int,one_one_int) = plus_plus_int(X0_int,iPr_def_11),
inference(superposition,[status(thm)],[c_185,c_4281]) ).
tcf(c_4318,plain,
plus_plus_int(iPr_def_11,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_4283,c_4315]) ).
tcf(c_4699,plain,
! [X0_int: int,X1_int: int] :
( ord_less_int(X0_int,plus_plus_int(X1_int,iPr_def_11))
| ~ ord_less_eq_int(X0_int,X1_int) ),
inference(demodulation,[status(thm)],[c_146,c_4315]) ).
tcf(c_4708,plain,
! [X0_int: int] :
( ord_less_int(X0_int,plus_plus_int(iPr_def_11,iPr_def_11))
| ~ ord_less_eq_int(X0_int,one_one_int) ),
inference(superposition,[status(thm)],[c_4281,c_4699]) ).
tcf(c_4717,plain,
! [X0_int: int] :
( ord_less_int(X0_int,iPr_def_12)
| ~ ord_less_eq_int(X0_int,one_one_int) ),
inference(light_normalisation,[status(thm)],[c_4708,c_4318]) ).
tcf(c_4727,plain,
! [X0_int: int,X1_int: int] :
( ord_less_eq_int(X0_int,X1_int)
| ~ ord_less_int(X0_int,plus_plus_int(X1_int,iPr_def_11)) ),
inference(demodulation,[status(thm)],[c_147,c_4315]) ).
tcf(c_4737,plain,
! [X0_int: int] :
( ord_less_eq_int(X0_int,one_one_int)
| ~ ord_less_int(X0_int,plus_plus_int(iPr_def_11,iPr_def_11)) ),
inference(superposition,[status(thm)],[c_4281,c_4727]) ).
tcf(c_4744,plain,
! [X0_int: int] :
( ord_less_eq_int(X0_int,one_one_int)
| ~ ord_less_int(X0_int,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_4737,c_4318]) ).
tcf(c_4993,plain,
! [X0_int: int] :
( ord_less_int(one_one_int,X0_int)
| ord_less_int(X0_int,iPr_def_12) ),
inference(superposition,[status(thm)],[c_2758,c_4717]) ).
tcf(c_5004,plain,
ord_less_int(t,iPr_def_12),
inference(superposition,[status(thm)],[c_4993,c_3524]) ).
tcf(c_5368,plain,
ord_less_eq_int(t,one_one_int),
inference(superposition,[status(thm)],[c_5004,c_4744]) ).
tcf(c_5380,plain,
( ( one_one_int = t )
| ~ ord_less_eq_int(t,one_one_int)
| ~ ord_less_eq_int(one_one_int,t) ),
inference(instantiation,[status(thm)],[c_2232]) ).
tcf(c_5381,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5380,c_5368,c_654,c_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926_1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.36 % Computer : n008.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 : Thu Sep 24 05:45:09 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 1.91/1.29 % SZS status Started for theBenchmark.p
% 1.91/1.29 % SZS status Theorem for theBenchmark.p
% 1.91/1.29
% 1.91/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.91/1.29
% 1.91/1.29 % ------ iProver source info
% 1.91/1.29
% 1.91/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 1.91/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.91/1.29 % git: non_committed_changes: false
% 1.91/1.29
% 1.91/1.29 % ------ Parsing...
% 1.91/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 1.91/1.29 %
% 1.91/1.29
% 1.91/1.29 % ------ Preprocessing... sup_sim: 30 pe_s pe_e sup_sim: 0 pe_s pe_e sup_sim: 0 pe_s pe_e sup_sim: 0 pe_s pe_e %
% 1.91/1.29
% 1.91/1.29 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 1.91/1.29 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 1.91/1.29 %
% 1.91/1.29
% 1.91/1.29 % ------ Preprocessing...
% 1.91/1.29 % ------ Proving...
% 1.91/1.29 % ------ Problem Properties
% 1.91/1.29
% 1.91/1.29 %
% 1.91/1.29 % clauses 95
% 1.91/1.29 % conjectures 0
% 1.91/1.29 % EPR 10
% 1.91/1.29 % Horn 83
% 1.91/1.29 % unary 47
% 1.91/1.29 % binary 42
% 1.91/1.29 % lits 149
% 1.91/1.29 % lits eq 49
% 1.91/1.29 % fd_pure 0
% 1.91/1.29 % fd_pseudo 0
% 1.91/1.29 % fd_cond 0
% 1.91/1.29 % fd_pseudo_cond 3
% 1.91/1.29 % AC symbols 4
% 1.91/1.29
% 1.91/1.29 % ------ Schedule dynamic 5 is on
% 1.91/1.29
% 1.91/1.29 % ------ no conjectures: strip conj schedule
% 1.91/1.29
% 1.91/1.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 1.91/1.29
% 1.91/1.29
% 1.91/1.29 % ------
% 1.91/1.29 % Current options:
% 1.91/1.29 % ------
% 1.91/1.29
% 1.91/1.29
% 1.91/1.29 %
% 1.91/1.29
% 1.91/1.29 % ------ Proving...
% 1.91/1.29 %
% 1.91/1.29
% 1.91/1.29 % SZS status Theorem for theBenchmark.p
% 1.91/1.29
% 1.91/1.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.91/1.29
% 1.91/1.29
%------------------------------------------------------------------------------