%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM924+3 : 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 : n016.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:16 PM UTC 2026
% Result : Theorem 7.48s 2.81s
% Output : CNFRefutation 7.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 24
% Syntax : Number of formulae : 103 ( 87 unt; 0 def)
% Number of atoms : 153 ( 114 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 91 ( 41 ~; 37 |; 6 &)
% ( 5 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 8 con; 0-2 aty)
% Number of variables : 107 ( 0 sgn 107 !; 0 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_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) ).
fof(f29,axiom,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_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) ).
fof(f61,axiom,
! [X0,X1] : hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_zmult__commute) ).
fof(f67,axiom,
! [X0,X1,X2] : hAPP_int_int(times_times_int(hAPP_int_int(times_times_int(X0),X1)),X2) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_zmult__assoc) ).
fof(f113,axiom,
hAPP_nat_nat(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) ).
fof(f158,axiom,
! [X0,X1,X2] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) = hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_zadd__assoc) ).
fof(f159,axiom,
! [X0,X1,X2] : hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(X1),hAPP_int_int(plus_plus_int(X0),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_zadd__left__commute) ).
fof(f160,axiom,
! [X0,X1] : hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_zadd__commute) ).
fof(f186,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_one__is__num__one) ).
fof(f190,axiom,
! [X0] :
( is_int(X0)
=> ( hAPP_int_int(plus_plus_int(X0),X0) = zero_zero_int
<=> X0 = zero_zero_int ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_double__eq__0__iff) ).
fof(f197,axiom,
bit0(pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_Bit0__Pls) ).
fof(f198,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_Pls__def) ).
fof(f208,axiom,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_Bit0__def) ).
fof(f213,axiom,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(bit0(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_double__number__of__Bit0) ).
fof(f229,axiom,
! [X0] : hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))) = hAPP_int_int(times_times_int(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_power2__eq__square) ).
fof(f262,axiom,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_Bit1__def) ).
fof(f353,axiom,
! [X0,X1,X2] : hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)) = hAPP_int_int(times_times_int(X1),hAPP_int_int(times_times_int(X0),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_327_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
fof(f441,axiom,
! [X0] : hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_415_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J) ).
fof(f447,axiom,
! [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X1)),X1) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(X0),one_one_int)),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_421_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J) ).
fof(f529,axiom,
! [X0,X1] :
( ( is_int(X1)
& is_int(X0) )
=> ( hAPP_int_int(times_times_int(X0),X1) = zero_zero_int
<=> ( X1 = zero_zero_int
| X0 = zero_zero_int ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_503_mult__eq__0__iff) ).
fof(f532,axiom,
! [X0] : hAPP_int_int(times_times_int(X0),zero_zero_int) = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_506_mult__zero__right) ).
fof(f1094,axiom,
twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_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_1068__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096) ).
fof(f1227,axiom,
! [X0,X1,X2] : hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_COMBC_000tc__Int__Oint_000tc__Int__Oint_000tc__HOL__Obool_U) ).
fof(f1230,conjecture,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_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) ).
fof(f1231,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(negated_conjecture,[status(cth)],[f1230]) ).
fof(f1235,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(flattening,[],[f1231]) ).
fof(f1331,plain,
! [X0] :
( ~ is_int(X0)
| ( hAPP_int_int(plus_plus_int(X0),X0) = zero_zero_int
<=> X0 = zero_zero_int ) ),
inference(ennf_transformation,[],[f190]) ).
fof(f1473,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| ( hAPP_int_int(times_times_int(X0),X1) = zero_zero_int
<=> ( X1 = zero_zero_int
| X0 = zero_zero_int ) ) ),
inference(ennf_transformation,[],[f529]) ).
fof(f1474,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| ( hAPP_int_int(times_times_int(X0),X1) = zero_zero_int
<=> ( X1 = zero_zero_int
| X0 = zero_zero_int ) ) ),
inference(flattening,[],[f1473]) ).
fof(f2291,plain,
! [X0] :
( ~ is_int(X0)
| ( ( zero_zero_int != hAPP_int_int(plus_plus_int(X0),X0)
| X0 = zero_zero_int )
& ( zero_zero_int != X0
| hAPP_int_int(plus_plus_int(X0),X0) = zero_zero_int ) ) ),
inference(nnf_transformation,[],[f1331]) ).
fof(f2371,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| ( ( zero_zero_int != hAPP_int_int(times_times_int(X0),X1)
| X1 = zero_zero_int
| X0 = zero_zero_int )
& ( ( zero_zero_int != X1
& zero_zero_int != X0 )
| hAPP_int_int(times_times_int(X0),X1) = zero_zero_int ) ) ),
inference(nnf_transformation,[],[f1474]) ).
fof(f2372,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| ( ( zero_zero_int != hAPP_int_int(times_times_int(X0),X1)
| X1 = zero_zero_int
| X0 = zero_zero_int )
& ( ( zero_zero_int != X1
& zero_zero_int != X0 )
| hAPP_int_int(times_times_int(X0),X1) = zero_zero_int ) ) ),
inference(flattening,[],[f2371]) ).
fof(f2634,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(cnf_transformation,[],[f28]) ).
fof(f2635,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int),
inference(cnf_transformation,[],[f29]) ).
fof(f2680,plain,
! [X0,X1] : hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0),
inference(cnf_transformation,[],[f61]) ).
fof(f2689,plain,
! [X2,X0,X1] : hAPP_int_int(times_times_int(hAPP_int_int(times_times_int(X0),X1)),X2) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)),
inference(cnf_transformation,[],[f67]) ).
fof(f2764,plain,
number_number_of_nat(bit0(bit1(pls))) = hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat),
inference(cnf_transformation,[],[f113]) ).
fof(f2836,plain,
! [X2,X0,X1] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) = hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)),
inference(cnf_transformation,[],[f158]) ).
fof(f2837,plain,
! [X2,X0,X1] : hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(X1),hAPP_int_int(plus_plus_int(X0),X2)),
inference(cnf_transformation,[],[f159]) ).
fof(f2838,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0),
inference(cnf_transformation,[],[f160]) ).
fof(f2872,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(cnf_transformation,[],[f186]) ).
fof(f2880,plain,
! [X0] :
( ~ is_int(X0)
| zero_zero_int != X0
| zero_zero_int = hAPP_int_int(plus_plus_int(X0),X0) ),
inference(cnf_transformation,[],[f2291]) ).
fof(f2889,plain,
pls = bit0(pls),
inference(cnf_transformation,[],[f197]) ).
fof(f2890,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f198]) ).
fof(f2904,plain,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
inference(cnf_transformation,[],[f208]) ).
fof(f2909,plain,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(bit0(X0)),
inference(cnf_transformation,[],[f213]) ).
fof(f2925,plain,
! [X0] : hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))) = hAPP_int_int(times_times_int(X0),X0),
inference(cnf_transformation,[],[f229]) ).
fof(f2969,plain,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
inference(cnf_transformation,[],[f262]) ).
fof(f3086,plain,
! [X2,X0,X1] : hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)) = hAPP_int_int(times_times_int(X1),hAPP_int_int(times_times_int(X0),X2)),
inference(cnf_transformation,[],[f353]) ).
fof(f3193,plain,
! [X0] : hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),X0),
inference(cnf_transformation,[],[f441]) ).
fof(f3199,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X1)),X1) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(X0),one_one_int)),X1),
inference(cnf_transformation,[],[f447]) ).
fof(f3316,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| zero_zero_int != X1
| zero_zero_int = hAPP_int_int(times_times_int(X0),X1) ),
inference(cnf_transformation,[],[f2372]) ).
fof(f3320,plain,
! [X0] : zero_zero_int = hAPP_int_int(times_times_int(X0),zero_zero_int),
inference(cnf_transformation,[],[f532]) ).
fof(f4128,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t) = twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)),
inference(cnf_transformation,[],[f1094]) ).
fof(f4340,plain,
! [X2,X0,X1] : hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1),
inference(cnf_transformation,[],[f1227]) ).
fof(f4343,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(cnf_transformation,[],[f1235]) ).
fof(f4350,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),pls))),
inference(definition_unfolding,[],[f2634,f2904,f2904,f2969,f2904,f2904,f2969,f2890]) ).
fof(f4351,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),one_one_int),
inference(definition_unfolding,[],[f2635,f2904,f2904,f2969,f2904,f2969]) ).
fof(f4426,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),
inference(definition_unfolding,[],[f2764,f2904,f2969]) ).
fof(f4481,plain,
one_one_int = number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),
inference(definition_unfolding,[],[f2872,f2969]) ).
fof(f4486,plain,
! [X0] :
( ~ is_int(X0)
| pls != X0
| pls = hAPP_int_int(plus_plus_int(X0),X0) ),
inference(definition_unfolding,[],[f2880,f2890,f2890]) ).
fof(f4496,plain,
pls = hAPP_int_int(plus_plus_int(pls),pls),
inference(definition_unfolding,[],[f2889,f2904]) ).
fof(f4510,plain,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(X0),X0)),
inference(definition_unfolding,[],[f2909,f2904]) ).
fof(f4526,plain,
! [X0] : hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))),
inference(definition_unfolding,[],[f2925,f2904,f2969]) ).
fof(f4693,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| pls != X1
| pls = hAPP_int_int(times_times_int(X0),X1) ),
inference(definition_unfolding,[],[f3316,f2890,f2890]) ).
fof(f4695,plain,
! [X0] : pls = hAPP_int_int(times_times_int(X0),pls),
inference(definition_unfolding,[],[f3320,f2890,f2890]) ).
fof(f4870,plain,
twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t),
inference(definition_unfolding,[],[f4128,f2904,f2904,f2969]) ).
fof(f4951,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),one_one_int)),pls)),
inference(definition_unfolding,[],[f4343,f2904,f2969,f2890]) ).
fof(f4994,plain,
( ~ is_int(pls)
| pls = hAPP_int_int(plus_plus_int(pls),pls) ),
inference(equality_resolution,[],[f4486]) ).
fof(f5030,plain,
! [X0] :
( ~ is_int(pls)
| ~ is_int(X0)
| pls = hAPP_int_int(times_times_int(X0),pls) ),
inference(equality_resolution,[],[f4693]) ).
tcf(c_76,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),pls))),
inference(cnf_transformation,[],[f4350]) ).
tcf(c_77,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),one_one_int),
inference(cnf_transformation,[],[f4351]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0),
inference(cnf_transformation,[],[f2680]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] : hAPP_int_int(times_times_int(hAPP_int_int(times_times_int(X0),X1)),X2) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)),
inference(cnf_transformation,[],[f2689]) ).
tcf(c_206,plain,
number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))) = hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat),
inference(cnf_transformation,[],[f4426]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i,X2: $i] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) = hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)),
inference(cnf_transformation,[],[f2836]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i,X2: $i] : hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(X1),hAPP_int_int(plus_plus_int(X0),X2)),
inference(cnf_transformation,[],[f2837]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] : hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0),
inference(cnf_transformation,[],[f2838]) ).
tcf(c_307,plain,
number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)) = one_one_int,
inference(cnf_transformation,[],[f4481]) ).
tcf(c_314,plain,
( ( hAPP_int_int(plus_plus_int(pls),pls) = pls )
| ~ is_int(pls) ),
inference(cnf_transformation,[],[f4994]) ).
tcf(c_324,plain,
hAPP_int_int(plus_plus_int(pls),pls) = pls,
inference(cnf_transformation,[],[f4496]) ).
tcf(c_342,plain,
! [X0: $i] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(X0),X0)),
inference(cnf_transformation,[],[f4510]) ).
tcf(c_358,plain,
! [X0: $i] : hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))) = hAPP_int_int(times_times_int(X0),X0),
inference(cnf_transformation,[],[f4526]) ).
tcf(c_518,plain,
! [X0: $i,X1: $i,X2: $i] : hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)) = hAPP_int_int(times_times_int(X1),hAPP_int_int(times_times_int(X0),X2)),
inference(cnf_transformation,[],[f3086]) ).
tcf(c_621,plain,
! [X0: $i] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),X0) = hAPP_int_int(plus_plus_int(X0),X0),
inference(cnf_transformation,[],[f3193]) ).
tcf(c_627,plain,
! [X0: $i,X1: $i] : hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X1)),X1) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(X0),one_one_int)),X1),
inference(cnf_transformation,[],[f3199]) ).
tcf(c_744,plain,
! [X0: $i] :
( ( hAPP_int_int(times_times_int(X0),pls) = pls )
| ~ is_int(pls)
| ~ is_int(X0) ),
inference(cnf_transformation,[],[f5030]) ).
tcf(c_748,plain,
! [X0: $i] : hAPP_int_int(times_times_int(X0),pls) = pls,
inference(cnf_transformation,[],[f4695]) ).
tcf(c_1509,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t) = twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)),
inference(cnf_transformation,[],[f4870]) ).
tcf(c_1715,plain,
! [X0: $i,X1: $i,X2: $i] : hAPP_int_bool(hAPP_i1948725293t_bool(X0,X1),X2) = hAPP_int_bool(cOMBC_int_int_bool(X0,X2),X1),
inference(cnf_transformation,[],[f4340]) ).
tcf(c_1718,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),one_one_int)),pls)),
inference(cnf_transformation,[],[f4951]) ).
tcf(c_2410,plain,
hAPP_int_int(plus_plus_int(pls),pls) = pls,
inference(global_subsumption_just,[status(thm)],[c_314,c_324]) ).
tcf(c_2418,plain,
! [X0: $i] : hAPP_int_int(times_times_int(X0),pls) = pls,
inference(global_subsumption_just,[status(thm)],[c_744,c_748]) ).
tcf(c_11192,plain,
number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int))) = one_one_int,
inference(demodulation,[status(thm)],[c_307,c_273]) ).
tcf(c_12054,plain,
! [X0: $i,X1: $i] : hAPP_int_int(plus_plus_int(X0),hAPP_int_int(times_times_int(X1),X0)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(X1),one_one_int)),X0),
inference(demodulation,[status(thm)],[c_627,c_273]) ).
tcf(c_13761,plain,
number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))) = hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat),
inference(demodulation,[status(thm)],[c_206,c_271,c_272,c_273]) ).
tcf(c_14580,plain,
! [X0: $i] : hAPP_nat_int(power_power_int(X0),hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat)) = hAPP_int_int(times_times_int(X0),X0),
inference(demodulation,[status(thm)],[c_358,c_271,c_272,c_273,c_13761]) ).
tcf(c_14767,plain,
~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)))),
inference(demodulation,[status(thm)],[c_1718,c_271,c_272,c_273,c_1715,c_13761,c_14580]) ).
tcf(c_15855,plain,
hAPP_int_int(plus_plus_int(t),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(t),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))) = twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)),
inference(demodulation,[status(thm)],[c_1509,c_122,c_131,c_271,c_272,c_273,c_342,c_518,c_621,c_12054,c_11192]) ).
tcf(c_16310,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)),
inference(demodulation,[status(thm)],[c_77,c_122,c_131,c_271,c_272,c_273,c_342,c_518,c_621,c_12054,c_11192,c_13761,c_14580,c_15855]) ).
tcf(c_16315,plain,
~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)))),
inference(demodulation,[status(thm)],[c_14767,c_16310]) ).
tcf(c_16404,plain,
hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu1241645765sum2sq(product_Pair_int_int(s,one_one_int)))),
inference(demodulation,[status(thm)],[c_76,c_122,c_131,c_271,c_272,c_273,c_2410,c_342,c_518,c_2418,c_621,c_12054,c_1715,c_11192,c_15855]) ).
tcf(c_16405,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_16404,c_16315]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+3 : 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.57 % Computer : n016.cluster.edu
% 0.09/0.57 % Model : x86_64 x86_64
% 0.09/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.57 % Memory : 8046.5625MB
% 0.09/0.57 % OS : Linux 6.8.0-71-generic
% 0.09/0.57 % CPULimit : 300
% 0.09/0.57 % WCLimit : 300
% 0.09/0.57 % DateTime : Thu Sep 24 05:46:13 UTC 2026
% 0.09/0.57 % CPUTime :
% 0.09/0.57 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.61 Running first-order theorem proving
% 0.09/0.61 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.09/0.62
% 0.09/0.62 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.62
% 0.09/0.63 % Detected problem language: tptp
% 0.14/0.64 % Proving...
% 7.48/2.81 % SZS status Started for theBenchmark.p
% 7.48/2.81 ERROR - "ProverProcess:heur/346297:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 7.48/2.81 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 7.48/2.81 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_sup_deep_mult 6 --comb_sup_mult 32 --conj_cone_tolerance 2.7380125131254 --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red false --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 1024 --inst_lit_activity_flag true --inst_lit_sel "[+depth;+sign;+num_symb;-split;-eq]" --inst_lit_sel_side cnt --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-num_lits];[-max_atom_input_occur;-ground]]" --inst_passive_queues_freq "[8;50]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.21724605765256222 --inst_solver_per_active 256 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-depth;+non_prol_conj_symb;-split;-ground;+num_var]" --inst_start_prop_sim_after_learn 8 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl true --prep_def_merge_tr_cl true --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim false --prep_sem_filter none --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten false --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 32 --pure_diseq_elim false --resolution_flag false --schedule none --share_sel_clauses false --smt_ac_axioms full --smt_preprocessing true --splitting_cvd true --splitting_cvd_svl false --splitting_grd true --splitting_mode full --splitting_nvd 128 --stats_out none --sub_typing true --subs_bck_mult 0 --sup_full_bw "[Demod]" --sup_full_fw "[Subsumption;SubsumptionRes;UnitSubsAndRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_full_triv "[PropSubs;Unflattening]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability]" --sup_immed_fw_main "[SubsumptionRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_immed_triv "[]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm]" --sup_input_bw "[]" --sup_input_fw "[]" --sup_input_triv "[PropSubs;Unflattening]" --sup_iter_deepening 4 --sup_passive_queue_type queue --sup_passive_queues "[[+num_symb]]" --sup_passive_queues_freq "[5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.4432297345384799 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox/benchmark/theBenchmark.p 1>> /export/starexec/sandbox/tmp/iprover_out_5d0_1fp8/0sef3lyu 2>> /export/starexec/sandbox/tmp/iprover_out_5d0_1fp8/0sef3lyu_error
% 7.48/2.81 % SZS status Theorem for theBenchmark.p
% 7.48/2.81
% 7.48/2.81 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.48/2.81
% 7.48/2.81 % ------ iProver source info
% 7.48/2.81
% 7.48/2.81 % git: date: 2026-07-19 20:42:38 +0200
% 7.48/2.81 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.48/2.81 % git: non_committed_changes: false
% 7.48/2.81
% 7.48/2.81 % ------ Parsing...
% 7.48/2.81 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 7.48/2.81
% 7.48/2.81 % ------ Preprocessing...%
% 7.48/2.81
% 7.48/2.81 % SZS status Theorem for theBenchmark.p
% 7.48/2.81
% 7.48/2.81 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 7.48/2.81
%------------------------------------------------------------------------------