%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM925_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 : n005.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:17 PM UTC 2026
% Result : Theorem 2.95s 1.35s
% Output : CNFRefutation 2.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 18
% Syntax : Number of formulae : 95 ( 71 unt; 0 typ; 4 def)
% Number of atoms : 357 ( 71 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 74 ( 36 ~; 31 |; 5 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of FOOLs : 225 ( 225 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 69 ( 0 sgn 69 !; 0 ?; 69 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
one_one_int: int ).
tff(pred_def_1,type,
ord_less_int: ( int * int ) > $o ).
tff(pred_def_2,type,
ord_less_nat: ( nat * nat ) > $o ).
tff(func_def_3,type,
plus_plus_nat: ( nat * nat ) > nat ).
tff(func_def_4,type,
zero_zero_int: int ).
tff(func_def_5,type,
zero_zero_nat: nat ).
tff(func_def_6,type,
bit0: int > int ).
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,
semiri1621563631at_int: nat > int ).
tff(func_def_12,type,
semiri984289939at_nat: nat > nat ).
tff(func_def_13,type,
power_power_int: ( nat * int ) > int ).
tff(func_def_14,type,
power_power_nat: ( nat * nat ) > nat ).
tff(func_def_15,type,
n: nat ).
tff(func_def_16,type,
t: int ).
tff(f13,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_semiring__one__add__one__is__two) ).
tff(f20,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_19_zless__linear) ).
tff(f51,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_50_zadd__assoc) ).
tff(f53,axiom,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_zadd__commute) ).
tff(f63,axiom,
~ ord_less_int(pls,zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_bin__less__0__simps_I1_J) ).
tff(f66,axiom,
! [X0: int,X1: int] :
( ord_less_int(X0,plus_plus_int(X1,one_one_int))
<=> ( ( X0 = X1 )
| ord_less_int(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_zless__add1__eq) ).
tff(f67,axiom,
! [X0: nat] : ~ ord_less_int(semiri1621563631at_int(X0),zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_int__less__0__conv) ).
tff(f79,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_Pls__def) ).
tff(f82,axiom,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_add__Pls) ).
tff(f84,axiom,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_Bit0__def) ).
tff(f100,axiom,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_Bit1__def) ).
tff(f104,axiom,
! [X0: int] :
( ord_less_int(zero_zero_int,power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))))
<=> ( X0 != zero_zero_int ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_zero__less__power2) ).
tff(f105,axiom,
! [X0: int] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_power2__less__0) ).
tff(f107,conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
tff(f108,negated_conjecture,
( ( ~ power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) ) != zero_zero_int ),
inference(negated_conjecture,[status(cth)],[f107]) ).
tff(f109,plain,
zero_zero_int = power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))),
inference(flattening,[],[f108]) ).
tff(f141,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_int(X0,plus_plus_int(X1,one_one_int))
| ( X0 = X1 )
| ord_less_int(X0,X1) )
& ( ( ( X0 != X1 )
& ~ ord_less_int(X0,X1) )
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ) ),
inference(nnf_transformation,[],[f66]) ).
tff(f142,plain,
! [X0: int,X1: int] :
( ( ~ ord_less_int(X0,plus_plus_int(X1,one_one_int))
| ( X0 = X1 )
| ord_less_int(X0,X1) )
& ( ( ( X0 != X1 )
& ~ ord_less_int(X0,X1) )
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ) ),
inference(flattening,[],[f141]) ).
tff(f153,plain,
! [X0: int] :
( ( ~ ord_less_int(zero_zero_int,power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))))
| ( X0 != zero_zero_int ) )
& ( ( zero_zero_int = X0 )
| ord_less_int(zero_zero_int,power_power_int(X0,number_number_of_nat(bit0(bit1(pls))))) ) ),
inference(nnf_transformation,[],[f104]) ).
tff(f171,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f13]) ).
tff(f179,plain,
! [X0: int,X1: int] :
( ord_less_int(X1,X0)
| ( X0 = X1 )
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
tff(f225,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,[],[f51]) ).
tff(f227,plain,
! [X0: int,X1: int] : ( plus_plus_int(X0,X1) = plus_plus_int(X1,X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f246,plain,
~ ord_less_int(pls,zero_zero_int),
inference(cnf_transformation,[],[f63]) ).
tff(f251,plain,
! [X0: int,X1: int] :
( ( X0 != X1 )
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ),
inference(cnf_transformation,[],[f142]) ).
tff(f253,plain,
! [X0: nat] : ~ ord_less_int(semiri1621563631at_int(X0),zero_zero_int),
inference(cnf_transformation,[],[f67]) ).
tff(f271,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f79]) ).
tff(f274,plain,
! [X0: int] : ( plus_plus_int(pls,X0) = X0 ),
inference(cnf_transformation,[],[f82]) ).
tff(f276,plain,
! [X0: int] : ( bit0(X0) = plus_plus_int(X0,X0) ),
inference(cnf_transformation,[],[f84]) ).
tff(f296,plain,
! [X0: int] : ( bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0) ),
inference(cnf_transformation,[],[f100]) ).
tff(f301,plain,
! [X0: int] :
( ( zero_zero_int = X0 )
| ord_less_int(zero_zero_int,power_power_int(X0,number_number_of_nat(bit0(bit1(pls))))) ),
inference(cnf_transformation,[],[f153]) ).
tff(f302,plain,
! [X0: int] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(cnf_transformation,[],[f105]) ).
tff(f306,plain,
zero_zero_int = power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))),
inference(cnf_transformation,[],[f109]) ).
tff(f321,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))),
inference(definition_unfolding,[],[f171,f276,f296]) ).
tff(f365,plain,
~ ord_less_int(pls,pls),
inference(definition_unfolding,[],[f246,f271]) ).
tff(f369,plain,
! [X0: nat] : ~ ord_less_int(semiri1621563631at_int(X0),pls),
inference(definition_unfolding,[],[f253,f271]) ).
tff(f400,plain,
! [X0: int] :
( ( pls = X0 )
| ord_less_int(pls,power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))))) ),
inference(definition_unfolding,[],[f301,f271,f276,f296,f271]) ).
tff(f402,plain,
! [X0: int] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),pls),
inference(definition_unfolding,[],[f302,f276,f296,f271]) ).
tff(f406,plain,
pls = power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),
inference(definition_unfolding,[],[f306,f271,f276,f296]) ).
tff(f419,plain,
! [X1: int] : ord_less_int(X1,plus_plus_int(X1,one_one_int)),
inference(equality_resolution,[],[f251]) ).
tcf(c_64,plain,
number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f321]) ).
tcf(c_72,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,[],[f179]) ).
tcf(c_111,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,[],[f225]) ).
tcf(c_113,plain,
! [X0_int: int,X1_int: int] : plus_plus_int(X0_int,X1_int) = plus_plus_int(X1_int,X0_int),
inference(cnf_transformation,[],[f227]) ).
tcf(c_131,plain,
~ ord_less_int(pls,pls),
inference(cnf_transformation,[],[f365]) ).
tcf(c_136,plain,
! [X0_int: int] : ord_less_int(X0_int,plus_plus_int(X0_int,one_one_int)),
inference(cnf_transformation,[],[f419]) ).
tcf(c_138,plain,
! [X0_nat: nat] : ~ ord_less_int(semiri1621563631at_int(X0_nat),pls),
inference(cnf_transformation,[],[f369]) ).
tcf(c_158,plain,
! [X0_int: int] : plus_plus_int(pls,X0_int) = X0_int,
inference(cnf_transformation,[],[f274]) ).
tcf(c_181,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))))
| ( X0_int = pls ) ),
inference(cnf_transformation,[],[f400]) ).
tcf(c_183,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))),pls),
inference(cnf_transformation,[],[f402]) ).
tcf(c_187,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(plus_plus_int(plus_plus_int(one_one_int,pls),pls),plus_plus_int(plus_plus_int(one_one_int,pls),pls)))) = pls,
inference(cnf_transformation,[],[f406]) ).
tcf(c_254,plain,
number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int)))))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(theory_normalisation,[status(thm)],[c_64,c_111,c_113]) ).
tcf(c_271,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))))
| ( X0_int = pls ) ),
inference(theory_normalisation,[status(thm)],[c_181,c_111,c_113]) ).
tcf(c_273,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))),pls),
inference(theory_normalisation,[status(thm)],[c_183,c_111,c_113]) ).
tcf(c_277,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))) = pls,
inference(theory_normalisation,[status(thm)],[c_187,c_111,c_113]) ).
tcf(c_390,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,one_one_int))))))))
| ( X0_int = pls ) ),
inference(prop_impl_just,[status(thm)],[c_271]) ).
tcf(c_1037,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))),pls),
inference(ac_demodulation,[status(thm)],[c_273,c_158,c_111,c_113]) ).
tcf(c_1038,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))),pls),
inference(ac_demodulation,[status(thm)],[c_1037,c_158,c_111,c_113]) ).
tcf(c_1039,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))),pls),
inference(ac_demodulation,[status(thm)],[c_1038,c_158,c_111,c_113]) ).
tcf(c_1040,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))),pls),
inference(ac_demodulation,[status(thm)],[c_1039,c_158,c_111,c_113]) ).
tcf(c_1049,plain,
number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls))))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_254,c_158,c_111,c_113]) ).
tcf(c_1050,plain,
number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls)))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_1049,c_158,c_111,c_113]) ).
tcf(c_1051,plain,
number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_1050,c_158,c_111,c_113]) ).
tcf(c_1052,plain,
number_number_of_nat(plus_plus_int(one_one_int,one_one_int)) = plus_plus_nat(one_one_nat,one_one_nat),
inference(ac_demodulation,[status(thm)],[c_1051,c_158,c_111,c_113]) ).
tcf(c_1054,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,plus_plus_nat(one_one_nat,one_one_nat)),pls),
inference(demodulation,[status(thm)],[c_1040,c_1052]) ).
tcf(c_1086,plain,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))) = pls,
inference(ac_demodulation,[status(thm)],[c_277,c_158,c_111,c_113]) ).
tcf(c_1087,plain,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))) = pls,
inference(ac_demodulation,[status(thm)],[c_1086,c_158,c_111,c_113]) ).
tcf(c_1088,plain,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))) = pls,
inference(ac_demodulation,[status(thm)],[c_1087,c_158,c_111,c_113]) ).
tcf(c_1089,plain,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(one_one_int,one_one_int))) = pls,
inference(ac_demodulation,[status(thm)],[c_1088,c_158,c_111,c_113]) ).
tcf(c_1090,plain,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),plus_plus_nat(one_one_nat,one_one_nat)) = pls,
inference(light_normalisation,[status(thm)],[c_1089,c_1052]) ).
tcf(c_1091,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(pls,plus_plus_int(pls,plus_plus_int(one_one_int,plus_plus_int(one_one_int,pls)))))))
| ( X0_int = pls ) ),
inference(ac_demodulation,[status(thm)],[c_390,c_158,c_111,c_113]) ).
tcf(c_1092,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))
| ( X0_int = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1091,c_158,c_111,c_113]) ).
tcf(c_1093,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))))
| ( X0_int = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1092,c_158,c_111,c_113]) ).
tcf(c_1094,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))))
| ( X0_int = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1093,c_158,c_111,c_113]) ).
tcf(c_1095,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,plus_plus_nat(one_one_nat,one_one_nat)))
| ( X0_int = pls ) ),
inference(light_normalisation,[status(thm)],[c_1094,c_1052]) ).
tcf(c_1269,plain,
! [X0_int: int] :
( ord_less_int(pls,power_power_int(X0_int,plus_plus_nat(one_one_nat,one_one_nat)))
| ( X0_int = pls ) ),
inference(prop_impl_just,[status(thm)],[c_1095]) ).
tcf(c_1893,definition,
iPr_def_10 = semiri1621563631at_int(n),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_1894,definition,
iPr_def_11 = plus_plus_int(one_one_int,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_1895,definition,
iPr_def_12 = plus_plus_nat(one_one_nat,one_one_nat),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_1896,definition,
iPr_def_13 = power_power_int(iPr_def_11,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_1897,plain,
iPr_def_13 = pls,
inference(demodulation,[status(thm)],[c_1090,c_1895,c_1893,c_1894,c_1896]) ).
tcf(c_2545,plain,
~ ord_less_int(iPr_def_13,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_131,c_1897]) ).
tcf(c_2547,plain,
! [X0_nat: nat] : ~ ord_less_int(semiri1621563631at_int(X0_nat),iPr_def_13),
inference(light_normalisation,[status(thm)],[c_138,c_1897]) ).
tcf(c_2554,plain,
~ ord_less_int(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_1893,c_2547]) ).
tcf(c_2563,plain,
plus_plus_int(iPr_def_10,one_one_int) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1894,c_111,c_113]) ).
tcf(c_2564,plain,
ord_less_int(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_2563,c_136]) ).
tcf(c_2631,plain,
! [X0_int: int] : ~ ord_less_int(power_power_int(X0_int,iPr_def_12),iPr_def_13),
inference(light_normalisation,[status(thm)],[c_1054,c_1895,c_1897]) ).
tcf(c_3132,plain,
! [X0_int: int] :
( ord_less_int(iPr_def_13,power_power_int(X0_int,iPr_def_12))
| ( power_power_int(X0_int,iPr_def_12) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_72,c_2631]) ).
tcf(c_3381,plain,
( ord_less_int(iPr_def_13,iPr_def_13)
| ( power_power_int(iPr_def_11,iPr_def_12) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1896,c_3132]) ).
tcf(c_3384,plain,
power_power_int(iPr_def_11,iPr_def_12) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_3381,c_2545]) ).
tcf(c_4342,plain,
! [X0_int: int] :
( ord_less_int(iPr_def_13,power_power_int(X0_int,iPr_def_12))
| ( X0_int = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_1269,c_1895,c_1897]) ).
tcf(c_4349,plain,
( ord_less_int(iPr_def_13,iPr_def_13)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3384,c_4342]) ).
tcf(c_4353,plain,
iPr_def_11 = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_4349,c_2545]) ).
tcf(c_4411,plain,
~ ord_less_int(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_2554,c_4353]) ).
tcf(c_4422,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4411,c_2564]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925_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.13/0.39 % Computer : n005.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Thu Sep 24 05:42:17 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.45 Running first-order theorem proving
% 0.13/0.45 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.13/0.47
% 0.13/0.47 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.47
% 0.13/0.47 % Detected problem language: tptp
% 0.20/0.48 % Proving...
% 2.95/1.35 % SZS status Started for theBenchmark.p
% 2.95/1.35 % SZS status Theorem for theBenchmark.p
% 2.95/1.35
% 2.95/1.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.95/1.35
% 2.95/1.35 % ------ iProver source info
% 2.95/1.35
% 2.95/1.35 % git: date: 2026-07-19 20:42:38 +0200
% 2.95/1.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.95/1.35 % git: non_committed_changes: false
% 2.95/1.35
% 2.95/1.35 % ------ Parsing...
% 2.95/1.35 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 2.95/1.35 %
% 2.95/1.35
% 2.95/1.35 % ------ Preprocessing... sup_sim: 31 pe_s pe_e sup_sim: 0 pe_s pe_e %
% 2.95/1.35
% 2.95/1.35 % ------ Preprocessing...% ------ preprocesses with Global Options Modified: tff_prep: switching off prep_sem_filter, sub_typing, pure_diseq_elim
% 2.95/1.35 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
% 2.95/1.35 %
% 2.95/1.35
% 2.95/1.35 % ------ Preprocessing...
% 2.95/1.35 % ------ Proving...
% 2.95/1.35 % ------ Problem Properties
% 2.95/1.35
% 2.95/1.35 %
% 2.95/1.35 % clauses 86
% 2.95/1.35 % conjectures 0
% 2.95/1.35 % EPR 6
% 2.95/1.35 % Horn 77
% 2.95/1.35 % unary 38
% 2.95/1.35 % binary 44
% 2.95/1.35 % lits 138
% 2.95/1.35 % lits eq 71
% 2.95/1.35 % fd_pure 0
% 2.95/1.35 % fd_pseudo 0
% 2.95/1.35 % fd_cond 9
% 2.95/1.35 % fd_pseudo_cond 6
% 2.95/1.35 % AC symbols 1
% 2.95/1.35
% 2.95/1.35 % ------ Schedule dynamic 5 is on
% 2.95/1.35
% 2.95/1.35 % ------ no conjectures: strip conj schedule
% 2.95/1.35
% 2.95/1.35 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 2.95/1.35
% 2.95/1.35
% 2.95/1.35 % ------
% 2.95/1.35 % Current options:
% 2.95/1.35 % ------
% 2.95/1.35
% 2.95/1.35
% 2.95/1.35 %
% 2.95/1.35
% 2.95/1.35 % ------ Proving...
% 2.95/1.35 %
% 2.95/1.35
% 2.95/1.35 % SZS status Theorem for theBenchmark.p
% 2.95/1.35
% 2.95/1.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.95/1.35
% 2.95/1.35
%------------------------------------------------------------------------------