%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM926+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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.22s 0.57s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 64 ( 35 unt; 0 def)
% Number of atoms : 103 ( 73 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 82 ( 43 ~; 31 |; 5 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 54 ( 42 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f40,hypothesis,
! [B_1_1] : ti(int,bit0(B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
! [B_1_1] : ti(int,bit1(B_1_1)) = bit1(B_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
ti(int,t) = t,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
ord_less_eq(int,one_one(int),t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
( t = one_one(int)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
( ord_less(int,one_one(int),t)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [Z_1,W_1] :
( ord_less(int,Z_1,W_1)
<=> ( ti(int,Z_1) != ti(int,W_1)
& ord_less_eq(int,Z_1,W_1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,axiom,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,axiom,
! [K] : number_number_of(int,K) = ti(int,K),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,axiom,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f229,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f653,conjecture,
? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f654,negated_conjecture,
~ ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(negated_conjecture,[status(cth)],[f653]) ).
fof(f760,plain,
! [X0] : ti(int,bit0(X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f762,plain,
! [X0] : ti(int,bit1(X0)) = bit1(X0),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f833,plain,
ti(int,t) = t,
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f834,plain,
ord_less_eq(int,one_one(int),t),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f835,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(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)],[f72]) ).
fof(f836,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(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)],[f835]) ).
fof(f837,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(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)],[f836]) ).
fof(f838,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f839,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ 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)],[f838]) ).
fof(f840,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(cnf_transformation,[status(thm)],[f839]) ).
fof(f871,plain,
! [Z_1,W_1] :
( ( ti(int,Z_1) = ti(int,W_1)
| ~ ord_less_eq(int,Z_1,W_1)
| ord_less(int,Z_1,W_1) )
& ( ( ti(int,Z_1) != ti(int,W_1)
& ord_less_eq(int,Z_1,W_1) )
| ~ ord_less(int,Z_1,W_1) ) ),
inference(NNF_transformation,[status(thm)],[f93]) ).
fof(f872,plain,
( ! [Z_1,W_1] :
( ti(int,Z_1) = ti(int,W_1)
| ~ ord_less_eq(int,Z_1,W_1)
| ord_less(int,Z_1,W_1) )
& ! [Z_1,W_1] :
( ( ti(int,Z_1) != ti(int,W_1)
& ord_less_eq(int,Z_1,W_1) )
| ~ ord_less(int,Z_1,W_1) ) ),
inference(miniscoping,[status(thm)],[f871]) ).
fof(f875,plain,
! [X0,X1] :
( ti(int,X0) = ti(int,X1)
| ~ ord_less_eq(int,X0,X1)
| ord_less(int,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f872]) ).
fof(f1051,plain,
! [X0,X1] : times_times(int,X0,X1) = times_times(int,X1,X0),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f1052,plain,
! [X0] : number_number_of(int,X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f1055,plain,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f1220,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f2269,plain,
! [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(pre_NNF_transformation,[status(thm)],[f654]) ).
fof(f2270,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(cnf_transformation,[status(thm)],[f2269]) ).
fof(f2363,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,m,number_number_of(int,bit0(bit0(bit1(pls))))),one_one(int)),
inference(backward_demodulation,[status(thm)],[f1051,f2270]) ).
fof(f2415,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,bit0(bit0(bit1(pls)))))),
inference(backward_demodulation,[status(thm)],[f1055,f2363]) ).
fof(f3248,plain,
one_one(int) = ti(int,bit1(pls)),
inference(backward_demodulation,[status(thm)],[f1052,f1220]) ).
fof(f3274,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,one_one(int),times_times(int,m,ti(int,bit0(bit0(bit1(pls)))))),
inference(backward_demodulation,[status(thm)],[f1052,f2415]) ).
fof(f3278,plain,
one_one(int) = bit1(pls),
inference(forward_demodulation,[status(thm)],[f762,f3248]) ).
fof(f3304,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(bit1(pls))))),
inference(forward_demodulation,[status(thm)],[f760,f3274]) ).
fof(f3318,plain,
ti(int,one_one(int)) = bit1(pls),
inference(paramodulation,[status(thm)],[f3278,f762]) ).
fof(f3338,plain,
ti(int,one_one(int)) = one_one(int),
inference(forward_demodulation,[status(thm)],[f3278,f3318]) ).
fof(f3356,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(one_one(int)))),power_power(int,X1,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(bit1(pls))))),
inference(forward_demodulation,[status(thm)],[f3278,f3304]) ).
fof(f3357,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(one_one(int)))),power_power(int,X1,number_number_of(nat,bit0(one_one(int))))) != plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(bit1(pls))))),
inference(forward_demodulation,[status(thm)],[f3278,f3356]) ).
fof(f3358,plain,
! [X0,X1] : plus_plus(int,power_power(int,X0,number_number_of(nat,bit0(one_one(int)))),power_power(int,X1,number_number_of(nat,bit0(one_one(int))))) != plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(one_one(int))))),
inference(forward_demodulation,[status(thm)],[f3278,f3357]) ).
fof(f3765,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(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)],[f3278,f837]) ).
fof(f3766,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(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)],[f3278,f3765]) ).
fof(f3767,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f1055,f3766]) ).
fof(f3768,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,bit0(bit0(bit1(pls))))))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f1051,f3767]) ).
fof(f3769,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,ti(int,bit0(bit0(bit1(pls))))))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f1052,f3768]) ).
fof(f3770,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(bit1(pls)))))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f760,f3769]) ).
fof(f3771,plain,
( plus_plus(int,power_power(int,sK0_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK1_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(one_one(int)))))
| t != one_one(int) ),
inference(forward_demodulation,[status(thm)],[f3278,f3770]) ).
fof(f3772,plain,
t != one_one(int),
inference(forward_subsumption_resolution,[status(thm)],[f3771,f3358]) ).
fof(f3838,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f3278,f840]) ).
fof(f3839,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f3278,f3838]) ).
fof(f3840,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f1055,f3839]) ).
fof(f3841,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,bit0(bit0(bit1(pls))))))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f1051,f3840]) ).
fof(f3842,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,ti(int,bit0(bit0(bit1(pls))))))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f1052,f3841]) ).
fof(f3843,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f760,f3842]) ).
fof(f3844,plain,
( plus_plus(int,power_power(int,sK2_skl,number_number_of(nat,bit0(one_one(int)))),power_power(int,sK3_skl,number_number_of(nat,bit0(one_one(int))))) = plus_plus(int,one_one(int),times_times(int,m,bit0(bit0(one_one(int)))))
| ~ ord_less(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f3278,f3843]) ).
fof(f3845,plain,
~ ord_less(int,one_one(int),t),
inference(forward_subsumption_resolution,[status(thm)],[f3844,f3358]) ).
fof(f4695,plain,
( ti(int,one_one(int)) = ti(int,t)
| ~ ord_less_eq(int,one_one(int),t) ),
inference(resolution,[status(thm)],[f875,f3845]) ).
fof(f4723,plain,
( one_one(int) = ti(int,t)
| ~ ord_less_eq(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f3338,f4695]) ).
fof(f4724,plain,
( one_one(int) = t
| ~ ord_less_eq(int,one_one(int),t) ),
inference(forward_demodulation,[status(thm)],[f833,f4723]) ).
fof(f4725,plain,
one_one(int) = t,
inference(forward_subsumption_resolution,[status(thm)],[f4724,f834]) ).
fof(f4823,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4725,f3772]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n006.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 : Mon Sep 21 03:18:27 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.43 % Drodi V4.1.1
% 0.22/0.57 % Refutation found
% 0.22/0.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.22/0.61 % Elapsed time: 0.213243 seconds
% 0.22/0.61 % CPU time: 1.154928 seconds
% 0.22/0.61 % Total memory used: 162.935 MB
% 0.22/0.61 % Net memory used: 162.292 MB
%------------------------------------------------------------------------------