%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM924+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:41:59 PM UTC 2026
% Result : Theorem 0.12s 0.47s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 15
% Syntax : Number of formulae : 69 ( 69 unt; 0 def)
% Number of atoms : 69 ( 42 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 3 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 31 ( 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,hypothesis,
! [B_1_1] : bit0(ti(int,B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,hypothesis,
! [B_1_1] : ti(int,bit0(B_1_1)) = bit0(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,hypothesis,
! [B_1_1] : ti(int,bit1(B_1_1)) = bit1(B_1_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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') ).
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') ).
fof(f88,axiom,
! [K] : number_number_of(int,K) = ti(int,K),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,axiom,
! [W] : times_times(int,pls,W) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,axiom,
! [K,L] : times_times(int,bit0(K),L) = bit0(times_times(int,K,L)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,axiom,
! [Z] : times_times(int,Z,one_one(int)) = ti(int,Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f132,axiom,
! [Z] : times_times(int,one_one(int),Z) = ti(int,Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f175,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,axiom,
! [K,L] : times_times(int,bit1(K),L) = plus_plus(int,bit0(times_times(int,K,L)),L),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
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') ).
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(f756,plain,
! [X0] : bit0(ti(int,X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f757,plain,
! [X0] : ti(int,bit0(X0)) = bit0(X0),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f759,plain,
! [X0] : ti(int,bit1(X0)) = bit1(X0),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f828,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,[status(thm)],[f68]) ).
fof(f829,plain,
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),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f875,plain,
! [X0] : number_number_of(int,X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f876,plain,
! [X0,X1] : times_times(int,X0,X1) = times_times(int,X1,X0),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f1000,plain,
! [X0] : times_times(int,pls,X0) = pls,
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f1001,plain,
! [X0,X1] : times_times(int,bit0(X0),X1) = bit0(times_times(int,X0,X1)),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f1006,plain,
! [X0] : times_times(int,X0,one_one(int)) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f1007,plain,
! [X0] : times_times(int,one_one(int),X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f1132,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f1133,plain,
! [X0,X1] : times_times(int,bit1(X0),X1) = plus_plus(int,bit0(times_times(int,X0,X1)),X1),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f1158,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f2259,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,[status(thm)],[f651]) ).
fof(f2295,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),pls),
inference(backward_demodulation,[status(thm)],[f1158,f2259]) ).
fof(f3348,plain,
! [X0] : times_times(int,bit1(X0),one_one(int)) = plus_plus(int,bit0(ti(int,X0)),one_one(int)),
inference(paramodulation,[status(thm)],[f1006,f1133]) ).
fof(f3368,plain,
! [X0] : ti(int,bit1(X0)) = plus_plus(int,bit0(ti(int,X0)),one_one(int)),
inference(forward_demodulation,[status(thm)],[f1006,f3348]) ).
fof(f3369,plain,
! [X0] : bit1(X0) = plus_plus(int,bit0(ti(int,X0)),one_one(int)),
inference(forward_demodulation,[status(thm)],[f759,f3368]) ).
fof(f3370,plain,
! [X0] : bit1(X0) = plus_plus(int,bit0(X0),one_one(int)),
inference(forward_demodulation,[status(thm)],[f756,f3369]) ).
fof(f3924,plain,
one_one(int) = ti(int,bit1(pls)),
inference(backward_demodulation,[status(thm)],[f875,f1132]) ).
fof(f3933,plain,
one_one(int) = bit1(pls),
inference(forward_demodulation,[status(thm)],[f759,f3924]) ).
fof(f3961,plain,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)),pls),
inference(backward_demodulation,[status(thm)],[f3933,f2295]) ).
fof(f4503,plain,
! [X0] : pls = times_times(int,X0,pls),
inference(paramodulation,[status(thm)],[f1000,f876]) ).
fof(f4555,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,ti(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(forward_demodulation,[status(thm)],[f875,f828]) ).
fof(f4556,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(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(forward_demodulation,[status(thm)],[f757,f4555]) ).
fof(f4557,plain,
ord_less(int,times_times(int,plus_plus(int,bit0(times_times(int,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(forward_demodulation,[status(thm)],[f1001,f4556]) ).
fof(f4558,plain,
ord_less(int,times_times(int,bit1(times_times(int,bit0(bit1(pls)),m)),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(forward_demodulation,[status(thm)],[f3370,f4557]) ).
fof(f4559,plain,
ord_less(int,times_times(int,bit1(bit0(times_times(int,bit1(pls),m))),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(forward_demodulation,[status(thm)],[f1001,f4558]) ).
fof(f4560,plain,
ord_less(int,times_times(int,bit1(bit0(times_times(int,one_one(int),m))),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(forward_demodulation,[status(thm)],[f3933,f4559]) ).
fof(f4561,plain,
ord_less(int,times_times(int,bit1(bit0(ti(int,m))),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(forward_demodulation,[status(thm)],[f1007,f4560]) ).
fof(f4562,plain,
ord_less(int,times_times(int,bit1(bit0(m)),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(forward_demodulation,[status(thm)],[f756,f4561]) ).
fof(f4563,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,plus_plus(int,times_times(int,ti(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f875,f4562]) ).
fof(f4564,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,plus_plus(int,times_times(int,bit0(bit0(bit1(pls))),m),one_one(int)),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f757,f4563]) ).
fof(f4565,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,plus_plus(int,bit0(times_times(int,bit0(bit1(pls)),m)),one_one(int)),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f1001,f4564]) ).
fof(f4566,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(times_times(int,bit0(bit1(pls)),m)),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f3370,f4565]) ).
fof(f4567,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(bit0(times_times(int,bit1(pls),m))),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f1001,f4566]) ).
fof(f4568,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(bit0(times_times(int,one_one(int),m))),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f3933,f4567]) ).
fof(f4569,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(bit0(ti(int,m))),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f1007,f4568]) ).
fof(f4570,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(bit0(m)),zero_zero(int))),
inference(forward_demodulation,[status(thm)],[f756,f4569]) ).
fof(f4571,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),times_times(int,bit1(bit0(m)),pls)),
inference(forward_demodulation,[status(thm)],[f1158,f4570]) ).
fof(f4578,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),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),
inference(forward_demodulation,[status(thm)],[f3933,f829]) ).
fof(f4579,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,ti(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
inference(forward_demodulation,[status(thm)],[f875,f4578]) ).
fof(f4580,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,bit0(bit0(bit1(pls))),m),one_one(int)),t),
inference(forward_demodulation,[status(thm)],[f757,f4579]) ).
fof(f4581,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,plus_plus(int,bit0(times_times(int,bit0(bit1(pls)),m)),one_one(int)),t),
inference(forward_demodulation,[status(thm)],[f1001,f4580]) ).
fof(f4582,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,bit1(times_times(int,bit0(bit1(pls)),m)),t),
inference(forward_demodulation,[status(thm)],[f3370,f4581]) ).
fof(f4583,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,bit1(bit0(times_times(int,bit1(pls),m))),t),
inference(forward_demodulation,[status(thm)],[f1001,f4582]) ).
fof(f4584,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,bit1(bit0(times_times(int,one_one(int),m))),t),
inference(forward_demodulation,[status(thm)],[f3933,f4583]) ).
fof(f4585,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,bit1(bit0(ti(int,m))),t),
inference(forward_demodulation,[status(thm)],[f1007,f4584]) ).
fof(f4589,plain,
~ ord_less(int,times_times(int,bit1(bit0(m)),t),pls),
inference(backward_demodulation,[status(thm)],[f4590,f3961]) ).
fof(f4590,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(one_one(int)))),one_one(int)) = times_times(int,bit1(bit0(m)),t),
inference(forward_demodulation,[status(thm)],[f756,f4585]) ).
fof(f4632,plain,
ord_less(int,times_times(int,bit1(bit0(m)),t),pls),
inference(backward_demodulation,[status(thm)],[f4503,f4571]) ).
fof(f4650,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4632,f4589]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n011.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 03:16:56 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.47 % Refutation found
% 0.12/0.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/0.53 % Elapsed time: 0.153729 seconds
% 0.15/0.53 % CPU time: 0.801053 seconds
% 0.15/0.53 % Total memory used: 153.752 MB
% 0.15/0.53 % Net memory used: 153.021 MB
%------------------------------------------------------------------------------