%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM925_2 : 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 : n017.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:18 PM UTC 2026
% Result : Theorem 1.08s 1.77s
% Output : CNFRefutation 1.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 46 ( 40 unt; 0 typ; 0 def)
% Number of atoms : 110 ( 50 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 33 ( 18 ~; 9 |; 5 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of FOOLs : 50 ( 50 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 16 prp; 0-3 aty)
% Number of functors : 67 ( 67 usr; 20 con; 0-2 aty)
% Number of variables : 37 ( 0 sgn 37 !; 0 ?; 37 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
one_one_int: int ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(pred_def_2,type,
sP0: ( bool * ( bool * int ) ) > $o ).
tff(pred_def_3,type,
sP1: ( bool * ( int * bool ) ) > $o ).
tff(func_def_4,type,
plus_plus_nat: nat > fun_nat_nat ).
tff(func_def_5,type,
plus_plus_real: real > fun_real_real ).
tff(func_def_6,type,
times_times_int: ( int * int ) > int ).
tff(func_def_7,type,
zero_zero_int: int ).
tff(func_def_8,type,
zero_zero_nat: nat ).
tff(func_def_9,type,
zero_zero_real: real ).
tff(func_def_10,type,
if_nat: ( nat * bool ) > fun_nat_nat ).
tff(func_def_11,type,
bit0: int > int ).
tff(func_def_12,type,
bit1: int > int ).
tff(func_def_13,type,
pls: int ).
tff(func_def_14,type,
number_number_of_int: int > int ).
tff(func_def_15,type,
number_number_of_nat: int > nat ).
tff(func_def_16,type,
number267125858f_real: int > real ).
tff(func_def_17,type,
succ: int > int ).
tff(func_def_18,type,
semiri1621563631at_int: fun_nat_int ).
tff(func_def_19,type,
semiri984289939at_nat: fun_nat_nat ).
tff(func_def_20,type,
semiri132038758t_real: fun_nat_real ).
tff(func_def_21,type,
sqrt: real > real ).
tff(func_def_22,type,
ord_less_int: fun_int_fun_int_bool ).
tff(func_def_23,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(func_def_24,type,
ord_less_real: fun_re413263731l_bool ).
tff(func_def_25,type,
ord_less_eq_int: fun_int_fun_int_bool ).
tff(func_def_26,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(func_def_27,type,
ord_less_eq_real: fun_re413263731l_bool ).
tff(func_def_28,type,
power_power_int: int > fun_nat_int ).
tff(func_def_29,type,
power_power_nat: nat > fun_nat_nat ).
tff(func_def_30,type,
power_power_real: real > fun_nat_real ).
tff(func_def_31,type,
fFalse: bool ).
tff(func_def_32,type,
fTrue: bool ).
tff(func_def_33,type,
hAPP_int_bool: ( int * fun_int_bool ) > bool ).
tff(func_def_34,type,
hAPP_int_int: ( int * fun_int_int ) > int ).
tff(func_def_35,type,
hAPP_i1948725293t_bool: ( int * fun_int_fun_int_bool ) > fun_int_bool ).
tff(func_def_36,type,
hAPP_nat_bool: ( nat * fun_nat_bool ) > bool ).
tff(func_def_37,type,
hAPP_nat_int: ( nat * fun_nat_int ) > int ).
tff(func_def_38,type,
hAPP_nat_nat: ( nat * fun_nat_nat ) > nat ).
tff(func_def_39,type,
hAPP_nat_real: ( nat * fun_nat_real ) > real ).
tff(func_def_40,type,
hAPP_n1699378549t_bool: ( nat * fun_nat_fun_nat_bool ) > fun_nat_bool ).
tff(func_def_41,type,
hAPP_real_bool: ( real * fun_real_bool ) > bool ).
tff(func_def_42,type,
hAPP_real_real: ( real * fun_real_real ) > real ).
tff(func_def_43,type,
hAPP_r1134773055l_bool: ( real * fun_re413263731l_bool ) > fun_real_bool ).
tff(func_def_44,type,
m1: int ).
tff(func_def_45,type,
n: nat ).
tff(func_def_46,type,
t: int ).
tff(func_def_47,type,
tn: nat ).
tff(func_def_48,type,
sK2: ( int * fun_int_bool ) > int ).
tff(func_def_49,type,
sK3: int > nat ).
tff(func_def_50,type,
sK4: ( nat * nat ) > nat ).
tff(func_def_51,type,
sK5: ( nat * real ) > real ).
tff(func_def_52,type,
sK6: ( nat * real ) > real ).
tff(func_def_53,type,
sK7: fun_int_bool > int ).
tff(func_def_54,type,
sK8: fun_int_bool > nat ).
tff(func_def_55,type,
sK9: fun_int_bool > nat ).
tff(func_def_56,type,
sK10: fun_int_bool > int ).
tff(func_def_57,type,
sK11: ( int * int ) > nat ).
tff(func_def_58,type,
sK12: int > nat ).
tff(func_def_59,type,
sK13: int > nat ).
tff(func_def_60,type,
sK14: ( nat * nat ) > nat ).
tff(func_def_61,type,
sK15: ( fun_nat_bool * nat ) > nat ).
tff(func_def_62,type,
sK16: int > nat ).
tff(func_def_63,type,
sK17: fun_nat_nat > nat ).
tff(func_def_64,type,
sK18: fun_nat_nat > nat ).
tff(func_def_65,type,
sK19: ( int * fun_int_bool ) > int ).
tff(func_def_66,type,
sK20: ( fun_nat_bool * nat ) > nat ).
tff(func_def_67,type,
sK21: fun_nat_nat > nat ).
tff(func_def_68,type,
sK22: fun_nat_nat > nat ).
tff(func_def_69,type,
sK23: ( real * real ) > real ).
tff(f1,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos) ).
tff(f99,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_Pls__def) ).
tff(f104,axiom,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_Bit0__def) ).
tff(f129,axiom,
! [X0: int] : ( bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_Bit1__def) ).
tff(f286,axiom,
! [X0: int,X1: nat] :
( ( hAPP_nat_int(power_power_int(X0),X1) = zero_zero_int )
<=> ( ( X1 != zero_zero_nat )
& ( X0 = zero_zero_int ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_285_power__eq__0__iff) ).
tff(f289,axiom,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_288_of__nat__less__0__iff) ).
tff(f296,axiom,
zero_zero_int = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_295_transfer__int__nat__numerals_I1_J) ).
tff(f340,axiom,
! [X0: int,X1: int,X2: int] : ( hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_339_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J) ).
tff(f361,axiom,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),zero_zero_int) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_360_add__0__right) ).
tff(f372,axiom,
! [X0: int] : ( hAPP_int_int(plus_plus_int(zero_zero_int),X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_371_add__0__left) ).
tff(f703,conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f704,negated_conjecture,
( ( ~ hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) ) != zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f703]) ).
tff(f707,plain,
zero_zero_int = hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),
inference(flattening,[],[f704]) ).
tff(f1235,plain,
! [X0: int,X1: nat] :
( ( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),X1) )
| ( ( X1 != zero_zero_nat )
& ( X0 = zero_zero_int ) ) )
& ( ( zero_zero_nat = X1 )
| ( zero_zero_int != X0 )
| ( hAPP_nat_int(power_power_int(X0),X1) = zero_zero_int ) ) ),
inference(nnf_transformation,[],[f286]) ).
tff(f1236,plain,
! [X0: int,X1: nat] :
( ( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),X1) )
| ( ( X1 != zero_zero_nat )
& ( X0 = zero_zero_int ) ) )
& ( ( zero_zero_nat = X1 )
| ( zero_zero_int != X0 )
| ( hAPP_nat_int(power_power_int(X0),X1) = zero_zero_int ) ) ),
inference(flattening,[],[f1235]) ).
tff(f1387,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[],[f1]) ).
tff(f1536,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f99]) ).
tff(f1541,plain,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
inference(cnf_transformation,[],[f104]) ).
tff(f1572,plain,
! [X0: int] : ( bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0) ),
inference(cnf_transformation,[],[f129]) ).
tff(f1794,plain,
! [X0: int,X1: nat] :
( ( zero_zero_int != hAPP_nat_int(power_power_int(X0),X1) )
| ( zero_zero_int = X0 ) ),
inference(cnf_transformation,[],[f1236]) ).
tff(f1798,plain,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
inference(cnf_transformation,[],[f289]) ).
tff(f1805,plain,
zero_zero_int = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(cnf_transformation,[],[f296]) ).
tff(f1866,plain,
! [X2: int,X0: int,X1: int] : ( 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,[],[f340]) ).
tff(f1893,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),zero_zero_int) = X0 ),
inference(cnf_transformation,[],[f361]) ).
tff(f1906,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(zero_zero_int),X0) = X0 ),
inference(cnf_transformation,[],[f372]) ).
tff(f2367,plain,
zero_zero_int = hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),
inference(cnf_transformation,[],[f707]) ).
tff(f2368,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(definition_unfolding,[],[f1387,f1536]) ).
tff(f2522,plain,
! [X0: int,X1: nat] :
( ( pls != hAPP_nat_int(power_power_int(X0),X1) )
| ( pls = X0 ) ),
inference(definition_unfolding,[],[f1794,f1536,f1536]) ).
tff(f2524,plain,
! [X0: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),pls)),
inference(definition_unfolding,[],[f1798,f1536]) ).
tff(f2526,plain,
pls = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(definition_unfolding,[],[f1805,f1536]) ).
tff(f2540,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),pls) = X0 ),
inference(definition_unfolding,[],[f1893,f1536]) ).
tff(f2545,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(pls),X0) = X0 ),
inference(definition_unfolding,[],[f1906,f1536]) ).
tff(f2693,plain,
pls = hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),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,[],[f2367,f1536,f1541,f1572]) ).
tcf(c_49,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(cnf_transformation,[],[f2368]) ).
tcf(c_429,plain,
! [X0_int: int,X0_nat: nat] :
( ( X0_int = pls )
| ( hAPP_nat_int(power_power_int(X0_int),X0_nat) != pls ) ),
inference(cnf_transformation,[],[f2522]) ).
tcf(c_433,plain,
! [X0_nat: nat] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0_nat)),pls)),
inference(cnf_transformation,[],[f2524]) ).
tcf(c_440,plain,
hAPP_nat_int(semiri1621563631at_int,zero_zero_nat) = pls,
inference(cnf_transformation,[],[f2526]) ).
tcf(c_489,plain,
! [X0_int: int,X1_int: int,X2_int: int] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0_int),X1_int)),X2_int) = hAPP_int_int(plus_plus_int(X0_int),hAPP_int_int(plus_plus_int(X1_int),X2_int)),
inference(cnf_transformation,[],[f1866]) ).
tcf(c_510,plain,
! [X0_int: int] : hAPP_int_int(plus_plus_int(X0_int),pls) = X0_int,
inference(cnf_transformation,[],[f2540]) ).
tcf(c_523,plain,
! [X0_int: int] : hAPP_int_int(plus_plus_int(pls),X0_int) = X0_int,
inference(cnf_transformation,[],[f2545]) ).
tcf(c_964,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),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)))) = pls,
inference(cnf_transformation,[],[f2693]) ).
tcf(c_1095,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(superposition,[status(thm)],[c_440,c_433]) ).
tcf(c_2710,plain,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) = pls,
inference(demodulation,[status(thm)],[c_964,c_489,c_510,c_523]) ).
tcf(c_2725,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = pls,
inference(superposition,[status(thm)],[c_2710,c_429]) ).
tcf(c_2738,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(demodulation,[status(thm)],[c_49,c_2725]) ).
tcf(c_2740,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_2738,c_1095]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925_2 : 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.37 % Computer : n017.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 05:37:31 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 1.08/1.77 % SZS status Started for theBenchmark.p
% 1.08/1.77 % SZS status Theorem for theBenchmark.p
% 1.08/1.77
% 1.08/1.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.08/1.77
% 1.08/1.77 % ------ iProver source info
% 1.08/1.77
% 1.08/1.77 % git: date: 2026-07-19 20:42:38 +0200
% 1.08/1.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.08/1.77 % git: non_committed_changes: false
% 1.08/1.77
% 1.08/1.77 % ------ Parsing...
% 1.08/1.77 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 1.08/1.77 % ------ Proving...
% 1.08/1.77 % ------ Problem Properties
% 1.08/1.77
% 1.08/1.77 %
% 1.08/1.77 % clauses 916
% 1.08/1.77 % conjectures 1
% 1.08/1.77 % EPR 13
% 1.08/1.77 % Horn 840
% 1.08/1.77 % unary 302
% 1.08/1.77 % binary 411
% 1.08/1.77 % lits 1772
% 1.08/1.77 % lits eq 471
% 1.08/1.77 % fd_pure 1
% 1.08/1.77 % fd_pseudo 0
% 1.08/1.77 % fd_cond 61
% 1.08/1.77 % fd_pseudo_cond 61
% 1.08/1.77 % AC symbols 0
% 1.08/1.77
% 1.08/1.77 % ------ Input Options Time Limit: Unbounded
% 1.08/1.77
% 1.08/1.77
% 1.08/1.77 % ------
% 1.08/1.77 % Current options:
% 1.08/1.77 % ------
% 1.08/1.77
% 1.08/1.77
% 1.08/1.77 %
% 1.08/1.77
% 1.08/1.77 % ------ Proving...
% 1.08/1.77 %
% 1.08/1.77
% 1.08/1.77 % SZS status Theorem for theBenchmark.p
% 1.08/1.77
% 1.08/1.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.08/1.77
% 1.08/1.77
%------------------------------------------------------------------------------