%------------------------------------------------------------------------------
% 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 : n002.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.06s 1.74s
% Output : CNFRefutation 1.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 49 ( 43 unt; 0 def)
% Number of atoms : 64 ( 53 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 33 ( 18 ~; 9 |; 5 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn 46 !; 0 ?; 11 :)
% Comments :
%------------------------------------------------------------------------------
fof(f6,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) ).
fof(f104,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_Pls__def) ).
fof(f109,axiom,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_Bit0__def) ).
fof(f134,axiom,
! [X0] : 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) ).
fof(f291,axiom,
! [X0,X1] :
( 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) ).
fof(f294,axiom,
! [X0] : ~ 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) ).
fof(f301,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) ).
fof(f345,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(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) ).
fof(f348,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/sandbox2/benchmark/theBenchmark.p',fact_342_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J) ).
fof(f366,axiom,
! [X0] : hAPP_int_int(plus_plus_int(X0),zero_zero_int) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_360_add__0__right) ).
fof(f377,axiom,
! [X0] : hAPP_int_int(plus_plus_int(zero_zero_int),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_371_add__0__left) ).
fof(f708,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) ).
fof(f709,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)],[f708]) ).
fof(f712,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,[],[f709]) ).
fof(f1242,plain,
! [X0,X1] :
( ( 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,[],[f291]) ).
fof(f1243,plain,
! [X0,X1] :
( ( 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,[],[f1242]) ).
fof(f1399,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,[],[f6]) ).
fof(f1548,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f104]) ).
fof(f1553,plain,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
inference(cnf_transformation,[],[f109]) ).
fof(f1584,plain,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
inference(cnf_transformation,[],[f134]) ).
fof(f1806,plain,
! [X0,X1] :
( zero_zero_int != hAPP_nat_int(power_power_int(X0),X1)
| zero_zero_int = X0 ),
inference(cnf_transformation,[],[f1243]) ).
fof(f1810,plain,
! [X0] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),zero_zero_int)),
inference(cnf_transformation,[],[f294]) ).
fof(f1817,plain,
zero_zero_int = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(cnf_transformation,[],[f301]) ).
fof(f1878,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,[],[f345]) ).
fof(f1881,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,[],[f348]) ).
fof(f1905,plain,
! [X0] : hAPP_int_int(plus_plus_int(X0),zero_zero_int) = X0,
inference(cnf_transformation,[],[f366]) ).
fof(f1918,plain,
! [X0] : hAPP_int_int(plus_plus_int(zero_zero_int),X0) = X0,
inference(cnf_transformation,[],[f377]) ).
fof(f2379,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,[],[f712]) ).
fof(f2380,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,[],[f1399,f1548]) ).
fof(f2534,plain,
! [X0,X1] :
( pls != hAPP_nat_int(power_power_int(X0),X1)
| pls = X0 ),
inference(definition_unfolding,[],[f1806,f1548,f1548]) ).
fof(f2536,plain,
! [X0] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),pls)),
inference(definition_unfolding,[],[f1810,f1548]) ).
fof(f2538,plain,
pls = hAPP_nat_int(semiri1621563631at_int,zero_zero_nat),
inference(definition_unfolding,[],[f1817,f1548]) ).
fof(f2552,plain,
! [X0] : hAPP_int_int(plus_plus_int(X0),pls) = X0,
inference(definition_unfolding,[],[f1905,f1548]) ).
fof(f2557,plain,
! [X0] : hAPP_int_int(plus_plus_int(pls),X0) = X0,
inference(definition_unfolding,[],[f1918,f1548]) ).
fof(f2705,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,[],[f2379,f1548,f1553,f1584]) ).
tcf(c_54,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,[],[f2380]) ).
tcf(c_434,plain,
! [X0: $i,X1: $i] :
( ( X0 = pls )
| ( hAPP_nat_int(power_power_int(X0),X1) != pls ) ),
inference(cnf_transformation,[],[f2534]) ).
tcf(c_438,plain,
! [X0: $i] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_nat_int(semiri1621563631at_int,X0)),pls)),
inference(cnf_transformation,[],[f2536]) ).
tcf(c_445,plain,
hAPP_nat_int(semiri1621563631at_int,zero_zero_nat) = pls,
inference(cnf_transformation,[],[f2538]) ).
tcf(c_494,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,[],[f1878]) ).
tcf(c_497,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,[],[f1881]) ).
tcf(c_515,plain,
! [X0: $i] : hAPP_int_int(plus_plus_int(X0),pls) = X0,
inference(cnf_transformation,[],[f2552]) ).
tcf(c_528,plain,
! [X0: $i] : hAPP_int_int(plus_plus_int(pls),X0) = X0,
inference(cnf_transformation,[],[f2557]) ).
tcf(c_969,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,[],[f2705]) ).
tcf(c_1099,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(superposition,[status(thm)],[c_445,c_438]) ).
tcf(c_2606,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_969,c_494,c_497,c_515,c_528]) ).
tcf(c_2617,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = pls,
inference(superposition,[status(thm)],[c_2606,c_434]) ).
tcf(c_2634,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(demodulation,[status(thm)],[c_54,c_2617]) ).
tcf(c_2636,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_2634,c_1099]) ).
%------------------------------------------------------------------------------
%----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.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 05:45:04 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.42 Running first-order theorem proving
% 0.11/0.42 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.06/1.74 % SZS status Started for theBenchmark.p
% 1.06/1.74 % SZS status Theorem for theBenchmark.p
% 1.06/1.74
% 1.06/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.06/1.74
% 1.06/1.74 % ------ iProver source info
% 1.06/1.74
% 1.06/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 1.06/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.06/1.74 % git: non_committed_changes: false
% 1.06/1.74
% 1.06/1.74 % ------ Parsing...
% 1.06/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 1.06/1.74 % ------ Proving...
% 1.06/1.74 % ------ Problem Properties
% 1.06/1.74
% 1.06/1.74 %
% 1.06/1.74 % clauses 921
% 1.06/1.74 % conjectures 1
% 1.06/1.74 % EPR 15
% 1.06/1.74 % Horn 845
% 1.06/1.74 % unary 307
% 1.06/1.74 % binary 410
% 1.06/1.74 % lits 1778
% 1.06/1.74 % lits eq 471
% 1.06/1.74 % fd_pure 0
% 1.06/1.74 % fd_pseudo 0
% 1.06/1.74 % fd_cond 62
% 1.06/1.74 % fd_pseudo_cond 61
% 1.06/1.74 % AC symbols 0
% 1.06/1.74
% 1.06/1.74 % ------ Input Options Time Limit: Unbounded
% 1.06/1.74
% 1.06/1.74
% 1.06/1.74 % ------
% 1.06/1.74 % Current options:
% 1.06/1.74 % ------
% 1.06/1.74
% 1.06/1.74
% 1.06/1.74 %
% 1.06/1.74
% 1.06/1.74 % ------ Proving...
% 1.06/1.74 %
% 1.06/1.74
% 1.06/1.74 % SZS status Theorem for theBenchmark.p
% 1.06/1.74
% 1.06/1.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.06/1.74
% 1.06/1.74
%------------------------------------------------------------------------------