%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM925+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:01 PM UTC 2026
% Result : Theorem 7.64s 1.90s
% Output : CNFRefutation 8.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 48 ( 38 unt; 0 def)
% Number of atoms : 66 ( 45 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 36 ( 18 ~; 12 |; 4 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-4 aty)
% Number of variables : 48 ( 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f106,hypothesis,
ti(int,pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f325,axiom,
! [K,L] :
( hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L)
<=> ti(int,K) = ti(int,L) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f329,axiom,
! [Z_1,W] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z_1),W) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),W),Z_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [K_4] : ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),K_4)),zero_zero(int))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f354,axiom,
hAPP(int,int,bit0,pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f358,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f360,axiom,
! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),pls) = ti(int,K_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f361,axiom,
! [K_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),K_4) = ti(int,K_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f375,axiom,
! [K_4,L_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit1,K_4)),hAPP(int,int,bit0,L_4)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),L_4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f377,axiom,
! [K_4] : hAPP(int,int,bit1,K_4) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),K_4)),K_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f570,axiom,
! [Wa,Z] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Wa),one_one(int))),Z))
<=> hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Wa),Z)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f594,axiom,
! [X] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5747,conjecture,
hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5748,negated_conjecture,
~ ( hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) != zero_zero(int) ),
inference(negated_conjecture,[status(cth)],[f5747]) ).
fof(f5887,plain,
ti(int,pls) = pls,
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f6211,plain,
! [K,L] :
( ( ti(int,K) != ti(int,L)
| hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L) )
& ( ti(int,K) = ti(int,L)
| hAPP(int,int,bit0,K) != hAPP(int,int,bit0,L) ) ),
inference(NNF_transformation,[status(thm)],[f325]) ).
fof(f6212,plain,
( ! [K,L] :
( ti(int,K) != ti(int,L)
| hAPP(int,int,bit0,K) = hAPP(int,int,bit0,L) )
& ! [K,L] :
( ti(int,K) = ti(int,L)
| hAPP(int,int,bit0,K) != hAPP(int,int,bit0,L) ) ),
inference(miniscoping,[status(thm)],[f6211]) ).
fof(f6214,plain,
! [X0,X1] :
( ti(int,X0) != ti(int,X1)
| hAPP(int,int,bit0,X0) = hAPP(int,int,bit0,X1) ),
inference(cnf_transformation,[status(thm)],[f6212]) ).
fof(f6222,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X0),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f6272,plain,
! [X0] : ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),X0)),zero_zero(int))),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f6304,plain,
hAPP(int,int,bit0,pls) = pls,
inference(cnf_transformation,[status(thm)],[f354]) ).
fof(f6313,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f6315,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f6316,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),X0) = ti(int,X0),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f6343,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,X1)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1)),
inference(cnf_transformation,[status(thm)],[f375]) ).
fof(f6345,plain,
! [X0] : hAPP(int,int,bit1,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X0),
inference(cnf_transformation,[status(thm)],[f377]) ).
fof(f6938,plain,
! [Wa,Z] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Wa),Z))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Wa),one_one(int))),Z)) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Wa),Z))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Wa),one_one(int))),Z)) ) ),
inference(NNF_transformation,[status(thm)],[f570]) ).
fof(f6939,plain,
( ! [Wa,Z] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Wa),Z))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Wa),one_one(int))),Z)) )
& ! [Wa,Z] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Wa),Z))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Wa),one_one(int))),Z)) ) ),
inference(miniscoping,[status(thm)],[f6938]) ).
fof(f6940,plain,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X0),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1)) ),
inference(cnf_transformation,[status(thm)],[f6939]) ).
fof(f7000,plain,
! [X0] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),
inference(cnf_transformation,[status(thm)],[f594]) ).
fof(f20963,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = zero_zero(int),
inference(cnf_transformation,[status(thm)],[f5748]) ).
fof(f21502,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f6313,f20963]) ).
fof(f21761,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,semiring_1_of_nat(int),n)),one_one(int))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(backward_demodulation,[status(thm)],[f6222,f21502]) ).
fof(f21985,plain,
! [X0] : ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),X0)),pls)),
inference(forward_demodulation,[status(thm)],[f6313,f6272]) ).
fof(f22077,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit1,X1)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X0)),
inference(forward_demodulation,[status(thm)],[f6222,f6343]) ).
fof(f22078,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),pls),hAPP(int,int,bit1,X0)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)),
inference(paramodulation,[status(thm)],[f6304,f22077]) ).
fof(f22082,plain,
! [X0] : ti(int,hAPP(int,int,bit1,X0)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),pls)),
inference(forward_demodulation,[status(thm)],[f6316,f22078]) ).
fof(f22083,plain,
! [X0] : ti(int,hAPP(int,int,bit1,X0)) = hAPP(int,int,bit1,ti(int,X0)),
inference(forward_demodulation,[status(thm)],[f6315,f22082]) ).
fof(f22096,plain,
! [X0,X1] :
( ti(int,X0) != hAPP(int,int,bit1,ti(int,X1))
| hAPP(int,int,bit0,X0) = hAPP(int,int,bit0,hAPP(int,int,bit1,X1)) ),
inference(paramodulation,[status(thm)],[f22083,f6214]) ).
fof(f22107,plain,
hAPP(int,int,bit1,pls) = ti(int,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),pls)),
inference(paramodulation,[status(thm)],[f6315,f6345]) ).
fof(f22129,plain,
hAPP(int,int,bit1,pls) = ti(int,ti(int,one_one(int))),
inference(forward_demodulation,[status(thm)],[f6315,f22107]) ).
fof(f23688,plain,
! [X0] :
( ti(int,X0) != hAPP(int,int,bit1,pls)
| hAPP(int,int,bit0,X0) = hAPP(int,int,bit0,hAPP(int,int,bit1,pls)) ),
inference(paramodulation,[status(thm)],[f5887,f22096]) ).
fof(f23857,plain,
hAPP(int,int,bit0,ti(int,one_one(int))) = hAPP(int,int,bit0,hAPP(int,int,bit1,pls)),
inference(resolution,[status(thm)],[f23688,f22129]) ).
fof(f23874,plain,
hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,semiring_1_of_nat(int),n)),one_one(int))),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int))))) = pls,
inference(backward_demodulation,[status(thm)],[f23857,f21761]) ).
fof(f24023,plain,
! [X0] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X0),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),X0),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int))))))),
inference(forward_demodulation,[status(thm)],[f23857,f7000]) ).
fof(f24041,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,semiring_1_of_nat(int),n)),one_one(int))),pls)),
inference(paramodulation,[status(thm)],[f23874,f24023]) ).
fof(f24080,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(nat,int,semiring_1_of_nat(int),n)),pls)),
inference(resolution,[status(thm)],[f24041,f6940]) ).
fof(f24090,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f24080,f21985]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+8 : 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.37 % Computer : n004.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 : Mon Sep 21 03:18:05 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.55/0.87 % Drodi V4.1.1
% 7.64/1.90 % Refutation found
% 7.64/1.90 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.64/1.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.81/2.04 % Elapsed time: 1.665049 seconds
% 4.81/2.04 % CPU time: 8.766490 seconds
% 4.81/2.04 % Total memory used: 1.032 GB
% 4.81/2.04 % Net memory used: 1.028 GB
%------------------------------------------------------------------------------