%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM331+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:32 PM UTC 2026
% Result : Theorem 106.88s 13.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM331+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:22:40 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 106.88/13.96 % Refutation found
% 106.88/13.96 % SZS status Theorem for theBenchmark: Theorem is valid
% 106.88/13.96 % SZS output start CNFRefutation for theBenchmark
% 106.88/13.96 fof(f7,axiom,(
% 106.88/13.96 rdn_translate(n6,rdn_pos(rdnn(n6))) ),
% 106.88/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.96 fof(f8,axiom,(
% 106.88/13.96 rdn_translate(n7,rdn_pos(rdnn(n7))) ),
% 106.88/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.96 fof(f14,axiom,(
% 106.88/13.96 rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1)))) ),
% 106.88/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.96 fof(f287,axiom,(
% 106.88/13.96 (! [X,Y,Z,RDN_X,RDN_Y,RDN_Z] :( ( rdn_translate(X,rdn_pos(RDN_X))& rdn_translate(Y,rdn_pos(RDN_Y))& rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)& rdn_translate(Z,rdn_pos(RDN_Z)) )=> sum(X,Y,Z) ) )),
% 106.88/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.96 fof(f293,axiom,(
% 106.88/13.96 (! [X,Y,Z1,Z2] :( ( sum(X,Y,Z1)& sum(X,Y,Z2) )=> Z1 = Z2 ) )),
% 106.88/13.96 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.96 fof(f298,axiom,(
% 106.88/13.96 (! [C,D1,D2,ID,RD,IC1,IC2] :( ( rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1))& rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))& rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(n1),rdnn(n0)) )=> rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdn(rdnn(RD),rdnn(n1))) ) )),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f312,axiom,(
% 106.88/13.97 rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)) ),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f332,axiom,(
% 106.88/13.97 rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0)) ),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f369,axiom,(
% 106.88/13.97 rdn_digit_add(rdnn(n6),rdnn(n7),rdnn(n3),rdnn(n1)) ),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f378,axiom,(
% 106.88/13.97 rdn_digit_add(rdnn(n7),rdnn(n6),rdnn(n3),rdnn(n1)) ),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f402,conjecture,(
% 106.88/13.97 (! [Z1,Z2] :( ( sum(n6,n7,Z1)& sum(n7,n6,Z2) )=> Z1 = Z2 ) )),
% 106.88/13.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 106.88/13.97 fof(f403,negated_conjecture,(
% 106.88/13.97 ~((! [Z1,Z2] :( ( sum(n6,n7,Z1)& sum(n7,n6,Z2) )=> Z1 = Z2 ) ))),
% 106.88/13.97 inference(negated_conjecture,[status(cth)],[f402])).
% 106.88/13.97 fof(f410,plain,(
% 106.88/13.97 rdn_translate(n6,rdn_pos(rdnn(n6)))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f7])).
% 106.88/13.97 fof(f411,plain,(
% 106.88/13.97 rdn_translate(n7,rdn_pos(rdnn(n7)))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f8])).
% 106.88/13.97 fof(f417,plain,(
% 106.88/13.97 rdn_translate(n13,rdn_pos(rdn(rdnn(n3),rdnn(n1))))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f14])).
% 106.88/13.97 fof(f716,plain,(
% 106.88/13.97 ![X,Y,Z,RDN_X,RDN_Y,RDN_Z]: ((((~rdn_translate(X,rdn_pos(RDN_X))|~rdn_translate(Y,rdn_pos(RDN_Y)))|~rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z))|~rdn_translate(Z,rdn_pos(RDN_Z)))|sum(X,Y,Z))),
% 106.88/13.97 inference(pre_NNF_transformation,[status(thm)],[f287])).
% 106.88/13.97 fof(f717,plain,(
% 106.88/13.97 ![X,Y,Z]: ((![RDN_Z]: ((![RDN_X,RDN_Y]: ((~rdn_translate(X,rdn_pos(RDN_X))|~rdn_translate(Y,rdn_pos(RDN_Y)))|~rdn_add_with_carry(rdnn(n0),RDN_X,RDN_Y,RDN_Z)))|~rdn_translate(Z,rdn_pos(RDN_Z))))|sum(X,Y,Z))),
% 106.88/13.97 inference(miniscoping,[status(thm)],[f716])).
% 106.88/13.97 fof(f718,plain,(
% 106.88/13.97 ![X0,X1,X2,X3,X4,X5]: (~rdn_translate(X0,rdn_pos(X1))|~rdn_translate(X2,rdn_pos(X3))|~rdn_add_with_carry(rdnn(n0),X1,X3,X4)|~rdn_translate(X5,rdn_pos(X4))|sum(X0,X2,X5))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f717])).
% 106.88/13.97 fof(f734,plain,(
% 106.88/13.97 ![X,Y,Z1,Z2]: ((~sum(X,Y,Z1)|~sum(X,Y,Z2))|Z1=Z2)),
% 106.88/13.97 inference(pre_NNF_transformation,[status(thm)],[f293])).
% 106.88/13.97 fof(f735,plain,(
% 106.88/13.97 ![Z1,Z2]: ((![X,Y]: (~sum(X,Y,Z1)|~sum(X,Y,Z2)))|Z1=Z2)),
% 106.88/13.97 inference(miniscoping,[status(thm)],[f734])).
% 106.88/13.97 fof(f736,plain,(
% 106.88/13.97 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~sum(X0,X1,X3)|X2=X3)),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f735])).
% 106.88/13.97 fof(f750,plain,(
% 106.88/13.97 ![C,D1,D2,ID,RD,IC1,IC2]: (((~rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1))|~rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2)))|~rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(n1),rdnn(n0)))|rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdn(rdnn(RD),rdnn(n1))))),
% 106.88/13.97 inference(pre_NNF_transformation,[status(thm)],[f298])).
% 106.88/13.97 fof(f751,plain,(
% 106.88/13.97 ![C,D1,D2,RD]: ((![IC1,IC2]: ((![ID]: (~rdn_digit_add(rdnn(D1),rdnn(D2),rdnn(ID),rdnn(IC1))|~rdn_digit_add(rdnn(ID),rdnn(C),rdnn(RD),rdnn(IC2))))|~rdn_digit_add(rdnn(IC1),rdnn(IC2),rdnn(n1),rdnn(n0))))|rdn_add_with_carry(rdnn(C),rdnn(D1),rdnn(D2),rdn(rdnn(RD),rdnn(n1))))),
% 106.88/13.97 inference(miniscoping,[status(thm)],[f750])).
% 106.88/13.97 fof(f752,plain,(
% 106.88/13.97 ![X0,X1,X2,X3,X4,X5,X6]: (~rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))|~rdn_digit_add(rdnn(X2),rdnn(X4),rdnn(X5),rdnn(X6))|~rdn_digit_add(rdnn(X3),rdnn(X6),rdnn(n1),rdnn(n0))|rdn_add_with_carry(rdnn(X4),rdnn(X0),rdnn(X1),rdn(rdnn(X5),rdnn(n1))))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f751])).
% 106.88/13.97 fof(f771,plain,(
% 106.88/13.97 rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f312])).
% 106.88/13.97 fof(f791,plain,(
% 106.88/13.97 rdn_digit_add(rdnn(n3),rdnn(n0),rdnn(n3),rdnn(n0))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f332])).
% 106.88/13.97 fof(f828,plain,(
% 106.88/13.97 rdn_digit_add(rdnn(n6),rdnn(n7),rdnn(n3),rdnn(n1))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f369])).
% 106.88/13.97 fof(f837,plain,(
% 106.88/13.97 rdn_digit_add(rdnn(n7),rdnn(n6),rdnn(n3),rdnn(n1))),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f378])).
% 106.88/13.97 fof(f861,plain,(
% 106.88/13.97 (?[Z1,Z2]: ((sum(n6,n7,Z1)&sum(n7,n6,Z2))&~Z1=Z2))),
% 106.88/13.97 inference(pre_NNF_transformation,[status(thm)],[f403])).
% 106.88/13.97 fof(f862,plain,(
% 106.88/13.97 ((sum(n6,n7,sK0_skl)&sum(n7,n6,sK1_skl))&~sK0_skl=sK1_skl)),
% 106.88/13.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z1,sK0_skl),skolemize(Z2,sK1_skl)],[f861])).
% 106.88/13.97 fof(f863,plain,(
% 106.88/13.97 sum(n6,n7,sK0_skl)),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f862])).
% 106.88/13.97 fof(f864,plain,(
% 106.88/13.97 sum(n7,n6,sK1_skl)),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f862])).
% 106.88/13.97 fof(f865,plain,(
% 106.88/13.97 ~sK0_skl=sK1_skl),
% 106.88/13.97 inference(cnf_transformation,[status(thm)],[f862])).
% 106.88/13.97 fof(f868,plain,(
% 106.88/13.97 ![X0]: (~sum(n7,n6,X0)|X0=sK1_skl)),
% 106.88/13.97 inference(resolution,[status(thm)],[f736,f864])).
% 106.88/13.97 fof(f869,plain,(
% 106.88/13.97 ![X0]: (~sum(n6,n7,X0)|X0=sK0_skl)),
% 106.88/13.97 inference(resolution,[status(thm)],[f736,f863])).
% 106.88/13.97 fof(f1791,plain,(
% 106.88/13.97 ![X0,X1,X2,X3,X4]: (~rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(n1))|~rdn_digit_add(rdnn(X2),rdnn(X3),rdnn(X4),rdnn(n0))|rdn_add_with_carry(rdnn(X3),rdnn(X0),rdnn(X1),rdn(rdnn(X4),rdnn(n1))))),
% 106.88/13.97 inference(resolution,[status(thm)],[f771,f752])).
% 106.88/13.97 fof(f2342,plain,(
% 106.88/13.97 ![X0,X1,X2,X3,X4,X5,X6]: (~rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(n1))|~rdn_digit_add(rdnn(X2),rdnn(n0),rdnn(X3),rdnn(n0))|~rdn_translate(X4,rdn_pos(rdnn(X0)))|~rdn_translate(X5,rdn_pos(rdnn(X1)))|~rdn_translate(X6,rdn_pos(rdn(rdnn(X3),rdnn(n1))))|sum(X4,X5,X6))),
% 106.88/13.97 inference(resolution,[status(thm)],[f1791,f718])).
% 106.88/13.97 fof(f3059,plain,(
% 106.88/13.97 ![X0,X1,X2,X3,X4]: (~rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(n3),rdnn(n1))|~rdn_translate(X2,rdn_pos(rdnn(X0)))|~rdn_translate(X3,rdn_pos(rdnn(X1)))|~rdn_translate(X4,rdn_pos(rdn(rdnn(n3),rdnn(n1))))|sum(X2,X3,X4))),
% 106.88/13.97 inference(resolution,[status(thm)],[f2342,f791])).
% 106.88/13.97 fof(f4418,plain,(
% 106.88/13.97 ![X0,X1,X2,X3]: (~rdn_digit_add(rdnn(X0),rdnn(X1),rdnn(n3),rdnn(n1))|~rdn_translate(X2,rdn_pos(rdnn(X0)))|~rdn_translate(X3,rdn_pos(rdnn(X1)))|sum(X2,X3,n13))),
% 106.88/13.97 inference(resolution,[status(thm)],[f3059,f417])).
% 106.88/13.97 fof(f9656,plain,(
% 106.88/13.97 ![X0,X1]: (~rdn_translate(X0,rdn_pos(rdnn(n7)))|~rdn_translate(X1,rdn_pos(rdnn(n6)))|sum(X0,X1,n13))),
% 106.88/13.97 inference(resolution,[status(thm)],[f4418,f837])).
% 106.88/13.97 fof(f9657,plain,(
% 106.88/13.97 ![X0,X1]: (~rdn_translate(X0,rdn_pos(rdnn(n6)))|~rdn_translate(X1,rdn_pos(rdnn(n7)))|sum(X0,X1,n13))),
% 106.88/13.97 inference(resolution,[status(thm)],[f4418,f828])).
% 106.88/13.97 fof(f20391,plain,(
% 106.88/13.97 ![X0]: (~rdn_translate(X0,rdn_pos(rdnn(n6)))|sum(n7,X0,n13))),
% 106.88/13.97 inference(resolution,[status(thm)],[f9656,f411])).
% 106.88/13.97 fof(f20392,plain,(
% 106.88/13.97 ![X0]: (~rdn_translate(X0,rdn_pos(rdnn(n6)))|sum(X0,n7,n13))),
% 106.88/13.97 inference(resolution,[status(thm)],[f9657,f411])).
% 106.88/13.97 fof(f20393,plain,(
% 106.88/13.97 sum(n7,n6,n13)),
% 106.88/13.97 inference(resolution,[status(thm)],[f20391,f410])).
% 106.88/13.97 fof(f20394,plain,(
% 106.88/13.97 sum(n6,n7,n13)),
% 106.88/13.97 inference(resolution,[status(thm)],[f20392,f410])).
% 106.88/13.97 fof(f20395,plain,(
% 106.88/13.97 n13=sK1_skl),
% 106.88/13.97 inference(resolution,[status(thm)],[f20393,f868])).
% 106.88/13.97 fof(f20445,plain,(
% 106.88/13.97 sum(n6,n7,sK1_skl)),
% 106.88/13.97 inference(forward_demodulation,[status(thm)],[f20395,f20394])).
% 106.88/13.97 fof(f20446,plain,(
% 106.88/13.97 sK1_skl=sK0_skl),
% 106.88/13.97 inference(resolution,[status(thm)],[f20445,f869])).
% 87.46/14.06 fof(f20450,plain,(
% 87.46/14.06 $false),
% 87.46/14.06 inference(forward_subsumption_resolution,[status(thm)],[f20446,f865])).
% 87.46/14.06 % SZS output end CNFRefutation for theBenchmark.p
% 43.29/14.17 % Elapsed time: 13.791762 seconds
% 43.29/14.17 % CPU time: 108.473166 seconds
% 43.29/14.17 % Total memory used: 699.787 MB
% 43.29/14.17 % Net memory used: 663.711 MB
%------------------------------------------------------------------------------