%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : NUM924+6 : 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 3.62s 1.09s
% Output : CNFRefutation 3.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 19
% Syntax : Number of formulae : 79 ( 79 unt; 0 def)
% Number of atoms : 79 ( 63 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 8 ( 8 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 15 ( 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-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 58 ( 0 sgn 58 !; 0 ?; 20 :)
% Comments :
%------------------------------------------------------------------------------
fof(f40,axiom,
! [X0] : ti(int,bit0(X0)) = bit0(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OBit0_res) ).
fof(f42,axiom,
! [X0] : ti(int,bit1(X0)) = bit1(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OBit1_res) ).
fof(f43,axiom,
ti(int,min) = min,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_Int_OMin_res) ).
fof(f68,axiom,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
file('/export/starexec/sandbox2/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(f69,axiom,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
fof(f88,axiom,
! [X0] : number_number_of(int,X0) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(f89,axiom,
! [X0,X1] : times_times(int,X0,X1) = times_times(int,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_zmult__commute) ).
fof(f127,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_61_nat__1__add__1) ).
fof(f128,axiom,
! [X0] : times_times(int,pls,X0) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_mult__Pls) ).
fof(f160,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_94_zadd__assoc) ).
fof(f161,axiom,
! [X0,X1,X2] : plus_plus(int,X0,plus_plus(int,X1,X2)) = plus_plus(int,X1,plus_plus(int,X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_zadd__left__commute) ).
fof(f162,axiom,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_zadd__commute) ).
fof(f186,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_Pls__def) ).
fof(f193,axiom,
! [X0] : plus_plus(int,X0,pls) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_add__Pls__right) ).
fof(f194,axiom,
! [X0] : plus_plus(int,pls,X0) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_add__Pls) ).
fof(f196,axiom,
! [X0] : bit0(X0) = plus_plus(int,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_Bit0__def) ).
fof(f228,axiom,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_Bit1__def) ).
fof(f390,axiom,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_324__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
fof(f650,conjecture,
ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f651,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
inference(negated_conjecture,[status(cth)],[f650]) ).
fof(f652,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
inference(flattening,[],[f651]) ).
fof(f1336,plain,
! [X0] : bit0(X0) = ti(int,bit0(X0)),
inference(cnf_transformation,[],[f40]) ).
fof(f1338,plain,
! [X0] : bit1(X0) = ti(int,bit1(X0)),
inference(cnf_transformation,[],[f42]) ).
fof(f1339,plain,
min = ti(int,min),
inference(cnf_transformation,[],[f43]) ).
fof(f1373,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(cnf_transformation,[],[f68]) ).
fof(f1374,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(cnf_transformation,[],[f69]) ).
fof(f1399,plain,
! [X0] : ti(int,X0) = number_number_of(int,X0),
inference(cnf_transformation,[],[f88]) ).
fof(f1400,plain,
! [X0,X1] : times_times(int,X0,X1) = times_times(int,X1,X0),
inference(cnf_transformation,[],[f89]) ).
fof(f1461,plain,
number_number_of(nat,bit0(bit1(pls))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(cnf_transformation,[],[f127]) ).
fof(f1462,plain,
! [X0] : pls = times_times(int,pls,X0),
inference(cnf_transformation,[],[f128]) ).
fof(f1515,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,[],[f160]) ).
fof(f1516,plain,
! [X2,X0,X1] : plus_plus(int,X0,plus_plus(int,X1,X2)) = plus_plus(int,X1,plus_plus(int,X0,X2)),
inference(cnf_transformation,[],[f161]) ).
fof(f1517,plain,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
inference(cnf_transformation,[],[f162]) ).
fof(f1550,plain,
pls = zero_zero(int),
inference(cnf_transformation,[],[f186]) ).
fof(f1561,plain,
! [X0] : ti(int,X0) = plus_plus(int,X0,pls),
inference(cnf_transformation,[],[f193]) ).
fof(f1562,plain,
! [X0] : ti(int,X0) = plus_plus(int,pls,X0),
inference(cnf_transformation,[],[f194]) ).
fof(f1564,plain,
! [X0] : bit0(X0) = plus_plus(int,X0,X0),
inference(cnf_transformation,[],[f196]) ).
fof(f1605,plain,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[],[f228]) ).
fof(f1822,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = minus_minus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),number_number_of(int,min)),
inference(cnf_transformation,[],[f390]) ).
fof(f2142,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
inference(cnf_transformation,[],[f652]) ).
fof(f2144,plain,
! [X0] : plus_plus(int,X0,X0) = ti(int,plus_plus(int,X0,X0)),
inference(definition_unfolding,[],[f1336,f1564,f1564]) ).
fof(f2146,plain,
! [X0] : plus_plus(int,plus_plus(int,one_one(int),X0),X0) = ti(int,plus_plus(int,plus_plus(int,one_one(int),X0),X0)),
inference(definition_unfolding,[],[f1338,f1605,f1605]) ).
fof(f2147,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),zero_zero(int))),
inference(definition_unfolding,[],[f1373,f1564,f1564,f1605,f1564,f1564,f1605]) ).
fof(f2148,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,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)))),one_one(int)),
inference(definition_unfolding,[],[f1374,f1564,f1564,f1605,f1564,f1605]) ).
fof(f2193,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,[],[f1461,f1564,f1605]) ).
fof(f2340,plain,
plus_plus(int,power_power(int,s,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)))),one_one(int)) = minus_minus(int,power_power(int,s,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)))),number_number_of(int,min)),
inference(definition_unfolding,[],[f1822,f1564,f1605,f1564,f1605]) ).
fof(f2364,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,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)))),one_one(int)),zero_zero(int)),
inference(definition_unfolding,[],[f2142,f1564,f1605]) ).
tcf(c_92,plain,
! [X0: $i] : ti(int,plus_plus(int,X0,X0)) = plus_plus(int,X0,X0),
inference(cnf_transformation,[],[f2144]) ).
tcf(c_94,plain,
! [X0: $i] : ti(int,plus_plus(int,plus_plus(int,one_one(int),X0),X0)) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[],[f2146]) ).
tcf(c_95,plain,
ti(int,min) = min,
inference(cnf_transformation,[],[f1339]) ).
tcf(c_129,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),zero_zero(int))),
inference(cnf_transformation,[],[f2147]) ).
tcf(c_130,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,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)))),one_one(int)),
inference(cnf_transformation,[],[f2148]) ).
tcf(c_155,plain,
! [X0: $i] : ti(int,X0) = number_number_of(int,X0),
inference(cnf_transformation,[],[f1399]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] : times_times(int,X0,X1) = times_times(int,X1,X0),
inference(cnf_transformation,[],[f1400]) ).
tcf(c_217,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,[],[f2193]) ).
tcf(c_218,plain,
! [X0: $i] : times_times(int,pls,X0) = pls,
inference(cnf_transformation,[],[f1462]) ).
tcf(c_268,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,[],[f1515]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i,X2: $i] : plus_plus(int,X0,plus_plus(int,X1,X2)) = plus_plus(int,X1,plus_plus(int,X0,X2)),
inference(cnf_transformation,[],[f1516]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
inference(cnf_transformation,[],[f1517]) ).
tcf(c_303,plain,
zero_zero(int) = pls,
inference(cnf_transformation,[],[f1550]) ).
tcf(c_314,plain,
! [X0: $i] : plus_plus(int,X0,pls) = ti(int,X0),
inference(cnf_transformation,[],[f1561]) ).
tcf(c_315,plain,
! [X0: $i] : plus_plus(int,pls,X0) = ti(int,X0),
inference(cnf_transformation,[],[f1562]) ).
tcf(c_573,plain,
minus_minus(int,power_power(int,s,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)))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,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)))),one_one(int)),
inference(cnf_transformation,[],[f2340]) ).
tcf(c_890,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,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)))),one_one(int)),zero_zero(int)),
inference(cnf_transformation,[],[f2364]) ).
tcf(c_6867,plain,
number_number_of(int,min) = min,
inference(demodulation,[status(thm)],[c_95,c_155]) ).
tcf(c_6900,plain,
! [X0: $i] : plus_plus(int,pls,X0) = number_number_of(int,X0),
inference(light_normalisation,[status(thm)],[c_315,c_155]) ).
tcf(c_6902,plain,
! [X0: $i] : plus_plus(int,X0,pls) = number_number_of(int,X0),
inference(light_normalisation,[status(thm)],[c_314,c_155]) ).
tcf(c_7203,plain,
! [X0: $i] : number_number_of(int,plus_plus(int,X0,X0)) = plus_plus(int,X0,X0),
inference(demodulation,[status(thm)],[c_92,c_155]) ).
tcf(c_8646,plain,
! [X0: $i] : number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,X0,X0))) = plus_plus(int,one_one(int),plus_plus(int,X0,X0)),
inference(demodulation,[status(thm)],[c_94,c_155,c_268]) ).
tcf(c_9616,plain,
number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),number_number_of(int,number_number_of(int,one_one(int))))))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(demodulation,[status(thm)],[c_217,c_268,c_269,c_6900,c_6902]) ).
tcf(c_9851,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,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)))),one_one(int)),pls),
inference(light_normalisation,[status(thm)],[c_890,c_303]) ).
tcf(c_9852,plain,
~ ord_less(int,plus_plus(int,one_one(int),power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat)))),pls),
inference(demodulation,[status(thm)],[c_9851,c_268,c_269,c_270,c_6900,c_6902,c_9616]) ).
tcf(c_10304,plain,
plus_plus(int,power_power(int,s,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)))),one_one(int)) = minus_minus(int,power_power(int,s,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)))),min),
inference(light_normalisation,[status(thm)],[c_573,c_6867]) ).
tcf(c_10305,plain,
plus_plus(int,one_one(int),power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat)))) = minus_minus(int,power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat))),min),
inference(demodulation,[status(thm)],[c_10304,c_268,c_269,c_270,c_6900,c_6902,c_9616]) ).
tcf(c_10307,plain,
~ ord_less(int,minus_minus(int,power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat))),min),pls),
inference(demodulation,[status(thm)],[c_9852,c_10305]) ).
tcf(c_10473,plain,
times_times(int,t,plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),number_number_of(int,plus_plus(int,one_one(int),number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),number_number_of(int,number_number_of(int,one_one(int)))))))))))))) = minus_minus(int,power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat))),min),
inference(demodulation,[status(thm)],[c_130,c_156,c_268,c_269,c_270,c_6900,c_6902,c_7203,c_8646,c_9616,c_10305]) ).
tcf(c_10477,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,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(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),m),one_one(int)),pls)),
inference(light_normalisation,[status(thm)],[c_129,c_303]) ).
tcf(c_10478,plain,
ord_less(int,minus_minus(int,power_power(int,s,plus_plus(nat,one_one(nat),one_one(nat))),min),pls),
inference(demodulation,[status(thm)],[c_10477,c_156,c_218,c_268,c_269,c_270,c_6900,c_6902,c_7203,c_8646,c_10473]) ).
tcf(c_10479,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_10478,c_10307]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % 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:37:16 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 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.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 3.62/1.09 % SZS status Started for theBenchmark.p
% 3.62/1.09 % SZS status Theorem for theBenchmark.p
% 3.62/1.09
% 3.62/1.09 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.62/1.09
% 3.62/1.09 % ------ iProver source info
% 3.62/1.09
% 3.62/1.09 % git: date: 2026-07-19 20:42:38 +0200
% 3.62/1.09 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.62/1.09 % git: non_committed_changes: false
% 3.62/1.09
% 3.62/1.09 % ------ Parsing...
% 3.62/1.09 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.62/1.09
% 3.62/1.09 % ------ Preprocessing...%
% 3.62/1.09
% 3.62/1.09 % SZS status Theorem for theBenchmark.p
% 3.62/1.09
% 3.62/1.09 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.62/1.09
% 3.62/1.09
%------------------------------------------------------------------------------