%------------------------------------------------------------------------------
% 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 : 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:17 PM UTC 2026
% Result : Theorem 1.14s 1.29s
% Output : CNFRefutation 1.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 18
% Syntax : Number of formulae : 95 ( 71 unt; 4 def)
% Number of atoms : 175 ( 71 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 74 ( 36 ~; 31 |; 5 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 69 ( 0 sgn 69 !; 0 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
fof(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) ).
fof(f20,axiom,
! [X0,X1] :
( ord_less_int(X1,X0)
| X0 = X1
| ord_less_int(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_zless__linear) ).
fof(f51,axiom,
! [X0,X1,X2] : 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) ).
fof(f53,axiom,
! [X0,X1] : plus_plus_int(X0,X1) = plus_plus_int(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_zadd__commute) ).
fof(f63,axiom,
~ ord_less_int(pls,zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_bin__less__0__simps_I1_J) ).
fof(f66,axiom,
! [X0,X1] :
( 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) ).
fof(f67,axiom,
! [X0] : ~ ord_less_int(semiri1621563631at_int(X0),zero_zero_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_int__less__0__conv) ).
fof(f79,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_Pls__def) ).
fof(f82,axiom,
! [X0] : plus_plus_int(pls,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_add__Pls) ).
fof(f84,axiom,
! [X0] : bit0(X0) = plus_plus_int(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_Bit0__def) ).
fof(f100,axiom,
! [X0] : bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_Bit1__def) ).
fof(f104,axiom,
! [X0] :
( 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) ).
fof(f105,axiom,
! [X0] : ~ 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) ).
fof(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) ).
fof(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]) ).
fof(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]) ).
fof(f141,plain,
! [X0,X1] :
( ( ~ 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]) ).
fof(f142,plain,
! [X0,X1] :
( ( ~ 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]) ).
fof(f153,plain,
! [X0] :
( ( ~ 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]) ).
fof(f171,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(cnf_transformation,[],[f13]) ).
fof(f179,plain,
! [X0,X1] :
( ord_less_int(X1,X0)
| X0 = X1
| ord_less_int(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f225,plain,
! [X2,X0,X1] : plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)),
inference(cnf_transformation,[],[f51]) ).
fof(f227,plain,
! [X0,X1] : plus_plus_int(X0,X1) = plus_plus_int(X1,X0),
inference(cnf_transformation,[],[f53]) ).
fof(f246,plain,
~ ord_less_int(pls,zero_zero_int),
inference(cnf_transformation,[],[f63]) ).
fof(f251,plain,
! [X0,X1] :
( X0 != X1
| ord_less_int(X0,plus_plus_int(X1,one_one_int)) ),
inference(cnf_transformation,[],[f142]) ).
fof(f253,plain,
! [X0] : ~ ord_less_int(semiri1621563631at_int(X0),zero_zero_int),
inference(cnf_transformation,[],[f67]) ).
fof(f271,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f79]) ).
fof(f274,plain,
! [X0] : plus_plus_int(pls,X0) = X0,
inference(cnf_transformation,[],[f82]) ).
fof(f276,plain,
! [X0] : bit0(X0) = plus_plus_int(X0,X0),
inference(cnf_transformation,[],[f84]) ).
fof(f296,plain,
! [X0] : bit1(X0) = plus_plus_int(plus_plus_int(one_one_int,X0),X0),
inference(cnf_transformation,[],[f100]) ).
fof(f301,plain,
! [X0] :
( 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]) ).
fof(f302,plain,
! [X0] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(cnf_transformation,[],[f105]) ).
fof(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]) ).
fof(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]) ).
fof(f365,plain,
~ ord_less_int(pls,pls),
inference(definition_unfolding,[],[f246,f271]) ).
fof(f369,plain,
! [X0] : ~ ord_less_int(semiri1621563631at_int(X0),pls),
inference(definition_unfolding,[],[f253,f271]) ).
fof(f400,plain,
! [X0] :
( 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]) ).
fof(f402,plain,
! [X0] : ~ 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]) ).
fof(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]) ).
fof(f419,plain,
! [X1] : 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: $i,X1: $i] :
( ord_less_int(X1,X0)
| ord_less_int(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] : plus_plus_int(plus_plus_int(X0,X1),X2) = plus_plus_int(X0,plus_plus_int(X1,X2)),
inference(cnf_transformation,[],[f225]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] : plus_plus_int(X0,X1) = plus_plus_int(X1,X0),
inference(cnf_transformation,[],[f227]) ).
tcf(c_131,plain,
~ ord_less_int(pls,pls),
inference(cnf_transformation,[],[f365]) ).
tcf(c_136,plain,
! [X0: $i] : ord_less_int(X0,plus_plus_int(X0,one_one_int)),
inference(cnf_transformation,[],[f419]) ).
tcf(c_138,plain,
! [X0: $i] : ~ ord_less_int(semiri1621563631at_int(X0),pls),
inference(cnf_transformation,[],[f369]) ).
tcf(c_158,plain,
! [X0: $i] : plus_plus_int(pls,X0) = X0,
inference(cnf_transformation,[],[f274]) ).
tcf(c_181,plain,
! [X0: $i] :
( 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)))))
| ( X0 = pls ) ),
inference(cnf_transformation,[],[f400]) ).
tcf(c_183,plain,
! [X0: $i] : ~ 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(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: $i] :
( ord_less_int(pls,power_power_int(X0,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 = pls ) ),
inference(theory_normalisation,[status(thm)],[c_181,c_111,c_113]) ).
tcf(c_273,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,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_392,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,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 = pls ) ),
inference(prop_impl_just,[status(thm)],[c_271]) ).
tcf(c_1036,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,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_1037,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,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_1036,c_158,c_111,c_113]) ).
tcf(c_1038,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))),pls),
inference(ac_demodulation,[status(thm)],[c_1037,c_158,c_111,c_113]) ).
tcf(c_1039,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))),pls),
inference(ac_demodulation,[status(thm)],[c_1038,c_158,c_111,c_113]) ).
tcf(c_1048,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_1049,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_1048,c_158,c_111,c_113]) ).
tcf(c_1050,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_1049,c_158,c_111,c_113]) ).
tcf(c_1051,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_1050,c_158,c_111,c_113]) ).
tcf(c_1053,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,plus_plus_nat(one_one_nat,one_one_nat)),pls),
inference(demodulation,[status(thm)],[c_1039,c_1051]) ).
tcf(c_1085,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_1086,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_1085,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(pls,one_one_int)))) = 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,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)),plus_plus_nat(one_one_nat,one_one_nat)) = pls,
inference(light_normalisation,[status(thm)],[c_1088,c_1051]) ).
tcf(c_1090,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,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 = pls ) ),
inference(ac_demodulation,[status(thm)],[c_392,c_158,c_111,c_113]) ).
tcf(c_1091,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(one_one_int,plus_plus_int(pls,pls))))))
| ( X0 = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1090,c_158,c_111,c_113]) ).
tcf(c_1092,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,plus_plus_int(pls,one_one_int)))))
| ( X0 = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1091,c_158,c_111,c_113]) ).
tcf(c_1093,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,number_number_of_nat(plus_plus_int(one_one_int,one_one_int))))
| ( X0 = pls ) ),
inference(ac_demodulation,[status(thm)],[c_1092,c_158,c_111,c_113]) ).
tcf(c_1094,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,plus_plus_nat(one_one_nat,one_one_nat)))
| ( X0 = pls ) ),
inference(light_normalisation,[status(thm)],[c_1093,c_1051]) ).
tcf(c_1283,plain,
! [X0: $i] :
( ord_less_int(pls,power_power_int(X0,plus_plus_nat(one_one_nat,one_one_nat)))
| ( X0 = pls ) ),
inference(prop_impl_just,[status(thm)],[c_1094]) ).
tcf(c_1913,definition,
iPr_def_10 = semiri1621563631at_int(n),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_1914,definition,
iPr_def_11 = plus_plus_int(one_one_int,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_1915,definition,
iPr_def_12 = plus_plus_nat(one_one_nat,one_one_nat),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_1916,definition,
iPr_def_13 = power_power_int(iPr_def_11,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_1917,plain,
iPr_def_13 = pls,
inference(demodulation,[status(thm)],[c_1089,c_1915,c_1913,c_1914,c_1916]) ).
tcf(c_3153,plain,
~ ord_less_int(iPr_def_13,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_131,c_1917]) ).
tcf(c_3155,plain,
! [X0: $i] : ~ ord_less_int(semiri1621563631at_int(X0),iPr_def_13),
inference(light_normalisation,[status(thm)],[c_138,c_1917]) ).
tcf(c_3162,plain,
~ ord_less_int(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_1913,c_3155]) ).
tcf(c_3171,plain,
plus_plus_int(iPr_def_10,one_one_int) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1914,c_111,c_113]) ).
tcf(c_3172,plain,
ord_less_int(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_3171,c_136]) ).
tcf(c_3239,plain,
! [X0: $i] : ~ ord_less_int(power_power_int(X0,iPr_def_12),iPr_def_13),
inference(light_normalisation,[status(thm)],[c_1053,c_1915,c_1917]) ).
tcf(c_3740,plain,
! [X0: $i] :
( ord_less_int(iPr_def_13,power_power_int(X0,iPr_def_12))
| ( power_power_int(X0,iPr_def_12) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_72,c_3239]) ).
tcf(c_3995,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_1916,c_3740]) ).
tcf(c_3998,plain,
power_power_int(iPr_def_11,iPr_def_12) = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_3995,c_3153]) ).
tcf(c_4914,plain,
! [X0: $i] :
( ord_less_int(iPr_def_13,power_power_int(X0,iPr_def_12))
| ( X0 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_1283,c_1915,c_1917]) ).
tcf(c_4921,plain,
( ord_less_int(iPr_def_13,iPr_def_13)
| ( iPr_def_11 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3998,c_4914]) ).
tcf(c_4925,plain,
iPr_def_11 = iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_4921,c_3153]) ).
tcf(c_4981,plain,
~ ord_less_int(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_3162,c_4925]) ).
tcf(c_4992,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4981,c_3172]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM925+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 05:38:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/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.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.43 % Detected problem language: tptp
% 0.09/0.44 % Proving...
% 1.14/1.29 % SZS status Started for theBenchmark.p
% 1.14/1.29 % SZS status Theorem for theBenchmark.p
% 1.14/1.29
% 1.14/1.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.14/1.29
% 1.14/1.29 % ------ iProver source info
% 1.14/1.29
% 1.14/1.29 % git: date: 2026-07-19 20:42:38 +0200
% 1.14/1.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.14/1.29 % git: non_committed_changes: false
% 1.14/1.29
% 1.14/1.29 % ------ Parsing...
% 1.14/1.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.14/1.29
% 1.14/1.29 % ------ Preprocessing... sup_sim: 31 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 1.14/1.29
% 1.14/1.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 1.14/1.29
% 1.14/1.29 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 1.14/1.29 % ------ Proving...
% 1.14/1.29 % ------ Problem Properties
% 1.14/1.29
% 1.14/1.29 %
% 1.14/1.29 % clauses 86
% 1.14/1.29 % conjectures 0
% 1.14/1.29 % EPR 6
% 1.14/1.29 % Horn 77
% 1.14/1.29 % unary 38
% 1.14/1.29 % binary 44
% 1.14/1.29 % lits 138
% 1.14/1.29 % lits eq 71
% 1.14/1.29 % fd_pure 0
% 1.14/1.29 % fd_pseudo 0
% 1.14/1.29 % fd_cond 9
% 1.14/1.29 % fd_pseudo_cond 6
% 1.14/1.29 % AC symbols 1
% 1.14/1.29
% 1.14/1.29 % ------ Schedule dynamic 5 is on
% 1.14/1.29
% 1.14/1.29 % ------ no conjectures: strip conj schedule
% 1.14/1.29
% 1.14/1.29 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 1.14/1.29
% 1.14/1.29
% 1.14/1.29 % ------
% 1.14/1.29 % Current options:
% 1.14/1.29 % ------
% 1.14/1.29
% 1.14/1.29
% 1.14/1.29 %
% 1.14/1.29
% 1.14/1.29 % ------ Proving...
% 1.14/1.29 %
% 1.14/1.29
% 1.14/1.29 % SZS status Theorem for theBenchmark.p
% 1.14/1.29
% 1.14/1.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.14/1.29
% 1.14/1.29
%------------------------------------------------------------------------------