%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM926+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:42:02 PM UTC 2026
% Result : Theorem 0.21s 0.65s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 12
% Syntax : Number of formulae : 63 ( 32 unt; 0 def)
% Number of atoms : 106 ( 67 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 81 ( 38 ~; 34 |; 5 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-4 aty)
% Number of variables : 54 ( 42 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f51,hypothesis,
! [B_1_1] : ti(int,bit0(B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,hypothesis,
! [B_1_1] : ti(int,bit1(B_1_1)) = bit1(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [B_1_1,X_a] :
( number(X_a)
=> ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
( t = one_one(int)
=> ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f100,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,axiom,
! [Z_2,W_1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))
<=> ( ti(int,Z_2) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [K_1] : number_number_of(int,K_1) = ti(int,K_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f258,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1149,axiom,
number(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1255,conjecture,
? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1256,negated_conjecture,
~ ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(negated_conjecture,[status(cth)],[f1255]) ).
fof(f1357,plain,
! [X0] : ti(int,bit0(X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f1359,plain,
! [X0] : ti(int,bit1(X0)) = bit1(X0),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f1365,plain,
! [B_1_1,X_a] :
( ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1)
| ~ number(X_a) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f1366,plain,
! [X_a] :
( ! [B_1_1] : ti(X_a,number_number_of(X_a,B_1_1)) = number_number_of(X_a,B_1_1)
| ~ number(X_a) ),
inference(miniscoping,[status(thm)],[f1365]) ).
fof(f1367,plain,
! [X0,X1] :
( ti(X0,number_number_of(X0,X1)) = number_number_of(X0,X1)
| ~ number(X0) ),
inference(cnf_transformation,[status(thm)],[f1366]) ).
fof(f1417,plain,
ti(int,t) = t,
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f1418,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f1419,plain,
( ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f1420,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl)],[f1419]) ).
fof(f1421,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(cnf_transformation,[status(thm)],[f1420]) ).
fof(f1422,plain,
( ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f1423,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f1422]) ).
fof(f1424,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(cnf_transformation,[status(thm)],[f1423]) ).
fof(f1455,plain,
! [Z_2,W_1] :
( ( ti(int,Z_2) = ti(int,W_1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1)) )
& ( ( ti(int,Z_2) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1)) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1)) ) ),
inference(NNF_transformation,[status(thm)],[f120]) ).
fof(f1456,plain,
( ! [Z_2,W_1] :
( ti(int,Z_2) = ti(int,W_1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1)) )
& ! [Z_2,W_1] :
( ( ti(int,Z_2) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1)) )
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1)) ) ),
inference(miniscoping,[status(thm)],[f1455]) ).
fof(f1459,plain,
! [X0,X1] :
( ti(int,X0) = ti(int,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1456]) ).
fof(f1641,plain,
! [X0] : number_number_of(int,X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f1809,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f4394,plain,
number(int),
inference(cnf_transformation,[status(thm)],[f1149]) ).
fof(f4502,plain,
! [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(pre_NNF_transformation,[status(thm)],[f1256]) ).
fof(f4503,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(cnf_transformation,[status(thm)],[f4502]) ).
fof(f5788,plain,
( ti(int,one_one(int)) = number_number_of(int,bit1(pls))
| ~ number(int) ),
inference(paramodulation,[status(thm)],[f1809,f1367]) ).
fof(f5794,plain,
( ti(int,one_one(int)) = one_one(int)
| ~ number(int) ),
inference(forward_demodulation,[status(thm)],[f1809,f5788]) ).
fof(f5795,plain,
ti(int,one_one(int)) = one_one(int),
inference(forward_subsumption_resolution,[status(thm)],[f5794,f4394]) ).
fof(f6111,plain,
number_number_of(int,t) = t,
inference(backward_demodulation,[status(thm)],[f1641,f1417]) ).
fof(f6117,plain,
! [X0] : number_number_of(int,bit1(X0)) = bit1(X0),
inference(backward_demodulation,[status(thm)],[f1641,f1359]) ).
fof(f6118,plain,
! [X0] : number_number_of(int,bit0(X0)) = bit0(X0),
inference(backward_demodulation,[status(thm)],[f1641,f1357]) ).
fof(f6287,plain,
one_one(int) = bit1(pls),
inference(backward_demodulation,[status(thm)],[f6117,f1809]) ).
fof(f6364,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(one_one(int))))),m)),one_one(int)),
inference(backward_demodulation,[status(thm)],[f6287,f4503]) ).
fof(f6425,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(one_one(int))))),m)),one_one(int)),
inference(forward_demodulation,[status(thm)],[f6287,f6364]) ).
fof(f6426,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(one_one(int))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(one_one(int))))),m)),one_one(int)),
inference(forward_demodulation,[status(thm)],[f6287,f6425]) ).
fof(f6689,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X0),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(one_one(int))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(one_one(int)))),m)),one_one(int)),
inference(forward_demodulation,[status(thm)],[f6118,f6426]) ).
fof(f6892,plain,
number_number_of(int,one_one(int)) = one_one(int),
inference(forward_demodulation,[status(thm)],[f1641,f5795]) ).
fof(f7559,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f6287,f1421]) ).
fof(f7560,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f6287,f7559]) ).
fof(f7561,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m)),one_one(int))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f6118,f7560]) ).
fof(f7562,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK1_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(one_one(int)))),m)),one_one(int))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f6287,f7561]) ).
fof(f7563,plain,
t != one_one(int),
inference(forward_subsumption_resolution,[status(thm)],[f7562,f6689]) ).
fof(f7719,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6287,f1424]) ).
fof(f7720,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6287,f7719]) ).
fof(f7721,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(bit1(pls)))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6118,f7720]) ).
fof(f7722,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2_skl),number_number_of(nat,bit0(one_one(int))))),hAPP(nat,int,power_power(int,sK3_skl),number_number_of(nat,bit0(one_one(int))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,bit0(bit0(one_one(int)))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6287,f7721]) ).
fof(f7723,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)),
inference(forward_subsumption_resolution,[status(thm)],[f7722,f6689]) ).
fof(f8786,plain,
! [X0,X1] :
( number_number_of(int,X0) = ti(int,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(forward_demodulation,[status(thm)],[f1641,f1459]) ).
fof(f8787,plain,
! [X0,X1] :
( number_number_of(int,X0) = number_number_of(int,X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1)) ),
inference(forward_demodulation,[status(thm)],[f1641,f8786]) ).
fof(f8788,plain,
( number_number_of(int,one_one(int)) = number_number_of(int,t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(resolution,[status(thm)],[f8787,f1418]) ).
fof(f8801,plain,
( one_one(int) = number_number_of(int,t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6892,f8788]) ).
fof(f8802,plain,
( one_one(int) = t
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(forward_demodulation,[status(thm)],[f6111,f8801]) ).
fof(f8803,plain,
one_one(int) = t,
inference(forward_subsumption_resolution,[status(thm)],[f8802,f7723]) ).
fof(f8885,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f8803,f7563]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 03:18:33 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.21/0.49 % Drodi V4.1.1
% 0.21/0.65 % Refutation found
% 0.21/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/0.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.63/0.72 % Elapsed time: 0.357581 seconds
% 0.63/0.72 % CPU time: 1.398745 seconds
% 0.63/0.72 % Total memory used: 238.373 MB
% 0.63/0.72 % Net memory used: 237.479 MB
%------------------------------------------------------------------------------